alternative to action composition?

[Sebastian Hunt]

In one aspect of the spec I'm developing I thought action composition (\cdot) was the right thing to use.

The system (simplified) includes state variables: value, range, mode. We aim to maintain an invariant:

SafeMode == mode = "closed" => inRange(value, range)

A Measure action changes value, a SetRange action changes range. In each case, if the change would violate the invariant, the mode should be changed from "closed" to "open" (in the actual spec the range check is a bit more complex, since other parts of the state may also be changed, depending on whether the value is too high or too low). My instinct is that the range check should be specified just once and reused. Using action composition I thought I would do something like this:

RangeCheck ==

  \/ /\ mode = "closed"

     /\ mode' = IF inRange(value, range) THEN mode ELSE "open"

     /\ UNCHANGED <<value, range>>

  \/ /\ mode = "open"

     /\ UNCHANGED <<value, range, mode>>

Measure == value' \in Measurement /\ UNCHANGED <<range, mode>>

SetRange == range' \in Range /\ UNCHANGED <<value, mode>>

Next == (Measure \cdot RangeCheck) \/ (SetRange \cdot RangeCheck) \/ ...

Since action composition is not currently supported by TLC I'm looking for an alternative. Perhaps there is an idiom which achieves something similar? Or perhaps there is a better way to look at the problem and action composition is a red herring? Any advice would be very welcome.

Seb

[Stephan Merz]

From the excerpts of your spec, it looks like only RangeCheck changes mode (btw, mode never seems to be reset to "closed") whereas the other actions change value and range. If this is so, you could just use conjunction, omitting the conjuncts leaving value and range unchanged in the definition of RangeCheck and reciprocally for mode in the other actions? Concretely,

RangeCheck ==
  \/ /\ mode = "closed"

     /\ mode' = IF inRange(value', range') THEN mode ELSE "open"

  \/ /\ mode = "open"

     /\ UNCHANGED mode

[...]

Next == (Measure /\ RangeCheck) \/ (SetRange /\ RangeCheck) \/ ...

Regards,

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

[Sebastian Hunt]

Thank you, yes, this works. I'm not sure why I thought it wouldn't. Probably because I am thinking too procedurally. (Though it seems you do have to think a *bit* procedurally, in that TLC is sensitive to the order of conjuncts. As I discovered just now when I tried to include RangeCheck as a conjunct before the UNCHANGED conjuncts in the Measure and SetRange actions).

(mode is set to "closed" by other actions in the full spec).

Seb