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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Sun, 3 Dec 2023 06:26:30 -0800 (PST)*References*: <0587c5ac-dabc-42d1-9914-e96b3e43b0c3n@googlegroups.com> <0856582c-74af-43c7-bb30-acdefaf2b590n@googlegroups.com>

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

====

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 )ThanksHua

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/e3dfaa78-3d81-4463-8fdd-afc213c62c30n%40googlegroups.com.

**Follow-Ups**:

**References**:**[tlaplus] 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?***From:*Guo Hua

**[tlaplus] Re: 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?***From:*Guo Hua

- Prev by Date:
**[tlaplus] Re: 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?** - Next by Date:
**[tlaplus] TLA Toolbox hang on startup** - Previous by thread:
**[tlaplus] Re: 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?** - Next by thread:
- Index(es):