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

# Re: [tlaplus] Re: Apparent bug in operators using \E

 On 09.11.2017 20:04, Leslie Lamport wrote: 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(<>) (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