[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How to implement a global reset?



Hi,

As a rule, specifications don't "compose" well and can't be easily modularized. This is true of all specification languages. With that in mind, I'd write a new top level Next:

Next ==
  \/ (A_Next /\ UNCHANGED not_A_vars)
  \/ (B_Next /\ UNCHANGED not_B_vars)
  \/ ...
  \/ (A_reset /\ B_reset /\ ...)

This will also be easier to check, as A_spec /\ B_spec contains two box-action formula and cannot be checked by TLC.

H

On 3/5/2021 11:49 AM, ns wrote:
(This isn't so much a question but my sharing my thoughts on a problem I encountered. Feedback on this is definitely welcome!)

Suppose I have a "reset" signal that is common to several modules A,B,C, etc. That is, when the reset is asserted in some top level module Sys, each module responds to that reset in its own way. What is the best way to write this in TLA+? One approach that came to mind is to do the following:

1.
----------------- MODULE A ----------------
A_Next == ...
A_Reset == ...
A_ResetOrNext == \E reset \in BOOLEAN: IF reset THEN A_Reset ELSE A_Next
ASpec == A_Init /\ [][A_ResetOrNext]_Avars
================================================

Every such spec, BSpec, CSpec, etc would have a very similar structure

Then they would be used in the following way in some grand top level spec

----------------- MODULE Sys ----------------
EXTENDS A,B
Spec == ASpec /\ BSpec  /\ ..

However, this way of specifying the problem allows each module to perform a reset at any time independent of what the other module does. Whereas I want one global reset signal.

2. An alternative I thought of is to declare a variable reset in each module,

----------------- MODULE A ----------------
VARIABLE reset
A_Next == ... /\ UNCHANGED reset
A_Reset == ... /\ reset'=FALSE
A_ResetOrNext == IF reset THEN A_Reset ELSE A_Next
A_Init == ... /\ reset=FALSE
ASpec == A_Init /\ [][A_ResetOrNext]_Avars
================================================

Then  I would instance each module in the system and now every module would have the common reset signal.

----------------- MODULE Sys ----------------
VARIABLES reset
INSTANCE A,B
Spec == ASpec /\ BSpec  /\ ..

The problem now however is the A_Init and A_Reset actions are having to make a local decision about what is essentially a global variable (eg. they must all be sure to turn off reset after responding) shown in blue above. Sys would also need duplicate vars for all the other vars in A, B, ...

3. I think the best solution is a variant on the first, but to make reset an argument 

----------------- MODULE A ----------------
...
A_ResetOrNext(reset) == IF reset THEN A_Reset ELSE A_Next
ASpec(reset) == A_Init /\ [][A_ResetOrNext(reset)]_Avars
...

Then the system that uses A would write
----------------- MODULE Sys ----------------
VARIABLE reset
EXTENDS A,B
Spec == ASpec(reset) /\ BSpec(reset) /\ ..

Its also possible I'm missing a more obvious or cleaner solution. Any thoughts? 
thanks


--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/d845b8cb-7220-4090-95dd-a0198ceea8fdn%40googlegroups.com.

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/48e6d600-6be1-4fad-eca7-3f39c29b7f88%40gmail.com.