To illustrate the great flexibility we have in defining strategies to control the process of execution of rules, we discuss a second example, namely, a system module NIM specifying a version of the game of Nim. There are two players and two bags of pebbles: a "draw" bag to remove pebbles from, and a "limit" bag to limit the number of pebbles that can be removed. We represent each state of the game as a pair of bags, where the first one represents the draw bag and the second one the limit bag. The two players take turns making moves in the game. At each move a player draws a nonempty set of pebbles not exceeding those in the limit bag. The limit bag is then readjusted to contain the least number of pebbles in either the double of what the player just drew, or what was left in the draw bag. The game then continues with the two bags in this new state. This move is axiomatized by the rule mv. The player who empties the draw bag wins.
mod NIM is
protecting MACHINE-INT .
sorts Pebble Bag State .
subsorts Pebble < Bag .
op o : -> Pebble .
op emptyBag : -> Bag .
op __ : Bag Bag -> Bag [assoc id: emptyBag] .
op <_;_> : Bag Bag -> State .
op size : Bag -> MachineInt .
op readjust : Bag Bag -> Bag .
vars X Y Z : Bag .
eq size((o X))
= size(X) + 1 .
eq size(emptyBag)
= 0 .
eq readjust(X, Y)
= if size((X X)) <= size(Y)
then (X X)
else Y
fi .
crl [mv] : < (X Y) ; Z >
=> < Y ; readjust(X, Y) >
if size(X) <= size(Z) and (X =/= emptyBag) .
endm
The initial model described by this module is the transition system containing exactly all the possible game moves allowed by the game. But there are many bad moves that would allow the other player to win. A good player should avoid such bad moves by trying to have a winning strategy. With such a strategy, each move made by the player inexorably leads to success, no matter what moves the other player attempts.
As we have already said, there is great freedom for defining many different strategy languages inside Maude. Even if some users decide to adopt a particular strategy language because of its good features, such a language remains fully extensible, so that new features and new strategies can be defined on top of them.
We define a winning strategy for the Nim game in the following extension of the module STRATEGY.
fmod NIM-STRATEGY is
protecting STRATEGY .
op moveToWin : -> Strategy .
op findWinMove : Term Term -> Term .
op noWinMove : -> Term .
op NIM : -> Module .
var T X Y Z : Term .
var M : Module .
eq NIM
= (mod 'NIM is
including 'BOOL .
including 'MACHINE-INT .
sorts 'Pebble ; 'Bag ; 'State .
subsort 'Pebble < 'Bag .
op 'o : nil -> 'Pebble [none] .
op 'emptyBag : nil -> 'Bag [none] .
op '__ : ('Bag 'Bag) -> 'Bag
[assoc id({'emptyBag}'Bag)] .
op '<_;_> : ('Bag 'Bag) -> 'State [none] .
op 'size : 'Bag -> 'MachineInt [none].
op 'readjust : ('Bag 'Bag) -> 'Bag [none] .
var 'X : 'Bag .
var 'Y : 'Bag .
var 'Z : 'Bag .
none
eq 'size['__[{'o}'Pebble, 'X]]
= '_+_['size['X], {'1}'MachineInt] .
eq 'size[{'emptyBag}'Bag] = {'0}'MachineInt .
eq 'readjust['X, 'Y]
= 'if_then_else_fi[
'_<=_['size['__['X, 'X]], 'size['Y]],
'__['X, 'X],
'Y] .
crl['mv]: '<_;_>['__['X, 'Y], 'Z]
=> '<_;_>['Y, 'readjust['X, 'Y]]
if '_and_['_<=_['size['X], 'size['Z]],
'_=/=_['X, {'emptyBag}'Bag]]
= {'true}'Bool .
endm) .
eq rewInWin(M, T, nilBindingList, moveToWin)
= if findWinMove(T, {'o}'Pebble) == noWinMove
then failure
else rewInWin(M, findWinMove(T, {'o}'Pebble),
nilBindingList, idle)
fi .
eq findWinMove('<_;_>[X, Y], Z)
= if meta-reduce(NIM, '_>=_['size[Y], 'size[Z]])
== {'true}'Bool
then (if findWinMove(
extTerm(
meta-apply(NIM, '<_;_>[X, Y],
'mv, ('X <- Z), 0)), {'o}'Pebble)
== noWinMove
then extTerm(
meta-apply(NIM, '<_;_>[X, Y],
'mv, ('X <- Z), 0))
else findWinMove('<_;_>[X, Y], '__[Z, {'o}'Pebble])
fi)
else noWinMove
fi .
endfm
Given a state < X ; Y > in the game, the strategy moveToWin finds a winning move < X' ; Y' > if there is one, in the sense that either < X' ; Y' > is equal to < emptyBag ; emptyBag > or < X' ; Y' > is a move that eventually will lead to success, no matter which moves the other players attempts, assuming that in the following moves the player that makes the winning move uses the same winning strategy.
The strategy moveToWin calls the function findWinMove with the representation of a bag with only one pebble as its second argument. This argument is used as a tentative move. If the tentative bag Z is valid (the number of pebbles in it is smaller than the number of pebbles in the limit bag) then we tentatively make that move; if it is the case that from the new state of the game there is no winning move for the other player, then we make that move; but, if there is a winning move for our opponent, then findWinMove is called again with the tentative number of pebbles to remove increased by one. If the size of the tentative bag is greater than the size of the limit bag, then there is no possible winning move and failure is returned.
For example, to make a winning move from a state with a draw bag with seven pebbles and a limit bag with three pebbles we use the following strategy expression:
Maude> rew rewInWith(NIM,
'<_;_>['__[{'o}'Pebble, {'o}'Pebble, {'o}'Pebble,
{'o}'Pebble, {'o}'Pebble, {'o}'Pebble,
{'o}'Pebble],
'__[{'o}'Pebble, {'o}'Pebble, {'o}'Pebble]],
nilBindingList, moveToWin) .
result StrategyExpression:
rewInWith(NIM,
'<_;_>['__[{'o}'Pebble,{'o}'Pebble,{'o}'Pebble,
{'o}'Pebble,{'o}'Pebble],
'__[{'o}'Pebble,{'o}'Pebble,{'o}'Pebble,
{'o}'Pebble]], nilBindingList, idle)
There are, of course, states of the game from which no winning move can be made. In these cases, the strategy moveToWin will return failure. For example:
Maude> rew rewInWith(NIM,
'<_;_>['__[{'o}'Pebble, {'o}'Pebble, {'o}'Pebble],
{'o}'Pebble], nilBindingList, moveToWin) .
result StrategyExpression: failure