fair process Firmware = 0
begin
Reset:
\* do some stuff
Step0:
\* do some more stuff
Step1:
\* do even more stuff
...
But I want it to be possible to transition from any StepN to Reset (without changing any variables). I can write it explicitly like this:
fair process Firmware = 0
begin
Reset:
\* do some stuff
either goto Reset; or goto Step0; end either;
Step0:
\* do some more stuff
either goto Reset; or goto Step1; end either;
Step1:
\* do even more stuff
either goto Reset; or goto Step2; end either;
...
This seems to work but is very tedious. Is there a less tedious way? It seems like the generated TLA+ formula is:
Firmware == Reset \/ Step0 \/ Step1
So I think I could just add another one in there like:
Firmware == Reset \/ Step0 \/ Step1 \/ GotoReset
GotoReset == /\ pc' = [pc EXCEPT ![0] = "Reset"]
/\ UNCHANGED << ...all the variables... >>
I'm pretty sure that works out. But since that code is the generated TLA+ from PlusCal I'm not sure how to modify the generation so it does that instead.