[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.