понедельник, 1 февраля 2021 г. в 15:43:12 UTC+3, leuschel:
Hi Oleg,On 1 Feb 2021, at 12:19, Oleg Levchenko <ole...@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 conditionsof 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 turnCaveats:- 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