TLC Outputs
Casey Richardson
Hillel Wayne
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
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7cfa6da6-fa39-410a-893d-1f78abca7542n%40googlegroups.com.
