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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 25 Jul 2016 14:44:05 -0700 (PDT)*References*: <dfaeacbc-77e2-4366-b9fe-ccf1b9151f58@googlegroups.com>

Andrew didn't notice that the conjunct

/\ ~has_entry(store', path)

is not "somewhat superfluous". It is completely superfluous because

it's implied by the preceding conjunct

/\ store' = [p \in (DOMAIN store \ path) |-> store[p]]

and the definition of has_entry. More precisely, it would if you had

written that preceding conjunct correctly. I don't remember what the

precedence of the operators is, so I don't know how

DOMAIN store \ path

is parsed. I presume you meant to write

DOMAIN (store \ path)

But S \ T is the set of elements in S but not in T, so the _expression_

you wanted is

DOMAIN (store \ {path})

To give you a more general answer, the next-state relation specifies

the new values of variables. A postcondition is a condition that

should hold on the values of the new variables. It should be implied

by the next-state relation and whatever precondition you assume about

the old values of the variables. As Andrew pointed out, sometimes you

can make the desired postcondition a conjunct of an action to rule out

some possible new values of variables that the rest of the action

allow.

----

TLC will check if a formula Inv is an invariant of the specification,

meaning that Inv is true on all reachable states. If you want to

put the assertion that Inv is an invariant in the specification, you

can write

THEOREM Spec => []Inv

where Spec is the TLA+ temporal formula that constitutes the

system's specification. However, TLC does not check THEOREMs.

----

As Andrew indicated, if you want to add a concept of time to your

spec, you should add a variable that represents a clock. If you want

your specification to model real time, see my article "Real Time is

Really Simple" at

http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#real-simple

You need real time if you are interested in properties such as "if X

happens then Y happens within 5 seconds". However, if you just need

properties such as "if X happens then Y eventually happens", then you

don't want to introduce time. You should instead learn about temporal

logic, liveness, and fairness--e.g., in Chapter 8 of "Specifying Systems".

Leslie

**References**:**Any examples of a specification of an S3-like object store API?***From:*Steve Loughran

- Prev by Date:
**Next-state involving existential quantifier using PlusCal?** - Next by Date:
**Re: Next-state involving existential quantifier using PlusCal?** - Previous by thread:
**Re: [tlaplus] Re: Any examples of a specification of an S3-like object store API?** - Next by thread:
**specify some action eventually will never happen** - Index(es):