Hi,
I'm trying to specify "If some operation does not happens, then some condition eventually becomes true"
full specification is following:
-------------------------------- MODULE test --------------------------------
EXTENDS Integers
VARIABLE x,y
Init ==
/\ x = 0
/\ y = 0
IncX ==
/\ x' = IF x < 5 THEN (x + 1) ELSE 5
/\ UNCHANGED <<y>>
IncY ==
/\ x > 0
/\ y' = IF y < 5 THEN (y + 1) ELSE 5
/\ UNCHANGED <<x>>
SetX ==
/\ x' = -1
/\ UNCHANGED <<y>>
Next ==
\/ IncX
\/ IncY
\/ SetX
Invariant1 ==
/\ x < 6
/\ y < 6
temporalFormula1 == (x > 0) ~> (y = 5)
=============================================================================
and behavior spec is:
Init /\ [][Next]_<<x,y>> /\ WF_x(IncX) /\ WF_x(SetX) /\ WF_<<x,y>>(IncY)
my question is, why temporalFormula1 is violated?
I know that (x > 0) ~> (y = 5) means:
□((x > 0) => <>(y = 5)) which is
\A n \in Nat. \sigma^{+n} ⊨ (x > 0) => ¬□¬(y = 5) which is
\A n \in Nat. \sigma^{+n} ⊨ (x > 0) => \sigma^{+n} ⊨ \E m \in Nat. \sigma{+m} ⊨ (y = 5) which is
\A n \in Nat. \sigma^{+n} ⊨ (x > 0) => \E m \in Nat. \sigma^{+n+m} ⊨ (y = 5)
so, i believed that error-trace should not contains the state that x is -1 but it does.
I even tried the formula (FALSE) ~> (y = 5) but it still fails with similar error trace. what's my mistake here?
