RE: [tlaplus] modeling resets

[RESCH Stefan <stefan...@xxxxxxxxxxxxxxx>]

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

From: tla...@xxxxxxxxxxxxxxxx [mailto:tla...@xxxxxxxxxxxxxxxx] On Behalf Of Brian
Sent: Donnerstag, 12. Mai 2016 17:50
To: tla...@xxxxxxxxxxxxxxxx
Subject: [tlaplus] modeling resets

I've modeled a reader process and a writer process using PlusCal, and they
communicate via some global state.

I'd like to model a reset event (such as a power failure) in which, regardless
of its current state, each process is reset back to its initial state.
Some global state would be reset as well, but some global state is persistent
and survives the reset.

I was imagining something similar to the LoseMsg process in the ABProtocol
algorithm example, but I'm not sure how to reset the other processes.

Is there an example of something like this, or any ideas on how I might achieve
it?


Thanks!
Brian

-- 
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.