Adding raw TLA+ to PlusCal process states

[Tim Hutt]

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!

[Tim Hutt]

Ah I ended up just adding `FirmwareWithReset == Firmware \/ GotoReset`, plus `SpecWithReset`, `NextWithReset` and `TerminationWithReset` copy & pasted from the generated ones. Maybe there's a better way but this seems to work ok.

[Stephan Merz]

The PlusCal structure that you suggest is perhaps not so tedious to write if you define a suitable macro that encapsulates the either … or?

Stephan

--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/d1c2315d-2560-470a-8d6b-6302ae683257n%40googlegroups.com.

[Hillel Wayne]

I don't recall if you can put a `goto` inside a macro, but if you could, you could do `either goto Reset or skip end either;`
H

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/621A6035-786C-475D-A895-5CE5897F8DAC%40gmail.com.