[tlaplus] A simple (distinct) states question

[jack malkovick <sillymouse333@xxxxxxxxx>]

I have this very simple spec

EXTENDS TLC
VARIABLES v
vars == << v >>
Init == v = "A" /\ PrintT("A")
SetV ==
     /\ v' = "B"
     /\ IF v' = "B" THEN PrintT("B") ELSE TRUE
Spec == Init /\ [][SetV]_vars /\ WF_vars(SetV)

If I model check it in TLA Toolbox, I get 

1 state found for action Init and 2 states found for action SetV

for a total of 3 states but 2 distinct ones.

The output is also "A", "B", "B". Why two "B"s? Why 2 identical states?

-- 
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/61933610-d4ee-46a2-aa35-ebd0f3ed1eb0n%40googlegroups.com.