On 1 Feb 2021, at 12:19, Oleg Levchenko <olevzon@xxxxxxxxx> wrote:
Is there any way in TLC to debug spec?
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
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "a2"]
/\ UNCHANGED turn
Caveats:
- 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).
Greetings,
Michael
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8127E210-670F-4357-8D60-864D086C9B46%40gmail.com.