in case you can load your spec in ProB, you can use the animation views to debug your spec and inspect the enabling conditions
of the various actions.
Below is a screenshot of the ProB2-UI animator for the Peterson.tla example and showing why the action a1 is not enabled:
a1(self) == /\ pc[self] = "a1"
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "a2"]
/\ UNCHANGED turn
- ProB only supports a subset of TLA+. In particular, it needs to be able to infer a type for every identifier.
- the terminology and syntax used in the State View and REPL comes from the B language, I am afraid
(but this can in principle be improved by extending the pretty-printer of ProB).