Proving an action leads to a temporal formula

[Dylan Zueck]

I have written my spec and I want to prove using TLAPS that if a specific action ever happens, some predicate holds permanently after the action. The following is a simplified example of what I came up with.

A \* Action

B \* State predicate

Spec => [] (A => [] B)

My actual formula is much more complex than this with \A and \E, but it boils down to this statement. The idea is that if the spec is implemented correctly, at any point, if the action A happens, the state that follows action A and all future states satisfy predicate B. (in my case it is okay if B has to apply a little early as I think it does in my example).

The reason this statement does not work is because A => [] B has an action on the left and a temporal formula on the right which as far as I can tell is not allowed. Is there some way to write this formula?

[Stephan Merz]

Indeed, a formula such as [](A => []B) is not well-formed when A is an action. I once suggested an extension of TLA (the temporal logic underlying TLA+) in which such properties could be expressed [1], but it was never adopted.

The simplest workaround is to use a state predicate expressing that A has occurred instead of the action A on the left-hand side of the implication. Perhaps your specification already allows you to identify such a predicate, otherwise you can add a history variable

VARIABLE AhasOccurred

HInit == Init /\ AhasOccurred = FALSE

HNext ==

  /\ Next

  /\ \/ A /\ AhasOccurred’ = TRUE

     \/ ~A /\ UNCHANGED AhasOccurred

HSpec == HInit /\ [][HNext]_<<vars, AhasOccurred>> /\ …

and then prove the theorem Spec => [](AhasOccurred => []B). That proof should be straightforward, the main arguments being that A establishes B and that every transition preserves B, assuming that AhasOccurred is true. It will require a suitable invariant.

You may notice that this property is subtly different from the one that you wrote in that it only shows that B will be (and remain) true after A has occurred, whereas your original formula claims that B must already be true when A occurs. In my experience, the former is more frequent, but if you really want the latter, you can find a similar way to express it.

Hope this helps,

Stephan

[1] https://members.loria.fr/SMerz/papers/gtla.html

--
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...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/1a967613-aa85-48d3-a488-a6bc643a3509n%40googlegroups.com.

[Dylan Zueck]

Thanks! I was thinking something along those lines would work, the only issue with that is that in my case A is actually \A args \in valid_args: A(args) and B is E\ value in some_range: []B(value, args) which would make my goal:

\A args \in valid_args: [](A(args) =>  E\ value in some_range: []B(value, args))

I think that technique would still work if instead I made AhasOccured a set containing args that have happened in the past.