meaning of the lead to (~>) operator

[seup yun]

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?

[Isaac DeFrain]

Hello Seup,

What is the error trace you're getting?

From the actions you have defined, as long as x remains <= 0, we never need to increment y. A possible behavior is Init, SetX, IncX, SetX, IncX, ...

It may be enough to simply change the enabling condition for IncY to x >= 0 (but that may not be "allowed" by what you are trying to specify).

Best,

Isaac DeFrain

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ca126b11-a19f-4cb2-b67c-fcd9df861299n%40googlegroups.com.

[seup yun]

here is the error trace i'm getting when using the formula (x > 0) ~> (y = 5)

and when using the fomrula (FALSE) ~> (y = 5)

I don't understand why these formulas even causes the error, what am i missing? why mplication operator evaluated as false when left operand of the implication is FALSE?

 

2021년 4월 11일 일요일 오전 3시 22분 22초 UTC+9에 isaacd...@gmail.com님이 작성:

[Calvin Loncaric]

The (FALSE) ~> (y = 5) case looks like a bug to me! I was able to reproduce it in a very simplified example on my own computer. It is either a bug or we have both deeply misunderstood the ~> operator.

The trace you showed for the (x > 0) ~> (y = 5) case does not look like a bug. It looks like a true counterexample to me. In the trace, there is a state where x>0 (e.g. state 2) and that state is not followed by a later state where y=5. Therefore, x>0 does not always lead to y=5. The property is indeed violated.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c46bd513-edfa-41cf-aca1-00b4aa3e669fn%40googlegroups.com.

[Hillel Wayne]

For (x > 0) ~> (y = 5),  x is set to 1 in state 2, meaning y = 5 must be true in a future state from 2. The error trace includes the step where x = -1 due to an implementation detail of TLC: based on how it calculates liveness, it doesn't guarantee that a liveness-violating trace will be the shortest one possible.

Re the FALSE ~> (y = 5),  no idea. Think it might be a bug? [](FALSE => <>TRUE) also fails, which doesn't seem right.

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c46bd513-edfa-41cf-aca1-00b4aa3e669fn%40googlegroups.com.

[Isaac DeFrain]

Okay so I clearly misinterpreted the original question... my apologies.

I now understand the issue you are encountering, Seup, as I am also encountering the same issue with ~> in a spec. This must be a bug in TLC.

Best,

Isaac DeFrain

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/84c27c0d-ecc1-7b8d-13c6-32bd48f81a07%40gmail.com.

[Markus Kuppe]

On 14.04.21 11:14, Isaac DeFrain wrote:
> I now understand the issue you are encountering, Seup, as I am also
> encountering the same issue with ~> in a spec. This must be a bug in TLC.

https://github.com/tlaplus/tlaplus/issues/604

Markus

[Isaac DeFrain]

Great! Thanks, Markus.

Isaac DeFrain

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/531db585-55d1-b729-0961-8c0d1877d8d4%40lemmster.de.

[Isaac DeFrain]

Is there a gauge on how widespread this issue is? The ~> operator seems to work as expected with some state predicates and not others...

Isaac DeFrain

[Markus Kuppe]

On 14.04.21 11:33, Isaac DeFrain wrote:
> Is there a gauge on how widespread this issue is? The ~> operator seems
> to work as expected with some state predicates and not others...

Please add any details you have to the Github issue.

Markus