[tlaplus] Proving an action leads to a temporal formula

[Dylan Zueck <dzueck@xxxxxxx>]

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?

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