TLC Deadlock on simple spec.

[justin.ja...@xxxxxxxxx]

Hi all! I'm learning TLA and trying to write a small spec that I can run TLC on. The gist of this spec is that a game board is a sequence of moves (as in: each is a state change of the board).

Any thoughts on what's off in it would be helpful.

Thanks,

Justin

Below is the the tla, cfg, and tlc ouput.

The tlc output is:

TLC2 Version 2.05 of 24 October 2012
Running in Model-Checking mode.
Parsing file Game.tla
Parsing file /home/justinscott/tla/tla2sany/StandardModules/Sequences.tla
Parsing file /home/justinscott/tla/tla2sany/StandardModules/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module Game
Starting... (2016-04-12 10:57:29)
Computing initial states...
Finished computing initial states: 1 distinct state generated.
Warning: The variable board was changed while it is specified as UNCHANGED at
line 22, col 25 to line 22, col 29 of module Game
(Use the -nowarning option to disable this warning.)
Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
board = <<m0>>

The coverage statistics at 2016-04-12 10:57:34
  line 20, col 21 to line 20, col 48 of module Game: 0
  line 22, col 25 to line 22, col 29 of module Game: 0
End of statistics.
1 states generated, 1 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
Finished. (2016-04-12 10:57:35)

Game.cfg:

SPECIFICATION Spec
INVARIANTS TypeOk
CONSTANT Move = {m0, m1, m2, m3}
CONSTANT Initial = m0
CONSTANT Pass = pass

Game.tla:

----------------------------- MODULE Game ------------------------------- 

LOCAL INSTANCE Sequences \* Imports definitions for private use.

CONSTANTS Move,    \* The set of all possible board state changes.
          Initial, \* The starting state of the board.
          Pass     \* A move where no action is taken.

ASSUME Initial \in Move \* Initial is of type Move.
ASSUME Pass \notin Move \* Pass cannot be a Move.

VARIABLES board \* A board state.

TypeOk == board \in Seq(Move) \* board is an ordered sequence of changes.

-----------------------------------------------------------------------------

Init == board = << Initial >> \* board's starting state is the initial change from nothing.

MovePlayed(move) == board' = Append(board, move)

MovePassed == UNCHANGED board

EnvNext(move) == \/ (move \in Move /\ MovePlayed(move))
                 \/ (move \in {Pass} /\ MovePassed)

-----------------------------------------------------------------------------

Next == \A move \in Move \union {Pass} : EnvNext(move) \* A player plays a move or passes.

Spec == Init /\ [][Next]_board

-----------------------------------------------------------------------------

THEOREM Spec => []TypeOk

=============================================================================