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

Hi Doron,

There is a need to fix the numeration. There are two different clauses
F.2.3.2...

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Bustan, Doron
Sent: Sunday, December 09, 2007 1:59 PM
To: Johan Martensson; sv-ac@server.eda.org
Subject: RE: [sv-ac] 1932: Review of LTL_Formal.071205.pdf

Hi Johan,

See my answers below:

>>
>>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.
>>

[[DB:]] The difference shows when b has value x. In the old definition 
(!b |-> P2) it does not require P2 to hold. 

There was an e-mail exchange about this problem and there is a mantis
item for it (1786). It was hard to converge but I think that (weak(b) or
P2). does the trick. The reason I add it in 1932 is that we need the
weak operator.

>>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"

[[DB:]] I agree that there is a problem; I am still not sure how to
solve it.

>>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.

[[DB:]] oops, sorry for that. I will fix it in the next version.

Thanks

Doron
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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