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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Wed, 25 Nov 2020 08:43:03 -0800 (PST)*References*: <9a13721f-eb0e-455c-bb04-befc940d27c9n@googlegroups.com>

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]_varsSpecStrong1 == Spec /\ []C1THEOREM ~(Spec => Safety)THEOREM SpecStrong1 => SafetyI 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']_varswhich 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/1eb911e2-4e51-48d0-a98b-0038334e6e48n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Conjoining a spec with an invariant***From:*Willy Schultz

**References**:**[tlaplus] Conjoining a spec with an invariant***From:*Willy Schultz

- Prev by Date:
**[tlaplus] Conjoining a spec with an invariant** - Next by Date:
**[tlaplus] Re: Conjoining a spec with an invariant** - Previous by thread:
**[tlaplus] Conjoining a spec with an invariant** - Next by thread:
**[tlaplus] Re: Conjoining a spec with an invariant** - Index(es):