[sv-ac] question about non-vacuity for accept_on

Hi Doron:

Why doesn't the definition of non-vacuity for accept_on parallel
that for disable iff?

For disable iff, the intuition is that if the attempt is ended 
by the disable condition, then it is vacuous.

The same intuition does not apply to accept_on.  Can you summarize
the rationale?

I am thinking that maybe it has to do with coding style in which the
accept_on condition is required to end the evaluation, like

   accept_on(halt) !halt[*0:$] ##1 1 |-> blah


J.H.
   

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