Apparent bug in operators using \E

[Michael Collins]

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)

[loki der quaeler]

On first blush, i'm not so sure this is a bug. It seems like you are treating state = v like an assignment (like one would do with a programming language) and not an atomic logical evaluation, and so, if that is true, your spec is expecting state to have the value of v when evaluating the conjunct state > 0.

In that bounded expression though, the model-state for an evaluation (not involving next states) is simultaneous; so state (an unfortunately named variable for this sentence) should be thought of as simultaneously being evaluated equal to v and greater than 0 - not set equal to v and then whether it is greater than 0.

(Though i'd appreciate confirmation or correction from Leslie or Markus.)

[Leslie Lamport]

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:

[Markus Alexander Kuppe]

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