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

[tlaplus] Re: Conjoining Specifications lemma1.2

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.


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