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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Mon, 6 Jan 2020 09:46:28 -0800*References*: <d389f4b8-f1f2-4227-ba0f-22394e491e95@googlegroups.com>

On 06.01.20 07:47, amin wrote: > I was wondering how to interpret a zero in "Distinct States" of an > action, especially with a large number of "Found States", e.g. as seen > below: > > To my understanding, those actions are very much enabled, but I'm not > sure what could result in zero distinct states. Hi Amin, an action with zero distinct states is one that didn't "produce" unseen states when evaluated by TLC. Consider the following spec with state constraint x \in -3..3: ---- MODULE Counter ---- EXTENDS Integers VARIABLES x Init == x = 1 B == x' = x + 1 A == x' = x + 1 Next == A \/ B ============ When TLC evaluates Next with x = 1, both sub-actions A and B evaluate to x' = 2. Consequently, the number of "Found States" is incremented for both sub-actions. However, the number of "Distinct States" is only incremented for one of them. In this spec, zero distinct states could suggest the removal of either sub-action A or B (to speed up model-checking). On the other hand, it might indicate a typo and you actually meant to write x' = x - 1 in sub-action A. In other specs, it can be perfectly fine for an action to have zero distinct states. One example would be the Terminating sub-action of a PlusCal algorithm. You can read more about the profiler in section 2.3.3 of https://arxiv.org/abs/1912.10633. Hope this helps, Markus -- 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/7f70c5f5-2c97-567e-90ae-b6135b18f411%40lemmster.de.

**References**:

- Prev by Date:
**[tlaplus] Zero Distinct States in TLC results?** - Next by Date:
**Re: [tlaplus] TLA+, Event B comparison** - Previous by thread:
**[tlaplus] Zero Distinct States in TLC results?** - Next by thread:
**[tlaplus] Modelling network partitions explicitly** - Index(es):