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.