Synthesis of Strategies for Games - The Unknown Component Problem: Theory and Applications - page 263

Fig. 17.1 Topology for
modeling the game NIM by
language equation solving

Fig. 17.2 Graphical output
of BALM showing the
automaton spec.aut used
in the script for the example
fixed.mv modeling the
game NIM

The automaton is complete and deterministic.
1 inputs 3 states 5 transitions
Inputs = { out(3) }

playing

OK

done

notOK

1wins 2wins

Similarly for Player 2. If out = done , then Player 2 has won. If out = notOK ,
then Player 1 has won. To solve for the winning strategy for Player 2 moving second,
we start with an initial condition 321 for the pile heights. We know that this is
a winnable condition for Player 2 starting second. So the game solution should
indicate this. Heights 653 would be another winnable starting condition for Player
2. We leave to the reader to design the automaton that encodes the fixed part of the
NIM game and to describe it in the format BLIF-MV for BALM.
The specification used is a simple 3-state automaton as shown in Fig. 17.2 .Note
that state 1wins is shaded to indicate that it is not an accepting state. We note
that this automaton can be described in BLIF-MV format too and the command
solve fsm equ can be used.
To solve for the winning strategy, the following script is executed in BALM:

read_blif_mv fixed.mv
extract_aut fixed.aut