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

*From*: Michael Collins <mjcol...@xxxxxxxxx>*Date*: Wed, 8 Nov 2017 08:35:02 -0800 (PST)

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)

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

**Follow-Ups**:**Re: Apparent bug in operators using \E***From:*Leslie Lamport

**Re: Apparent bug in operators using \E***From:*loki der quaeler

- Prev by Date:
**Re: [tlaplus] Re: Login required for TLA toolbox?** - Next by Date:
**Re: Why Amazon Chose TLA+** - Previous by thread:
**Re: [tlaplus] Re: Login required for TLA toolbox?** - Next by thread:
**Re: Apparent bug in operators using \E** - Index(es):