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