On Sat, Apr 10, 2021 at 3:31 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:
--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
On 4/10/2021 2:41 PM, seup yun wrote:
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...@xxxxxxxxx님이 작성:
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
On Sat, Apr 10, 2021 at 10:56 AM seup yun <syun...@xxxxxxxxx> wrote:
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?
--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ca126b11-a19f-4cb2-b67c-fcd9df861299n%40googlegroups.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c46bd513-edfa-41cf-aca1-00b4aa3e669fn%40googlegroups.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/84c27c0d-ecc1-7b8d-13c6-32bd48f81a07%40gmail.com.