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

*From*: Victor Clayton Barnett <vcbarnett93@xxxxxxxxx>*Date*: Wed, 13 Jul 2022 07:40:11 -0700 (PDT)

Hi,

I am trying to learn TLA+ as a Computer Engineering undergrad. I am reading the safety and liveness document from the TLA+ website and am trying to understand the definition of:

<<A>>_v = A /\ (v' \= v)

and when it is enabled. When I first read the definition, it seems this would be ENABLED in a behaviour specified by a formula S when there is a step allowed by S that satisfies:

A /\ (v' \= v).

But then this example is provided:

However, WF_v(A) and SF_v(A) need not be fairness properties. For example, let S equal (x=0) /\ [][x’=x+1]_x,

let A equal x’=x+2

and let v equal x.

An <<x’=x+2>>_x step is possible in any reachable state of S , but no such step satisfies x’=x+1. (A reachable state of S is one that occurs in some behavior that satisfies S .) Hence, no finite sequence of states satisfying S can be extended to satisfy S as well as WF_v(A) or SF_v(A).

So in this case, he's saying that <<x’=x+2>>_x is enabled in any state of a behavior satisfying S because a <<x’=x+2>>_x step is 'possible' in any state of S, but it is not a fairness property essentially because it's not actually allowed within the confines of S. What does possible mean in this case?

Thank you,

Victor

-- 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/befc81a6-d74d-4c08-ae5d-2fc6a18d53cbn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Simple Question - Safety and Liveness***From:*Stephan Merz

**[tlaplus] Re: Simple Question - Safety and Liveness***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Re: Hidden variables (via existential quantifier bold-∃)** - Next by Date:
**[tlaplus] EOL/EOVS dates of v1.7.2** - Previous by thread:
**[tlaplus] Re: Hidden variables (via existential quantifier bold-∃)** - Next by thread:
**[tlaplus] Re: Simple Question - Safety and Liveness** - Index(es):