[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:Cindy.html>, Dana Fisman, John Havlicek<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/h/Havlicek:John.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:Anthony.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#EisnerFHLMC03>: 27-39

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