Subject: FW: PSL LRM: More comments and issues
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Tue Jun 24 2003 - 07:50:30 PDT
Ben,
A very belated response to one of your comments.
> 4.4.3 Strong vs. weak operators
> A property which (change to THAT) uses a non-negated strong operator is a liveness property, while one that contains only non-negated weak operators is a safety property.
> 4.4.2 states: a safety property claims that â??something
> badâ?? does not happen.
> Question: (req until ack) : is that safety if ack never happens?
> The weak until does not require that ack happens.
Yes, (req until ack) is a safety property. The bad thing that we are
claiming never happens is that !req is seen before ack is seen.
Since "until" is a weak operator, (req until ack) is a safety
property under both characterizations.
There does seem to be some inconsistency in the characterizations
of liveness. According to 4.4.3, (req until! ack) is a liveness
property. But it is not true that every finite path can be extended
to a path on which this property holds, since we could have
!req && !ack on the first cycle.
In fact, (req until! ack) has both a safety aspect and a liveness aspect.
It might be more accurate to say that a property that uses a non-negated
strong operator has a liveness element.
Regards,
Anthony
This archive was generated by hypermail 2b28 : Tue Jun 24 2003 - 07:59:54 PDT