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