Re: [tlaplus] TLC Deadlock on simple spec.

[Stephan Merz <stepha...@xxxxxxxxx>]

Look at the definition of the next-state predicate: I am sure you meant to write \E (there exists) instead of \A (for all)?

Regards,
Stephan

> On 12 Apr 2016, at 20:02, justin.ja...@xxxxxxxxx wrote:
> 
> 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
> 
> =============================================================================
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.