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

*From*: Guo Hua <fchdir@xxxxxxxxx>*Date*: Sat, 2 Dec 2023 23:41:35 -0800 (PST)*References*: <0587c5ac-dabc-42d1-9914-e96b3e43b0c3n@googlegroups.com>

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/0856582c-74af-43c7-bb30-acdefaf2b590n%40googlegroups.com.

**Follow-Ups**:

**References**:

- Prev by Date:
**[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?** - Next 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?** - Previous by thread:
**[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?** - Next 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?** - Index(es):