Here's my attempt:
---- MODULE Test ----
EXTENDS TLC
VARIABLES a, b, c
Vars == <<a, b, c>>
TypeOK ==
/\ a \in BOOLEAN
/\ b \in BOOLEAN
/\ c \in BOOLEAN
GeneratesNewState == Vars' /= Vars
SomeAction(msg) == Print(msg, TRUE)
Action1 == UNCHANGED Vars
Action2 ==
/\ a' = ~a
/\ b' = ~b
/\ c' = ~c
Init ==
/\ a = TRUE
/\ b = TRUE
/\ c = TRUE
Next ==
\/ /\ Action1
/\ GeneratesNewState => SomeAction("Action1")
\/ /\ Action2
/\ GeneratesNewState => SomeAction("Action2")
Spec ==
/\ Init
/\ [][Next]_Vars
====
If you run TLC on this it will print "Action2" but never "Action1". Note how the prime operator distributes over the variables in Vars; a neat feature!
Andrew
On Sunday, December 3, 2023 at 2:41:35 AM UTC-5 Guo Hua wrote:
Also, I thought, can I simply achieve this by adding OperatorX to Invariants?
On Sunday, December 3, 2023 at 3:00:17 PM UTC+8 Guo Hua wrote:
Does TLA+ have a feature where a certain operator is true if and only if a new, different state is produced in the next action?
If
there are no built-in features like this, could I write new overriding
operators or modules to implement this? I need some tips.
Just like in the following example,
OperatorX is true if and only if Next produces a new state. In this
case, OperatorX cannot change the state and does not have prime
operators.
Next ==
/\ (\/ Next1
\/ Next2)
/\ (NextCanProduceNewState => OperatorX )
Thanks
Hua