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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Mon, 4 Dec 2023 11:00:47 -0800*References*: <bb7d6e3f-6731-4b08-bb7d-717df3834e4fn@googlegroups.com>

Perhaps, ENALBED Next is what you are looking. M. > On Dec 2, 2023, at 10:58 PM, Guo Hua <fchdir@xxxxxxxxx> 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 > > > -- > 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/bb7d6e3f-6731-4b08-bb7d-717df3834e4fn%40googlegroups.com. -- 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/74B1A8F5-B43C-44A4-98BC-3D72C94D734D%40lemmster.de.

**References**:

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