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

*From*: Guo Hua <fchdir@xxxxxxxxx>*Date*: Tue, 12 Dec 2023 09:04:59 -0800 (PST)*References*: <0587c5ac-dabc-42d1-9914-e96b3e43b0c3n@googlegroups.com> <0856582c-74af-43c7-bb30-acdefaf2b590n@googlegroups.com> <e3dfaa78-3d81-4463-8fdd-afc213c62c30n@googlegroups.com> <58808b68-abcf-4078-9594-7046cb225f86n@googlegroups.com> <1EEE058A-8DA2-446D-A0B4-26F53671FEA6@lemmster.de>

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.

**Follow-Ups**:

**References**:**[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?***From:*Guo Hua

**[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?***From:*Guo Hua

**[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?***From:*Andrew Helwer

**[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?***From:*Guo Hua

**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?***From:*Markus Kuppe

- Prev by Date:
**[tlaplus] Does TLC handle <> and ~[]~ differently?** - Next by Date:
**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?** - Previous by thread:
**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?** - Next by thread:
- Index(es):