[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(<<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

[1] https://github.com/tlaplus/tlaplus/issues/113