[sv-ac] 1932: Review of LTL_Formal.071205.pdf

Hi Doron, 

some remarks on remaining issues.


F.2.3.2.4 Derived conditional operator
======================================

Why did the second operand become (weak(b) or P2). Is there some subtle
semantic difference between it and (!b |-> P2). I would prefer the
second since it seems intuitively simpler to comprehend.

F.3.1.1 and F.3.1.2
===================

I still don't like the explanations of what T^s and T^p does. As I
explained in an earlier mail. I think

a) The abstract syntax and the "surface syntax" are not the same w.r.t.
clock scope.
   -- clock scope in the surface syntax is determined by left to right
   "clock flow".
   -- the abstract syntax has hierarchical clock scope.
b) The clock rewriting rules in this form are not correctly applicable
to the "surface syntax"
c) The concept of leading clock is only "defined" (does only make
sense?) for the surface syntax.

Therefore it seems it is not appropriate to talk about "leading clock"
in the description of the clock rewriting rules.

Furthermore I think the description should not preclude application of T
to non clocked properties and sequences.

> 
> "The transformation T^s(S,c) recursively defined below produces an
> unclocked sequence R equivalent to a given clocked sequence S with a
> leading clock c"

F.3.6.1.
========

The mention of "last index" was not removed in this instance of the
definition for accept_on.

Furthermore I think the qualification "and no letter of w satisfies b"
is unnecessary.


Best Regards,

Johan


On Wed, Dec 05, 2007 at 11:20:51AM +0100, Johan Mårtensson wrote:
> Hi,
> 
> I went through all of LTL_Formal.071120.pdf and here is my comments:
> 
> F.2.1.
> =====
> 
> The abstract grammar for clocked properties.
> 
> Instead of '|->' there is the sequence of symbols
> longdash-shortdash-upsidedownquestionmark.
> 
> This is the case in for example F.3.3.1.
> 
> F.2.3.1.4 Other derived operators
> =================================
> 
> In the case for throughout there is a 'b1' on the right hand side. It
> should be 'b'.
> 
> F.2.3.2.1 Derived sequential property
> =====================================
> 
> I think the first occurrence of 'under' should be changed to 'in a' and
> the second one to 'in an'.
> 
> F.2.3.2.4 Derived conditional operator
> ======================================
> 
> The rightmost P_1 should be changed to P_2.
> 
> 
> F.2.3.2.7 Derived unbounded temporal operators
> ===============================================
> 
> In the case for s_until I think s_eventually and not eventually should
> be used on the right hand side.
> 
> F.2.3.2.8 Derived bounded temporal operators
> ============================================
> 1) In the case for 'next p' and 'next[0] p' there are ugly gaps in the
> operator symbols for suffix implication.
> 
> This occurs in many places in the document.
> 
> 2) In the case for 'next[m] p' m>0 there is an 'n' on the rhs. It should be
> an 'm'.
> 
> 3) In the case for 's_eventually[m:$]p', why not use 'not always[m:$]
> not p' as the definition as in the case for 's_eventually[m:n]p'?
> 
>  s_next[m] s_eventually p
> =
>  not next[m] not s_eventually p
> =
>  not next[m] always not p
> =
>  not always[m:$] not p
> 
> F.3.1.1 Rewrite rules for sequences.
> ====================================
> 
> "The transformation T^s(S,c) recursively defined below produces an
> unclocked sequence R equivalent to a given clocked sequence S with a
> leading clock c"
> 
>  Not all clocked sequences according to the abstract syntax (F.2.1) have
>  a leading clock, for example (@(c1)R1)##1(@(c2)R2). However the clock
>  rewrite rules are applicable also in this case by
>  T^s((@(c1)R1)##1(@(c2)R2),1).
> 
>  In addition according to the (Draft4) abstract syntax for the clocked
>  sequence '@(c) R' R must be unclocked. To apply the rewrite to this
>  clocked sequence would be to evaluate T^s(R,c) or to evaluate T^s(@(c)
>  R,1). Neither of these seem to match with the description.
> 
>  BTW. I hope we have some mantis item for removing the restriction that
>  clocks cannot be nested in the abstract syntax.
> 
> Maybe the following could serve as a replacement.
> 
>  "The transformation T^s(S,c) recursively defined below produces an
>  unclocked sequence R equivalent to a given clocked (or unclocked)
>  sequence S in the context of a clock c"
> 
> 
> F.3.1.2 Rewrite rules for properties.
> ====================================
> 
> Similar comment to that of F.3.1.1
> 
> F.3.3 Satisfaction without local variables
> ==========================================
> 
> Case for or: On the right hand side 'and' should be changed to 'or'.
> 
> Case for accept_on: Should be changed to accord with Mantis 1757 where
> the definition is not in terms of 'least index'. (Same for F.3.6.1)
> 
> Best Regards,
> 
> Johan
> 
> -- 
> ------------------------------------------------------------
> Johan Mårtensson                 Office: +46 31 7451913
> Jasper Design Automation         Mobile: +46 703749681 
> Kvarnbergsgatan 2                Fax: +46 31 7451914
> 411 05 Gothenburg, Sweden        Skype ID: johanmartensson
> ------------------------------------------------------------

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Kvarnbergsgatan 2                Fax: +46 31 7451914
411 05 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

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