Hello Brian,
You could add one additional reset event, which sets the generated
program counter variable pc to the state it has defined by the
also generated Init formula. So in the file below the translation
of your PlusCal code you can add something like:
reset == /\ pc = [self \in ProcSet |-> "<your first label here>"]
/\ <here the reset of part of the system state>
There you can also reset part of your global state.
Then you would have to define a new Next formula including the reset
event like this:
NNext == Next \/ reset
And use it for the new Spec:
NSpec == Init /\ [][NNext]_vars
Hope it works, but I haven't tried it.
Best regards,
Stefan
--
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...@googlegroups.com.
Visit this group at
https://groups.google.com/group/tlaplus.
For more options, visit
https://groups.google.com/d/optout.