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

*From*: seup yun <syun4541@xxxxxxxxx>*Date*: Sat, 10 Apr 2021 09:55:45 -0700 (PDT)*Ironport-hdrordr*: A9a23:kUjvM65Q1yJ+pRCqtAPXwA7XdLJzesId70hD6mlaTxtJfsuE0/2/hfhz726XtB89UGwt8OruBICuWnXZnKQa3aA0HZOPGDbro3GpKoYK1/qA/xTFFzfl/uBQkYdMGpIeNPTKAVJ3jdn37WCDer5K/PC87Kuqie3Cpk0BcShWbchbhTtRO0K+Gk1ySBIuP/oEPavZ3+t/4xy6eXoWacynBn4KG9LIvN3TifvdDSI7Ow==

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)

=============================================================================

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:

\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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ca126b11-a19f-4cb2-b67c-fcd9df861299n%40googlegroups.com.

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

- Prev by Date:
**[tlaplus] Re: How to solve this error ?** - Next by Date:
**Re: [tlaplus] meaning of the lead to (~>) operator** - Previous by thread:
**[tlaplus] Re: How to solve this error ?** - Next by thread:
**Re: [tlaplus] meaning of the lead to (~>) operator** - Index(es):