From cb7bdf8c1f196c9d91c2bd770adc07b7aa6a35b7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 28 Jul 2013 21:04:10 +0200 Subject: [PATCH] Fix interpretation of {e[*]} and !{e[*]}. This follows from a discussion with Ernesto Posse. The semantics for the {...} operator we use in Spot comes from the cl(...) operator defined by Dax et al. (ATVA'09). This is slightly different from the the way the PSL spec interprets a SERE used in the context of a temporal formula (appendix B.3.1.1.2, item 7). cl({a;b}[*]) would match any infinite word that starts with a;b, while in PSL {a;b}[*] would match any infinite word that alternates a and b. Spot documents that {SERE} in a temporal formula is interpreted like cl(SERE) however it failed to ignore the empty prefix of SERE. So {{a;b}[*]} would match anything, because the empty word is a prefix of any word, and is also accepted by {a;b}[*]. Some trivial identities and basic rewritings were also wrongly considering these empty prefixes as well. This patch therefore fixes the translation and syntactic simplification rules, to really ignore these empty prefixes. In some future version it should probably be wise to rename this {...} operator as cl(...), and use {...} for the semantics given in appendix B.3.1.1.2 (item 7) of the PSL specs. * src/ltlast/unop.cc: Fix trivial identities. We have {[*0]} = 0 and !{[*0]} = 1. * src/ltlvisit/simplify.cc: Fix basic rewriting rules. {e[*]} = {e} and !{e[*]} = !{e}. * doc/tl/tl.tex: Adjust documentation. * doc/tl/tl.bib (dax.09.atva): New entry. * src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any infinite word for {e[*]} just because the empty prefix is matched by e[*]. * src/tgbatest/ltl2tgba.test: Add a test case. * NEWS: Mention it. * THANKS: Add Ernesto. --- NEWS | 7 ++++ THANKS | 1 + doc/tl/tl.bib | 16 ++++++++- doc/tl/tl.tex | 21 ++++++++---- src/ltlast/unop.cc | 18 +++++----- src/ltlvisit/simplify.cc | 65 ++++++++++++++++++++++++++---------- src/tgbaalgos/ltl2tgba_fm.cc | 11 ------ src/tgbatest/ltl2tgba.test | 8 +++++ 8 files changed, 103 insertions(+), 44 deletions(-) diff --git a/NEWS b/NEWS index eb2ec2e4d..3666d89ae 100644 --- a/NEWS +++ b/NEWS @@ -7,6 +7,13 @@ New in spot 1.1.3a (not released) - When used from ltlcross, the same parser would fail to parse further neverclaims after the first failure. - Add a missing newline in some error message of ltlcross. + - Expressions like {SERE} were wrongly translated and simplified + for SEREs that accept the empty word: they were wrongly reduced + to true. Simplification and translation rules have been fixed, + and the doc/tl/tl.pdf specifications have been updated to better + explain that {SERE} has the semantics of a closure operator that + is not exactly what one could expect after reading the PSL + standard. New in spot 1.1.3 (2013-07-09) diff --git a/THANKS b/THANKS index f318e8a9e..2960fe0ac 100644 --- a/THANKS +++ b/THANKS @@ -3,6 +3,7 @@ suggestions. Akim Demaille Christian Dax +Ernesto Posse Étienne Renault Felix Klaedtke František Blahoudek diff --git a/doc/tl/tl.bib b/doc/tl/tl.bib index bf0bee99b..7ccab7f74 100644 --- a/doc/tl/tl.bib +++ b/doc/tl/tl.bib @@ -12,7 +12,7 @@ publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7214}, - pages = {95--109} + pages = {95--109} } @InProceedings{ beer.01.cav, @@ -80,6 +80,20 @@ note = {\url{https://es.fbk.eu/people/tonetta/tests/tcad07/}} } +@InProceedings{ dax.09.atva, + author = {Christian Dax and Felix Klaedtke and Stefan Leue}, + title = {Specification Languages for Stutter-Invariant Regular + Properties}, + booktitle = {Proceedings of the 7th International Symposium on + Automated Technology for Verification and Analysis + (ATVA'09)}, + pages = {244--254}, + year = {2009}, + volume = {5799}, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag} +} + @InProceedings{ duret.11.vecos, author = {Alexandre Duret-Lutz}, title = {{LTL} Translation Improvements in {Spot}}, diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 8947c9cfa..57c9f8ede 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -833,6 +833,13 @@ is not a model of \samp{$\sere{a\PLUS{}\CONCAT\NOT a\CONCAT(a\STAR{}\ANDALT(a\STAR{}\CONCAT\NOT a\CONCAT a\STAR{}))}$} because this SERE does accept any word. +Note that the semantics of $\sere{r}$ comes from the +$\mathsf{cl}(\cdot)$ operator defined by~\citet{dax.09.atva}. This +differs from the interpretation of a SERE in the context of a temporal +formula given by the PSL standard~\citep[Appendix~B.3.1.1.2, +item~7]{psl.04.lrm}: the $\mathit{cl}(\cdot)$ semantics accepts more +words. + \subsection{Syntactic Sugar}\label{sec:pslsugar} The syntax on the left is equivalent to the syntax on the right. @@ -869,8 +876,8 @@ formula $b$, the following rewritings are systematically performed & \nsere{\1} & \equiv \0 \\ \sere{\eword}\Asuffix f&\equiv \1 & \sere{\eword}\Esuffix f&\equiv \0 -& \sere{\eword} & \equiv \1 -& \nsere{\eword} & \equiv \0 \\ +& \sere{\eword} & \equiv \0 +& \nsere{\eword} & \equiv \1 \\ \sere{b}\Asuffix f&\equiv (\NOT{b})\OR f & \sere{b}\Esuffix f&\equiv b\AND f & \sere{b} &\equiv b @@ -1531,10 +1538,12 @@ denoted with $\equiV$ can be disabled by setting the Here are basic the rewritings for the weak closure and its negation: \begin{align*} - \sere{r}&\equiv \1\text{~if~}\varepsilon\VDash r& - \nsere{r}&\equiv \0\text{~if~}\varepsilon\VDash r\\ - \sere{r_1;r_2}&\equiv \sere{r_1}\text{~if~}\varepsilon\VDash r_2& - \nsere{r_1;r_2}&\equiv \nsere{r_1}\text{~if~}\varepsilon\VDash r_2\\ + \sere{r\STAR{}}&\equiv \sere{r}& + \nsere{r\STAR{}}&\equiv \nsere{r}\\ + \sere{r_1;r_2}&\equiv \sere{r_1}\phantom{{}\OR\sere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2& + \nsere{r_1;r_2}&\equiv \nsere{r_1}\phantom{{}\AND\nsere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2\\ + \sere{r_1;r_2}&\equiv \sere{r_1}\OR\sere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2& + \nsere{r_1;r_2}&\equiv \nsere{r_1}\AND\nsere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2\\ \sere{b;r}&\equiV b\AND\X\sere{r}& \nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\ \sere{b\STAR{};r}&\equiv b\W\sere{r}& diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 8717493f1..2ac6cbec8 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -292,19 +292,19 @@ namespace spot // {0} = 0, {1} = 1, {b} = b if (child->is_boolean()) return child; - // {[*0]} = 1 + // {[*0]} = 0 if (child == constant::empty_word_instance()) - return constant::true_instance(); + return constant::false_instance(); break; case NegClosure: case NegClosureMarked: - // {1} = 0, {[*0]} = 0 - if (child == constant::true_instance() - || child == constant::empty_word_instance()) + // {1} = 0 + if (child == constant::true_instance()) return constant::false_instance(); - // {0} = 1 - if (child == constant::false_instance()) + // {0} = 1, {[*0]} = 1 + if (child == constant::false_instance() + || child == constant::empty_word_instance()) return constant::true_instance(); // {b} = !b if (child->is_boolean()) diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 633346faf..e71e7ffd6 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1550,16 +1550,17 @@ namespace spot case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: - // {e} = 1 if e accepts [*0] - // !{e} = 0 if e accepts [*0] + // {e[*]} = {e} + // !{e[*]} = !{e} if (result_->accepts_eword()) - { - result_->destroy(); - result_ = ((op == unop::Closure) - ? constant::true_instance() - : constant::false_instance()); - return; - } + if (const bunop* bo = is_Star(result_)) + { + result_ = + recurse_destroy(unop::instance(op, + bo->child()->clone())); + bo->destroy(); + return; + } if (!opt_.reduce_size_strictly) if (const multop* mo = is_OrRat(result_)) { @@ -1578,6 +1579,26 @@ namespace spot } if (const multop* mo = is_Concat(result_)) { + if (mo->accepts_eword()) + { + if (opt_.reduce_size_strictly) + break; + // If all terms accept the empty word, we have + // {e₁;e₂;e₃} = {e₁}|{e₂}|{e₃} + // !{e₁;e₂;e₃} = !{e₁}&!{e₂}&!{e₃} + multop::vec* v = new multop::vec; + unsigned end = mo->size(); + v->reserve(end); + for (unsigned i = 0; i < end; ++i) + v->push_back(unop::instance(op, mo->nth(i)->clone())); + mo->destroy(); + result_ = multop::instance(op == unop::Closure ? + multop::Or : multop::And, v); + result_ = recurse_destroy(result_); + return; + } + + // Some term does not accept the empty word. unsigned end = mo->size() - 1; // {b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄} // = b₁&X(b₂&X(b₃ W {e₁;f₁;e₂;f₂})) @@ -1601,15 +1622,25 @@ namespace spot unsigned s = end + 1 - start; if (s != mo->size()) { - multop::vec* v = new multop::vec; - v->reserve(s); - for (unsigned n = start; n <= end; ++n) - v->push_back(mo->nth(n)->clone()); - const formula* tail = - multop::instance(multop::Concat, v); - tail = unop::instance(op, tail); - bool doneg = op != unop::Closure; + const formula* tail; + if (s > 0) + { + multop::vec* v = new multop::vec; + v->reserve(s); + for (unsigned n = start; n <= end; ++n) + v->push_back(mo->nth(n)->clone()); + tail = multop::instance(multop::Concat, v); + tail = unop::instance(op, tail); + } + else + { + if (doneg) + tail = constant::false_instance(); + else + tail = constant::true_instance(); + } + for (unsigned n = start; n > 0;) { --n; diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 0988e461f..290f3b6b5 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1367,12 +1367,6 @@ namespace spot { // rat_seen_ = true; const formula* f = node->child(); - if (f->accepts_eword()) - { - res_ = bddtrue; - return; - } - tgba_succ_iterator* i = dict_.transdfa.succ(f); res_ = bddfalse; @@ -1410,11 +1404,6 @@ namespace spot rat_seen_ = true; { const formula* c = node->child(); - if (c->accepts_eword()) - { - res_ = bddfalse; - return; - } if (mark_all_) { op = unop::NegClosureMarked; diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index a3098dd5a..afbf703d6 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -209,3 +209,11 @@ grep 'states: 4$' stdout # the following formula to be considered equivalent to anything... ../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'false' && exit 1 ../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'true' + +# Test some equivalences fixed in Spot 1.1.4 +../../bin/ltlfilt -f '{{a;b}[*]}' --equivalent-to 'a & Xb' +../../bin/ltlfilt -r -f '{{a;b}[*]}' --equivalent-to 'a & Xb' +../../bin/ltlfilt -f '!{{a;b}[*]}' --equivalent-to '!a | X!b' +../../bin/ltlfilt -r -f '!{{a;b}[*]}' --equivalent-to '!a | X!b' +../../bin/ltlfilt -f '{a[*];b[*]}' --equivalent-to 'a | b' +../../bin/ltlfilt -r -f '{a[*];b[*]}' --equivalent-to 'a | b'