From 48471b51147f777fe35f4c005b32a2b90dfe903d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 13 May 2014 16:59:51 +0200 Subject: [PATCH] simplify: fix 3 incorrect simplification rules * src/ltlvisit/simplify.cc: Remove two incorrect rules, and partially disable another one. * doc/tl/tl.tex: Reflect the change. * src/ltltest/reduccmp.test: Likewise. * src/ltltest/equals.cc: Add safety checks to catch such errors in the future. * NEWS: Mention the bug. --- NEWS | 3 + doc/tl/tl.tex | 10 ++-- src/ltltest/equals.cc | 39 ++++++++++-- src/ltltest/reduccmp.test | 11 ++-- src/ltlvisit/simplify.cc | 121 +++++--------------------------------- 5 files changed, 61 insertions(+), 123 deletions(-) diff --git a/NEWS b/NEWS index b4fcd0617..3509f9e3c 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,9 @@ New in spot 1.2.3a (not yet released) - "ltl2tgta --ta" could crash in certain conditions due to the introduction of a simulation-based reduction after degeneralization. + - Fix three incorrect simplifications rules, all related to the + factorization of Boolean subformulas in operands of the + non-length-matching "&" SERE operator. New in spot 1.2.3 (2014-02-11) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 6c1c5d79e..18d89f1f8 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1460,13 +1460,11 @@ SERE. \0 &\text{else}\\ \end{cases}\\ \sere{b_1\CONCAT r_1}\ANDALT\sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\ANDALT r_2} & - \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\ + \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} \\ \sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} & - \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \\ - \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} & - \sere{r_1\CONCAT b_1}\AND \sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\AND b_2} \\ - \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} & - \sere{r_1\FUSION b_1}\AND \sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\AND b_2} \\ + \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} \\ + \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\ + \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \mathrlap{\quad\text{if~}\varepsilon\nVDash r_1\land\varepsilon\nVDash r_2}\\ \end{align*} Starred subformul\ae{} are rewritten in Star Normal diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index a9b5905f9..99ae46cfe 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -68,7 +68,7 @@ main(int argc, char** argv) if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) return 2; - int exit_code; + int exit_code = 0; { #if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM @@ -112,6 +112,14 @@ main(int argc, char** argv) const spot::ltl::formula* tmp; tmp = f1; f1 = simp.simplify(f1); + + if (!simp.are_equivalent(f1, tmp)) + { + std::cerr << "Source and simplified formulae are not equivalent!\n"; + std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n"; + exit_code = 1; + } + tmp->destroy(); } spot::ltl::dump(std::cout, f1); @@ -124,6 +132,14 @@ main(int argc, char** argv) const spot::ltl::formula* tmp; tmp = f1; f1 = simp.simplify(f1); + + if (!simp.are_equivalent(f1, tmp)) + { + std::cerr << "Source and simplified formulae are not equivalent!\n"; + std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n"; + exit_code = 1; + } + tmp->destroy(); } spot::ltl::dump(std::cout, f1); @@ -136,13 +152,21 @@ main(int argc, char** argv) const spot::ltl::formula* tmp; tmp = f1; f1 = simp.simplify(f1); + + if (!simp.are_equivalent(f1, tmp)) + { + std::cerr << "Source and simplified formulae are not equivalent!\n"; + std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n"; + exit_code = 1; + } + tmp->destroy(); } spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif - exit_code = f1 != f2; + exit_code |= f1 != f2; #if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR)) spot::ltl::ltl_simplifier simp; @@ -150,8 +174,11 @@ main(int argc, char** argv) if (!simp.are_equivalent(f1, f2)) { - std::cerr << "Source and destination formulae are not equivalent!" - << std::endl; +#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR)) + std::cerr << "Source and destination formulae are not equivalent!\n"; +#else + std::cerr << "Simpl. and destination formulae are not equivalent!\n"; +#endif exit_code = 1; } diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 0068be820..65338f1cd 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -# et Developpement de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +# Recherche et Developpement de l'Epita (LRDE). # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -317,9 +317,10 @@ for x in ../reduccmp ../reductaustr; do run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \ '{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}' run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}' - run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}' - run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}' - run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}' + run 0 $x '{{b1:(r1;x1*)}&{b2:(r2;x2*)}}' '{{b1&&b2}:{{r1&&r2};{x1*&x2*}}}' + run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1:r1*}&{b2:r2*}}' # Not reduced + run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*;b1}&{r2*;b2}}' # Not reduced + run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*:b1}&{r2*:b2}}' # Not reduced run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \ '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}' run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!' diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 3d57e8647..c2ce125d7 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -3456,22 +3456,14 @@ namespace spot if (op == multop::Concat) { head1->push_back(h->clone()); - multop::vec* tail = new multop::vec; - unsigned s = f->size(); - for (unsigned j = 1; j < s; ++j) - tail->push_back(f->nth(j)->clone()); - tail1->push_back(multop::instance(op, tail)); + tail1->push_back(f->all_but(0)); (*i)->destroy(); *i = 0; } else if (op == multop::Fusion) { head2->push_back(h->clone()); - multop::vec* tail = new multop::vec; - unsigned s = f->size(); - for (unsigned j = 1; j < s; ++j) - tail->push_back(f->nth(j)->clone()); - tail2->push_back(multop::instance(op, tail)); + tail2->push_back(f->all_but(0)); (*i)->destroy(); *i = 0; } @@ -3535,20 +3527,14 @@ namespace spot if (op == multop::Concat) { tail3->push_back(t->clone()); - multop::vec* head = new multop::vec; - for (unsigned j = 0; j < s; ++j) - head->push_back(f->nth(j)->clone()); - head3->push_back(multop::instance(op, head)); + head3->push_back(f->all_but(s)); (*i)->destroy(); *i = 0; } else if (op == multop::Fusion) { tail4->push_back(t->clone()); - multop::vec* head = new multop::vec; - for (unsigned j = 0; j < s; ++j) - head->push_back(f->nth(j)->clone()); - head4->push_back(multop::instance(op, head)); + head4->push_back(f->all_but(s)); (*i)->destroy(); *i = 0; } @@ -4155,6 +4141,8 @@ namespace spot // head1 tail1 // {b1:r1}&{b2:r2} = {b1∧b2}:{r1&r2} // head2 tail2 + // BEWARE: The second rule is correct only when + // both r1 and r2 do not accept [*0]. multop::vec* head1 = new multop::vec; multop::vec* tail1 = new multop::vec; @@ -4175,22 +4163,20 @@ namespace spot if (op == multop::Concat) { head1->push_back(h->clone()); - multop::vec* tail = new multop::vec; - unsigned s = f->size(); - for (unsigned j = 1; j < s; ++j) - tail->push_back(f->nth(j)->clone()); - tail1->push_back(multop::instance(op, tail)); + tail1->push_back(f->all_but(0)); (*i)->destroy(); *i = 0; } else if (op == multop::Fusion) { + const formula* t = f->all_but(0); + if (t->accepts_eword()) + { + t->destroy(); + continue; + } head2->push_back(h->clone()); - multop::vec* tail = new multop::vec; - unsigned s = f->size(); - for (unsigned j = 1; j < s; ++j) - tail->push_back(f->nth(j)->clone()); - tail2->push_back(multop::instance(op, tail)); + tail2->push_back(t); (*i)->destroy(); *i = 0; } @@ -4230,83 +4216,6 @@ namespace spot delete tail2; } - // {r1;b1}&{r2;b2} = {r1&r2};{b1∧b2} - // head3 tail3 - // {r1:b1}&{r2:b2} = {r1&r2}:{b1∧b2} - // head4 tail4 - multop::vec* head3 = new multop::vec; - multop::vec* tail3 = new multop::vec; - multop::vec* head4 = new multop::vec; - multop::vec* tail4 = new multop::vec; - for (multop::vec::iterator i = s.res_other->begin(); - i != s.res_other->end(); ++i) - { - if (!*i) - continue; - if ((*i)->kind() != formula::MultOp) - continue; - const multop* f = down_cast(*i); - unsigned s = f->size() - 1; - const formula* t = f->nth(s); - if (!t->is_boolean()) - continue; - multop::type op = f->op(); - if (op == multop::Concat) - { - tail3->push_back(t->clone()); - multop::vec* head = new multop::vec; - for (unsigned j = 0; j < s; ++j) - head->push_back(f->nth(j)->clone()); - head3->push_back(multop::instance(op, head)); - (*i)->destroy(); - *i = 0; - } - else if (op == multop::Fusion) - { - tail4->push_back(t->clone()); - multop::vec* head = new multop::vec; - for (unsigned j = 0; j < s; ++j) - head->push_back(f->nth(j)->clone()); - head4->push_back(multop::instance(op, head)); - (*i)->destroy(); - *i = 0; - } - else - { - continue; - } - } - if (!head3->empty()) - { - const formula* h = - multop::instance(multop::AndNLM, head3); - const formula* t = - multop::instance(multop::And, tail3); - const formula* f = - multop::instance(multop::Concat, h, t); - s.res_other->push_back(f); - } - else - { - delete head3; - delete tail3; - } - if (!head4->empty()) - { - const formula* h = - multop::instance(multop::AndNLM, head4); - const formula* t = - multop::instance(multop::And, tail4); - const formula* f = - multop::instance(multop::Fusion, h, t); - s.res_other->push_back(f); - } - else - { - delete head4; - delete tail4; - } - result_ = multop::instance(multop::AndNLM, s.res_other); // If we altered the formula in some way, process // it another time.