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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Fri, 9 Feb 2024 08:19:58 -0800 (PST)*References*: <7cfa6da6-fa39-410a-893d-1f78abca7542n@googlegroups.com> <9c565f90-1b93-48f9-842c-82e633a9745c@gmail.com> <289a4211-e214-4684-9799-238a9fd06ca9n@googlegroups.com>

I think you can also view (3) as the number of state transitions in your system (probably off by one).

Andrew

On Friday, February 9, 2024 at 8:31:14 AM UTC-5 Casey Richardson wrote:

Thank you for the pointer, somehow I missed this on the learntla site (which has been very helpful as a learning resource btw)On Thursday, February 8, 2024 at 3:17:26 PM UTC-5 Hillel Wayne wrote:Hi Casey,

I wrote a description of them on learntla. From there:

> 1. Since complicated models can take a long time to check, the “state space progress” tab updates roughly once a minute.

>

> 2. Diameter is the length of the longest behavior. If TLC found a thousand behaviors with length 2 and one with length 20, the diameter will be reported as 20.

>

> 3. States found is how many system states the model checker has explored. This includes duplicate states the checker found in different paths.

>

> 4. The number of _unique_ states found.

>

> 5. How many states TLC knows _for certain_ it’ll have to check. Some of these states will add more states to check, and so on and so forth.

>

> 6. TLC stores explored states as hashes, this is the chance that there’s a hash collision. In practice this never goes above one in a million billion and can be ignored.

>

> 7. How often each label was run and how many states that lead to. If one label has 0 states then there’s probably a bug in your spec.

H

On 2/8/2024 12:20 PM, Casey Richardson wrote:

Hi, apologies if this has been asked before, can someone point me to a description of the TLC outputs, what they mean. For example, "queue", "distinct", "diameter", etc., found in the VS Code extension output:

--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7cfa6da6-fa39-410a-893d-1f78abca7542n%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/879314cd-59d5-4b8f-bcf7-e5bcdbe9924fn%40googlegroups.com.

**References**:**[tlaplus] TLC Outputs***From:*Casey Richardson

**Re: [tlaplus] TLC Outputs***From:*Hillel Wayne

**Re: [tlaplus] TLC Outputs***From:*Casey Richardson

- Prev by Date:
**Re: [tlaplus] TLC Outputs** - Next by Date:
**[tlaplus] Open an existing spec - does it work in the TLA+ Toolbox?** - Previous by thread:
**Re: [tlaplus] TLC Outputs** - Next by thread:
**[tlaplus] Open an existing spec - does it work in the TLA+ Toolbox?** - Index(es):