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

[tlaplus] Why does TLC find two initial states?



When I run TLC on my spec, the Model Checking Results page shows that the Init action occurred twice. But I think that Init specifies a unique initial state:

Init ==
  /\ depth_limit = 2
  /\ node_stack = Push( EMPTY, Start )
  /\ edges_tried = 0
  /\ deque = EMPTY
  /\ progress_stack = Push( EMPTY, FALSE )
  /\ deadend = {}
  /\ done = {}

(The model defines Start to be “a1”.) Why does the Init action occur twice?



--
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/B1349735-9A2F-4C4E-9219-49B2D9BEFC43%40RyanLeonard.us.