InitOp(state) == /\ \E v \in 0..1 : state = v
/\ state = b
/\ PrintT(<<state, b>>)
<<0, 0>>
<<0, 1>>
This is a strange and subtle bug, as shown by the following. If the definition of InitOp is changed to
InitOp(state) == /\ \E v \in 0..1 : state = v
/\ state = b
/\ PrintT(<<state, b>>)
(and the TLC module is added to the EXTENDS statement), then TLC finds the expected two initial states, but the PrintT statement prints
<<0, 0>>
<<0, 1>>
Moreover if the third line of the definition is replaced by "b = state", then only one initial state is found and the PrintT statement prints only <<0,0>>.
The semantics of TLA+ state that InitOp(b) should mean the formula obtained by simply substituting "b" for "state" in the right-hand side of the definition. However, TLC is doing that substitution in only some places. In other places it seems to be substituting the first value of b that it finds for "state".
I would expect the same problem to arise in computing the next-state relation, but I haven't been able to find it.
Hi Leslie,
the next-state relation doesn't seem to exhibit the same bug because Tool#getInitStates and Tool#getNextStates - while being similar in concept - don't share much code.
By the way, I created an issue [1] to work on a fix.
Thanks
Markus