You should almost always ignore the total number of states
(3). It is affected by lots of factors and can change from run
to run on the same input spec. Only the number of distinct
states (2) really matters.
The more interesting question is why you saw two "B"s!
The model checker does not just visit every reachable state;
it also visits every reachable action. Your spec has
two reachable states:
v="A"
v="B"
...and two reachable actions:
v="A" ---[SetV]---> v="B"
v="B" ---[SetV]---> v="B"
Yes, the second one is indeed a legal action, even though it
doesn't change any of the variables! I suspect the second "B"
is the result of the second possible action, where v does not
change.
To see this in action, add "/\ v' /= v" to the definition
of SetV before the PrintT call, thus requiring it to change
the value of v. The second "B" should go away.
One final warning: the PrintT calls happen while the model
checker is exploring. The model checker promises to explore
everything, but it doesn't really promise anything about what
order it explores things or how many times it visits them. If
you use multiple threads, two different threads might visit
the same action in parallel, and you will get duplicated
outputs. So while there is a good explanation for the two "B"s
in this simple case, you shouldn't necessarily rely on PrintT
to behave how you expect it does in a real programming
language.
--
Calvin
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.
--