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

Re: [tlaplus] TLC Outputs



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:


Capture.PNG
--
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/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/9c565f90-1b93-48f9-842c-82e633a9745c%40gmail.com.