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

*From*: Guo Hua <fchdir@xxxxxxxxx>*Date*: Sat, 2 Dec 2023 23:00:17 -0800 (PST)

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,

/\ (\/ Next1

\/ Next2)

/\ (NextCanProduceNewState => OperatorX )

Thanks

Hua

-- 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/0587c5ac-dabc-42d1-9914-e96b3e43b0c3n%40googlegroups.com.

**Follow-Ups**:

- Prev by Date:
**[tlaplus] Does TLA+ have a feature where a certain operator is true if and only if when 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:
**Re: [tlaplus] Does TLA+ have a feature where a certain operator is true if and only if when 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):