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

[tlaplus] Re: Conjoining a spec with an invariant



Great, thank you, that makes sense. 

To your point about SpecStrong2 not being exactly equivalent to SpecStrong1: in my particular spec it's more or less trivial to see that the initial states satisfy Safety (regardless of whether C1 holds or not), so I was less worried about constraining the initial states to satisfy C1. But thank you for pointing it out. I will indeed be careful to include C1 in the initial state predicate if I want to ensure that SpecStrong2 is exactly equivalent to SpecStrong1.

On Wednesday, November 25, 2020 at 11:43:03 AM UTC-5 Leslie Lamport wrote:
As you suspected, your specification SpecStrong1 is perfectly fine TLA+, but TLC does not handle it correctly.  It is considering the formula []C1 part of a liveness specification, so if you had it check a liveness property P it would actually be checking the property []C1 => P.  SpecStrong2 is almost equivalent to SpecStrong1.  The equivalent specification is

   Init /\ C1  /\  [][Next /\ C1']_vars

assuming that vars includes all the variables in C1.  That's the best way to write your spec.  Using it as a state constraint wouldn't quite work because, if I recall correctly, TLC does not look for successor states to a state not satisfying the constraint, but it does do invariance checking on that state.

On Wednesday, November 25, 2020 at 6:52:05 AM UTC-8 will...@xxxxxxxxx wrote:
I am working on a spec, call it Spec, that I expect to violate some safety property, call it Safety, but I want to demonstrate that under a certain stronger assumption C1 (which is a state predicate), Spec does satisfy safety. That is:

C1 == (* some state predicate *)
Spec == Init /\ [][Next]_vars
SpecStrong1 == Spec /\ []C1

THEOREM ~(Spec => Safety)
THEOREM SpecStrong1 => Safety

I was not sure if TLC would correctly handle the form of specification used for SpecStrong1, though. I also tried writing this as:

SpecStrong2 == Init /\ [][Next /\ C1']_vars

which seemed to work correctly i.e. the model checker returned no invariant violation which matched my expectations. 

I also considered specifying C1 as a state constraint during model checking but I'm not sure if that would achieve my goal correctly. My understanding is that, from a pure TLA+ perspective, SpecStrong1 is a valid formula with a sensible meaning, it just may not be handled by TLC. Any thoughts or suggestions on this would be appreciated.

  

--
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/44ddbf84-1f2a-462e-8108-f9f2076d8475n%40googlegroups.com.