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

*From*: Ron Pressler <ron.pressler@xxxxxxxxx>*Date*: Mon, 18 Mar 2019 06:21:50 -0700 (PDT)*Ironport-data*: A9a23:hdWplaD6jyDEfxVWkefolB7pSiHEJp4JiSr74LtitojPGpt29E4cT3 9fQ01mF4dKn6AD2AXuFqHqovWofymCQj9FuXuJ4JA5xOtZIkWa3O50/5wtvbcupeWgrynLo5 o8Nu0w8oIn8OPCzeqtF70y+HZZbkFWPen8hdjk1/uQ978vZlBXlZbHV6Wv4T7wv4DX6cTwck I0jC1mXIcjQBzK1gBE1CmLNGpFkKNPWqjyw5YD7noxsg+KfFVCe4ajfcThhnDlg0ueHP4nl2 Xn6MP8NmsN8u1yLrmq0BD1zvhjkK1elYX8LSxc8eP/oE2i+1PNgo3EDMDeVB7GDR1pL1FxZm QErCeeguH/8d7/nSVKXAG0O7BdL4ywEiGz5YTyKVbnZdJgNqppQ/11qiWX9OGxXE9gfRuTfX GjqYk+6mfFqHKkjBqWAjvQ9IvTVpDjB3wuCeOaW37RZyNKPgmCsMOjwQ0EfUHjVsxZV8+9iz ZoyHFUUrvnnTGXOgox/eUf4qW3CJDXUSAwJ39Ui0GxYVtZ81nAGMg5R66pRpgqINkcN/RSZw DwJI5no3tq6eslf31+p9FTIWyZDfr5ZZgcWjSOcjHsEtMuQ/GW58IhS1wsdwcEdYkk4FTq3F vBbLa3CDug6tOxA6sXaJNIIbL2B9SopycoNjzT2pDVMoEsODyVC+dkraN+B4TY8EL+f/XZ7U NzXkc7JtgoUWvlQqI3t3/VEzTFueoMWmVP2M4BYNJUepygEKCLsUzSWyy/0IhGC1vlBmpGFm I+GdpZcB6mbBVORE5OJxPOyRT5aQAteB9hYlAxz6OkpneYz7Kz4dXOEMRkWohwLHY789YUcd 7C/DERXZuSkfXm7UANVD1fSRXF0TX42s385DFAB8V8UqW57YbsWVrpZyvpxmo3gfwn7V4QC2 +O1pjGrYlW06lKzvn4KLep3BS59432R2eo4tueIRyvkI4RAX1Y0jAyLH4U5byBCiMQv47Lpf vzGQ==*References*: <CAFEV_-im2PbUEpqkipW=GprWeqtr6OAw7QovVMpbcjyz=M9EJw@mail.gmail.com> <29bbe489-7365-429a-b054-9fcf9c5b264d@googlegroups.com> <CAFEV_-jKLP9rB12EOkHDRH0xad-An+vxjfSmFy9HZcZDvubV9Q@mail.gmail.com>

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.

R

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 , thenif ⊨ ((PC /\ PA) => PB) , then ⊨ (PC => (PA -▹ PB))Consider closed sets1 . 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 .

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 .

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.

**Follow-Ups**:**Re: [tlaplus] Re: Conjoining Specifications lemma1.2***From:*Apostolis Xekoukoulotakis

**References**:**[tlaplus] Conjoining Specifications lemma1.2***From:*Apostolis Xekoukoulotakis

**[tlaplus] Re: Conjoining Specifications lemma1.2***From:*Leslie Lamport

**Re: [tlaplus] Re: Conjoining Specifications lemma1.2***From:*Apostolis Xekoukoulotakis

- Prev by Date:
**Re: [tlaplus] TLA Proof System - the syntax has impact on provability ?** - Next by Date:
**Re: [tlaplus] Re: Conjoining Specifications lemma1.2** - Previous by thread:
**Re: [tlaplus] Re: Conjoining Specifications lemma1.2** - Next by thread:
**Re: [tlaplus] Re: Conjoining Specifications lemma1.2** - Index(es):