Hi, I'm trying to model a CPU program that can be reset at any point. This seems suitable for PlusCal. I want this:
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.
Is there a way to add a raw TLA+ step into a PlusCal process?
Cheers,
Tim
PS: It's my first time writing TLA+, if that wasn't obvious!
--
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 visit
https://groups.google.com/d/msgid/tlaplus/d1c2315d-2560-470a-8d6b-6302ae683257n%40googlegroups.com.