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
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.
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.