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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Sat, 10 Apr 2021 16:31:47 -0500*Ironport-hdrordr*: A9a23:U13hC6pJwQnmjkG0SIW+eMUaV5ojeYIsi2QD101hICF9X8SEm6mV8Mgz+gTzjF8qNU0IvdybIqGPTTf9+PdOj7U5BrupUAn4tGbAFugLhrfK+SHqGCH164dmuptITq4WMrfNMWQ=*References*: <ca126b11-a19f-4cb2-b67c-fcd9df861299n@googlegroups.com> <CAM3xQxH4BdebG+fYKYN4XokHabKazhRRYS1TzGRWv81+OS0Pnw@mail.gmail.com> <c46bd513-edfa-41cf-aca1-00b4aa3e669fn@googlegroups.com>*User-agent*: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.9.1

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.

**Follow-Ups**:**Re: [tlaplus] meaning of the lead to (~>) operator***From:*Isaac DeFrain

**References**:**[tlaplus] meaning of the lead to (~>) operator***From:*seup yun

**Re: [tlaplus] meaning of the lead to (~>) operator***From:*Isaac DeFrain

**Re: [tlaplus] meaning of the lead to (~>) operator***From:*seup yun

- Prev by Date:
**Re: [tlaplus] meaning of the lead to (~>) operator** - Next by Date:
**[tlaplus] Proving refinement for specs with fairness properties** - Previous by thread:
**Re: [tlaplus] meaning of the lead to (~>) operator** - Next by thread:
**Re: [tlaplus] meaning of the lead to (~>) operator** - Index(es):