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

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.

(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:

----------------- 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.