Zero Distinct States in TLC results?

[amin]

Hello,

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.

Thanks,

amin

[Markus Kuppe]

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