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

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?

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


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

> On Dec 8, 2023, at 3:31 AM, Guo Hua <fchdir@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/1EEE058A-8DA2-446D-A0B4-26F53671FEA6%40lemmster.de.