Re: [sv-ac] 1932 LTL_Formal.0701009.pdf partial review.

Hi.

One erratum below.

/Johan

On Tue, Oct 23, 2007 at 02:54:47PM +0200, Johan Mårtensson wrote:
> Hi,
> 
> 
> The following are some comments on F.2 of LTL_Formal.0701009.pdf
> 
> 
> 
> F.2.1
> p.1
> In the comments to the abstract grammar:
> 
> "s_next" form  ==> "next" form 
> "s_until" form  ==> "until" form 
> 
> p.2
> Same as above in abstract grammar for clocked properties.
> 
> p.6
> F.2.3.2.7
> REPLACE
> (p s_until q) == ((p s_until q) and eventually p) [circular]
> WITH
> (p s_until q) == ((p until q) and s_eventually q)
> OR
> (p s_until q) == not (not q until_with not p)
> 
> MAYBE REPLACE
> (p s_until_with q) == (p s_until (p and q))
> WITH
> (p s_until_with q) == not (not q until not p)
> 
> With the last two replacements the duality of the different until operators
> becomes more visible.
> 
> 
> F.2.3.2.8 
> 
> It seems unnecessarily convoluted to me to define  next[m] in terms of
> s_next[m] which then is defined in terms of s_next which is defined in terms of
> next.
> 
> Why not instead define the weak wariant of the ranged operators in terms of the
> weak primitive operator, and then define the strong ranged operators in terms
> of the weak ranged operators:
> 
> next[0] p == p (next[0] is needed for the definition of eventually[0:x])
> next[n] p == next (next[n-1] p) [n>0]
> 
> and
> s_next[n] p == not next[n] not p [n>0]
> 
> eventually[m:m] p == next[m] p [m>=0]
> eventually[m:n] p == eventually[m:n-1] p or next[n] p [0<=m<n]
> always[m:m] p == always[m] p [m>=0]

Should be 
 always[m:m] p == next[m] p [m>=0]

> always[m:n] p == always[m:n-1] p and next[n] p [0<=m<n]
> s_eventually[m:n] p = not always[m:n] not p
> s_always[m:n] p = not eventually[m:n] not p
> 
> 
> /Johan
> -- 
> ------------------------------------------------------------
> Johan Mårtensson                 Office: +46 31 7451913
> Jasper Design Automation         Mobile: +46 703749681 
> Arvid Hedvalls backe 4           Fax: +46 31 7451939
> 411 33 Gothenburg, Sweden        Skype ID: johanmartensson
> ------------------------------------------------------------
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

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