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