diff --git a/ChangeLog b/ChangeLog index 4f1371754..9a30531e2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,14 @@ 2004-06-23 Alexandre Duret-Lutz + * src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files, + extracted from ... + * src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented + again. + * src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call + simplify_f_g() in addition to unabbreviate_logic(). + * src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES): + Add simpfg.cc and simpfg.hh. + * src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ... * src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match the function name. diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 90504e740..71e0b160e 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -35,6 +35,7 @@ ltlvisit_HEADERS = \ nenoform.hh \ postfix.hh \ reduce.hh \ + simpfg.hh \ syntimpl.hh \ tostring.hh \ tunabbrev.hh @@ -51,6 +52,7 @@ libltlvisit_la_SOURCES = \ nenoform.cc \ postfix.cc \ reduce.cc \ + simpfg.cc \ syntimpl.cc \ tostring.cc \ tunabbrev.cc diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index cc6b7013f..7c006a1e5 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -71,19 +71,11 @@ namespace spot unop::instance(unop::Not, f2))); return; - /* true U f2 == F(f2) */ - case binop::U: - if (f1 == constant::true_instance()) - result_ = unop::instance(unop::F, f2); - else - result_ = binop::instance(bo->op(), f1, f2); - return; - /* false R f2 == G(f2) */ + /* f1 U f2 == f1 U f2 */ + /* f1 R f2 == f1 R f2 */ + case binop::U: case binop::R: - if (f1 == constant::false_instance()) - result_ = unop::instance(unop::G, f2); - else - result_ = binop::instance(bo->op(), f1, f2); + result_ = binop::instance(bo->op(), f1, f2); return; } /* Unreachable code. */ diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 5a4d1871f..35b0e9f35 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -26,6 +26,7 @@ #include #include "lunabbrev.hh" +#include "simpfg.hh" #include "nenoform.hh" #include "ltlvisit/destroy.hh" @@ -293,8 +294,11 @@ namespace spot formula* f2; f1 = unabbreviate_logic(f); - f2 = negative_normal_form(f1); + f2 = simplify_f_g(f1); destroy(f1); + f1 = negative_normal_form(f2); + destroy(f2); + f2 = f1; if (opt & Reduce_Basics) { diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc new file mode 100644 index 000000000..fa143cfd9 --- /dev/null +++ b/src/ltlvisit/simpfg.cc @@ -0,0 +1,86 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "ltlast/allnodes.hh" +#include "ltlvisit/clone.hh" +#include "simpfg.hh" +#include + +namespace spot +{ + namespace ltl + { + + simplify_f_g_visitor::simplify_f_g_visitor() + { + } + + simplify_f_g_visitor::~simplify_f_g_visitor() + { + } + + void + simplify_f_g_visitor::visit(binop* bo) + { + formula* f1 = recurse(bo->first()); + formula* f2 = recurse(bo->second()); + + switch (bo->op()) + { + case binop::Xor: + case binop::Implies: + case binop::Equiv: + result_ = binop::instance(bo->op(), f1, f2); + return; + /* true U f2 == F(f2) */ + case binop::U: + if (f1 == constant::true_instance()) + result_ = unop::instance(unop::F, f2); + else + result_ = binop::instance(binop::U, f1, f2); + return; + /* false R f2 == G(f2) */ + case binop::R: + if (f1 == constant::false_instance()) + result_ = unop::instance(unop::G, f2); + else + result_ = binop::instance(binop::R, f1, f2); + return; + } + /* Unreachable code. */ + assert(0); + } + + formula* + simplify_f_g_visitor::recurse(formula* f) + { + return simplify_f_g(f); + } + + formula* + simplify_f_g(const formula* f) + { + simplify_f_g_visitor v; + const_cast(f)->accept(v); + return v.result(); + } + } +} diff --git a/src/ltlvisit/simpfg.hh b/src/ltlvisit/simpfg.hh new file mode 100644 index 000000000..8f01350cd --- /dev/null +++ b/src/ltlvisit/simpfg.hh @@ -0,0 +1,52 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_LTLVISIT_SIMPFG_HH +# define SPOT_LTLVISIT_SIMPFG_HH + +#include "clone.hh" + +namespace spot +{ + namespace ltl + { + /// \brief Replace true U f and false R g by + /// F f and G g. + class simplify_f_g_visitor : public clone_visitor + { + typedef clone_visitor super; + public: + simplify_f_g_visitor(); + virtual ~simplify_f_g_visitor(); + + using super::visit; + void visit(binop* bo); + + virtual formula* recurse(formula* f); + }; + + /// \brief Replace true U f and false R g by + /// F f and G g. + formula* simplify_f_g(const formula* f); + } +} + +#endif // SPOT_LTLVISIT_LUNABBREV_HH diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index e0e910015..8c404bcf6 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -24,6 +24,7 @@ #include #include "lunabbrev.hh" +#include "simpfg.hh" #include "nenoform.hh" #include "ltlvisit/destroy.hh" @@ -515,33 +516,32 @@ namespace spot bool syntactic_implication_neg(const formula* f1, const formula* f2, bool right) { - const formula* ftmp1; - const formula* ftmp2; - const formula* ftmp3 = unop::instance(unop::Not, - right ? clone(f2) : clone(f1)); - const formula* ftmp4 = negative_normal_form(right ? f1 : f2); - const formula* ftmp5; - const formula* ftmp6; - bool result; - - ftmp2 = unabbreviate_logic(ftmp3); - ftmp1 = negative_normal_form(ftmp2); - - ftmp5 = unabbreviate_logic(ftmp4); - ftmp6 = negative_normal_form(ftmp5); - + formula* l = clone(f1); + formula* r = clone(f2); if (right) - result = syntactic_implication(ftmp6, ftmp1); + r = unop::instance(unop::Not, r); else - result = syntactic_implication(ftmp1, ftmp6); + l = unop::instance(unop::Not, l); - destroy(ftmp1); - destroy(ftmp2); - destroy(ftmp3); - destroy(ftmp4); - destroy(ftmp5); - destroy(ftmp6); + formula* tmp = unabbreviate_logic(l); + destroy(l); + l = simplify_f_g(tmp); + destroy(tmp); + tmp = negative_normal_form(l); + destroy(l); + l = tmp; + tmp = unabbreviate_logic(r); + destroy(r); + r = simplify_f_g(tmp); + destroy(tmp); + tmp = negative_normal_form(r); + destroy(r); + r = tmp; + + bool result = syntactic_implication(l, r); + destroy(l); + destroy(r); return result; } }