[sv-ac] Re: review 1734

Doron:

I have uploaded an updated proposal for mantis 1734 and deleted the
old ones.

Please review it.

> * Vacuity,  should have a sub-section for T (Q is not there anyway) and 
> put the disable iff there

This I did not do.  I think that if you add T here, then you have to
add U and Q too and repeat all the top-level forms and explain that Q
needs to be replaced by Q' using the clock rewrite rules.  I did find
some mismatches between subscripted and non-subscripted P, and the
easiest fix to me was to remove the unnecessary subscripts.

J.H.


> Date: Wed, 07 Mar 2007 14:44:01 -0600
> From: Doron Bustan <dbustan@freescale.com>
> X-Accept-Language: en-us, en
> X-OriginalArrivalTime: 07 Mar 2007 20:44:02.0735 (UTC) FILETIME=[57133BF0:01C760F9]
> 
> I didn't see anything wrong but I think that some information is still 
> missing.
> 
> At E.3.3.1 should add
> 
> * for neutral satisfaction
> 
> —For U = Q, w\models U iff w \models Q.
> — For U = disable iff (b) Q, w\models U iff either
> — w\models Q and no letter of w satisfies b, or
> — Some letter of w satisfies b and w^{0.. i–1}\bot^\omega\models P for i 
> the least index such that
> w i\models b, 0 < i < |w| .
> 
> * for the \models^d relation , should add
> 
> Disabling of top-level properties is defined as follows:
> — w\not\models^d Q.
> — w\models^d Q disable iff (b) iff some letter of w satisfies b and both 
> w^{0.. i–1}\top^\omega\not\models P and
> w^{0..i–1}\bot^\omega\models P for i the least index such that 
> w^i\models b, 0 < i < |w|.
> 
> 
> 
> * Vacuity,  should have a sub-section for T (Q is not there anyway) and 
> put the disable iff there
> 
> * E.3.6.1 same as E.3.3.1
> 
> Doron

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