Thanks. That was it!
Can you help me understand what was off in my thinking?
My original thought was that since I defined the state change for any element of Move and for the Pass, it seemed natural that saying for all elements of Move and pass, the spec would be satisfied. Does the "for all" have some more nuanced meaning that I'm missing?
Thanks,
Justin
On Tuesday, April 12, 2016 at 12:22:08 PM UTC-7, Stephan Merz wrote:
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...@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...@googlegroups.com.
> 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.