Re: [sv-ac] Comment regarding LTL - Mantis 1932

Hi Doron, Ed:

> >>Regarding the leading clock in until. My point is that the rule deals
> with
> >>the case when some clock v flows in P1 until P2. But what if there is
> no
> >>clock flowing in? E.g. Assert property (P1 until P2);
> >>Does the leading clock of P1 have to be the same as in P2? (I hope
> so.)
> >>
> 
> [[DB:]] Since the leading clock of until is inherited, there must be a
> clock flowing from the left into the until property; so unless there is
> an inferred clock, the assertion "assert property (P1 until P2);" is
> illegal.

I agree with Doron that if no clock flows in, then this think that

   assert property (P1 until P2); 

is illegal.  Whether or not the semantic leading clock of P1 and P1
must be identical and identicla to the inherited clock depend on 1683.
If 1683 is rejected, then any non-inherited clocks of P1 and P2 must
be identical and also identical to the inherited clock.

> 
> The rule in item c) says "- Every explicit semantic leading clock of P1
> or P2 is identical to c."  I think this match your intuition
> 
> 
> >>In the formal part, vacuity, in the case of P1 or P2, it seems to me
> that
> >>if P1 has vacuous success and P2 is non-vacuous failure, it would be
> >>declared as non-vacuous success. That looks strange. Or did I miss
> >>something?
> >>
> [[DB:]] I think you are right, and this is bothering. However, it is not
> part of 1932. We tried to give a conservative definition (no false
> negatives) and keep the definition indifferent to negation. I think that
> sometime in the future we will have to find a better definition.

This seems to be an inevitable consequence of decoupling "success"
from "vacuity".  Our basic intuition has been that non-vacuity is
oblivious to negation because of the rule

   w |=^{non} not p

iff 

   w |=^{non} p

I think that if we want

   (w |= p or q)  and  (w |=^{non} p or q)

to imply that 

   either
      w |= p and w^{non} |= p 
   or 
      w |= q and w^{non} |= q

then we will need to recouple the concepts.  This seems to provide
some chanllenges for negated formulas.

J.H.
 
   

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.