Re: Apparent bug in operators using \E

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.

Leslie

On Wednesday, November 8, 2017 at 8:35:02 AM UTC-8, Michael Collins wrote:

This appears to be a bug: given a spec like

---------------------------- MODULE
EXTENDS Integers

VARIABLE b

InitOp(state) == \E v \in 0..1 : (state = v /\ state > 0)

Init == InitOp(b)
Next == (*whatever*)

Spec == Init /\ [][Next]_b /\ WF_b(Next)

===================================

The TLC model checker does not find any initial states. We do get the expected initial state [b=1] if we instead define

InitOp(state) == \E v \in 0..1 : (state = v /\ v > 0)

More generally, if S is some finite set, and Predicate(CHOOSE e \in S : TRUE) is false, the model checker fails to find any initial states with

InitOp(state) == \E v \in S : (state = v /\ Predicate(state))

Furthermore, if Predicate(CHOOSE e \in S : TRUE) is true, this generates initial states with b equal to every member of S, even those for which Predicate is false.

We get the expected initial states with

InitOp(state) == \E v \in S : (state = v /\ Predicate(v))

(same behavior on Ubuntu, Mac, and Windows)