Re: [tlaplus] Re: Conjoining Specifications lemma1.2

It's not a matter of the definition of a safety property so much as the definition of a safety property plus additional constraints on the specification.

A safety property is a closed set (or class) of behaviors, but in "Refinement Mappings" only stuttering-invariant specifications are considered and "Conjoining Specifications" uses TLA, where all formulas are invariant under stuttering anyway.

A state machine is a form of specification with a set of initial states and a next-state relation. While a state machine (without fairness conditions) is a safety property, it, too, can be either invariant under stuttering or not. Because in TLA all formulas are invariant under stuttering, in particular all state machines specified *in TLA* would be.

On Saturday, March 16, 2019 at 10:42:50 PM UTC, Apostolis Xekoukoulotakis wrote:

According to your paper "The existence of refinement mappings." , the safety property is a closed set , similarly to this paper.
The definition you mention now, coincides with the property generated by a state machine , which is a safety property.

I will first try to prove properties with the more general definition, and If I can't, go with the second definition.

Ok let me see if it works.

On Sat, Mar 16, 2019 at 11:46 PM Leslie Lamport <tlapl...@xxxxxxxxx> wrote:
What you missed is the fact that if a safety property is satified by a
behavior b, then it is satisfied by the behavior that has the same
first N states as b and then halts--where halting means taking nothing
but stuttering steps. In your example, since PA and PC are safety
properties, they are both satisfied by the behavior (2, 2, 2, ...) --
a behavior not satisfied by PB. Hence |= (PC /\ PA => PB) is false,
so the implication is true. And I believe the lemma is true.

Leslie

On Friday, March 15, 2019 at 9:56:22 PM UTC-7, Apostolis Xekoukoulotakis wrote:
I am unable to prove this direction :

If PA , PB , PC are safety properties , then
if ⊨ ((PC /\ PA) => PB) , then ⊨ (PC => (PA -▹ PB))

Consider closed sets
1 . PA : all sequences with prefix (2 , 4 , ....)
2 . PC : all sequences with prefix (2 , 5 , ...)
3 . PB : all sequences with prefix (3 , ....)

All sets are closed, aka they are safety properties, and the condition is true.
However , for sequence a = (2 , 5 , ...) , the result of the lemma is not true.
since a belongs at PC, and the finite prefix (2) belongs at PA, but the prefix (2) does not belong at PB, as it should.

Am I missing something? Maybe I made an error in the definitions .

1 . https://lamport.azurewebsites.net/pubs/pubs.html#abadi-conjoining

--
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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.