RE: [sv-ac] triggering of action blocks.

Hi Dana:
 
See also Mantis 0921 on making precise when subroutines attached to
sequences execute. It is similar to, but not the same as, the problem
for action blocks.
 
It may be that a semantic approach works better for action blocks, while
a syntactic approach works better for subroutines attached to sequences.
 
A question that was never really decided was whether the policy for
subroutines should be liberal or conservative, or allow both, with some
controls to specify when a liberal or conservative policy applies.
 
J.H.
 
 
________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Dana
Fisman
Sent: Thursday, June 03, 2010 4:52 AM
To: sv-ac@server.eda.org
Cc: Korchemny, Dmitry; Eduard Cerny
Subject: [sv-ac] triggering of action blocks.

 Hi all,

I added a comment to mantis item 1509. (This follows a mantis item 3099
I opened before Dmitry pointed me to this one. Here you can see
properties exemplifying the problem.)

The issue is that the LRM does not define when an action block should be
triggered. Doron and Dmitry proposed a syntactic definition (that is a
definition based on the structure of the assertion). I commented that we
can use a semantic definition as per the paper [EFHLMV03]. I believe
that even if we would like to have the syntactic definition, we can
benefit by comparing the two.

Regardless, we should decide about the cases where there is no point to
trigger the fail/pass action block statements. Should this be allowed or
not?

Best regards,

Dana

1509: http://www.eda-twiki.org/mantis/view.php?id=1502

3099: http://www.eda-twiki.org/mantis/view.php?id=3099

[EFHLMV03]: Cindy Eisner
<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/e/Eisner:Cind
y.html> , Dana Fisman, John Havlicek
<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/h/Havlicek:Jo
hn.html> , Yoad Lustig
<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/l/Lustig:Yoad
.html> , Anthony McIsaac
<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/m/McIsaac:Ant
hony.html> , David Van Campenhout
<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/c/Campenhout:
David_Van.html> : Reasoning with Temporal Logic on Truncated Paths. CAV
2003
<http://www.informatik.uni-trier.de/~ley/db/conf/cav/cav2003.html#Eisner
FHLMC03> : 27-39

-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.