Re: [tlaplus] States Found vs Distinct States

[Stephan Merz <stepha...@xxxxxxxxx>]

Hi Jaak,

the number of "generated states" indicates the number of states that TLC has computed so far (as initial states or as successors of previously generated states). Since the same state may be the successor of different states, this number is bigger than the number of distinct states. The latter indicates the real size of your state space, the former gives you an idea of how different the state space is from a tree.

Best,
Stephan

> On 08 Oct 2015, at 13:43, Jaak Ristioja <jaak.r...@xxxxxxxx> wrote:
> 
> Hi!
> 
> TLC progress report messages contains the number of states generated and
> the number of distinct states found. Have I correctly assumed that the
> latter to signifies the size of the set of different values-to-VARIABLES
> assignments that TLC has encountered this far. But what exactly does the
> value of "generated states" count and what is this value useful for?
> 
> Best Regards,
> Jaak Ristioja
> 
> -- 
> 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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.