| The formula is true of all behaviors (sequences of states) such that Init is true in the initial state and Next \/ board'=board is true of all pairs of subsequent states. For the definition \A move \in ... : EnvNext(move), TLC attempts to construct a successor state such that the formula EnvNext holds for all values in the set, and this is certainly not what you intend. Formally,
board' = Append(board, move)
would have to hold simultaneously for all values move \in Move, as well as board' = board (because of the clause for Pass), and this is impossible. Therefore TLC cannot construct any successor state (except stuttering) for the initial state and signals a deadlock.
When you replace \A by \E, TLC will construct one successor state per move, as well as the (stuttering) successor for Pass. In this way, you obtain the tree (or in general, graph) of reachable states. Every branch of this tree corresponds to a possible behavior satisfying your spec, and TLC will evaluate the properties over each branch.
Note by the way that the transition for Pass is an explicit stuttering step according to your definitions, indistinguishable from the implicit stuttering transition that is anyway possible for TLA+ specifications.
Regards, Stephan
Is it that
Spec == Init /\ [][Next]_<<board>>
essentially means: A starting state and all individual state transitions? And "there exists" would mean "an individual state transition" but "for all" means "all possible transitions"? Which would end making the Spec mean: A starting state and all "all possible" state transitions... which doesn't really make any sense? On Tuesday, April 12, 2016 at 12:52:50 PM UTC-7, Justin Scott wrote: 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 tlaplu...@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.
--
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.
|