Re: [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?

[Akash <akash.gopkrish@xxxxxxxxx>]

I'm a beginner to TLA+, so I may be wrong, but, I think you are referring to "leads to" in temporal logic.

F squiggly arrow G.

If F is true then eventually G must be true. 

Then you can apply this concept to your operator and make it nested.

Kind regards,

Akash

On Tue, Dec 12, 2023, 12:05 PM Guo Hua <fchdir@xxxxxxxxx> wrote:

Thank you for your reply.  I got it.

On Saturday, December 9, 2023 at 1:03:02 AM UTC+8 Markus Kuppe wrote:

TLC exposes TLCGet(“distinct”) among other statistics [1].

Markus

[1] https://lamport.azurewebsites.net/tla/current-tools.pdf

> On Dec 8, 2023, at 3:31 AM, Guo Hua <fch...@xxxxxxxxx> wrote:
>
> However, I am sorry for not describing it clearly.
> What I said was "generating distinct new states in the entire search space of TLC model checking", rather than "not changing the value of variables".
>

--
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/abdbce77-89f5-4964-8151-75946c390b37n%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/CAFZmCwD222at7Y0A_kyLaRF%3DwCSiT6-ZBEahP571Z3RH%2BqwhQw%40mail.gmail.com.