From d1f915c748a82e5daa8a8299cd6b5639fe402440 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 17 Aug 2015 15:26:42 +0200 Subject: [PATCH] merge tunnabrev/lunnabrev/wmunabbrev into a single function * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh, src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh, src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh: Delete. * src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: New files. * src/ltlvisit/Makefile.am: Adjust. * src/ltlvisit/print.cc, src/tests/equalsf.cc, src/tests/Makefile.am, src/twaalgos/ltl2taa.cc, wrap/python/spot_impl.i, src/bin/ltlfilt.cc: Adjust callers. * src/ltlvisit/contain.cc, src/tests/syntimpl.cc: Remove useless include. * wrap/python/tests/formulas.ipynb: New test cases. * doc/tl/tl.tex: Group all rules in a single section. * NEWS: Mention it. --- NEWS | 5 + doc/tl/tl.tex | 54 +++---- src/bin/ltlfilt.cc | 4 +- src/ltlvisit/Makefile.am | 8 +- src/ltlvisit/contain.cc | 1 - src/ltlvisit/lunabbrev.cc | 149 ------------------- src/ltlvisit/lunabbrev.hh | 75 ---------- src/ltlvisit/print.cc | 12 +- src/ltlvisit/tunabbrev.cc | 80 ---------- src/ltlvisit/tunabbrev.hh | 69 --------- src/ltlvisit/unabbrev.cc | 243 +++++++++++++++++++++++++++++++ src/ltlvisit/unabbrev.hh | 72 +++++++++ src/ltlvisit/wmunabbrev.cc | 96 ------------ src/ltlvisit/wmunabbrev.hh | 41 ------ src/tests/Makefile.am | 6 +- src/tests/equalsf.cc | 24 +-- src/tests/syntimpl.cc | 2 - src/twaalgos/ltl2taa.cc | 9 +- wrap/python/spot_impl.i | 6 +- wrap/python/tests/formulas.ipynb | 65 ++++++++- 20 files changed, 427 insertions(+), 594 deletions(-) delete mode 100644 src/ltlvisit/lunabbrev.cc delete mode 100644 src/ltlvisit/lunabbrev.hh delete mode 100644 src/ltlvisit/tunabbrev.cc delete mode 100644 src/ltlvisit/tunabbrev.hh create mode 100644 src/ltlvisit/unabbrev.cc create mode 100644 src/ltlvisit/unabbrev.hh delete mode 100644 src/ltlvisit/wmunabbrev.cc delete mode 100644 src/ltlvisit/wmunabbrev.hh diff --git a/NEWS b/NEWS index 3e3703bca..5f3fea5b7 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,11 @@ New in spot 1.99.2a (not yet released) SCCs, but it now does remove Fin marks from transitions between SCCs. + * All the unabbreviation functions (unabbreviate_ltl(), + unabbreviate_logic(), unabbreviate_wm()) have been merged into a + single unabbreviate() function that takes a string representing + the list of rewritting rules to enable. + * Bugs fixed - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3) were not detected as generalized-Rabin. diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 3de918c20..ea75b81d0 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -466,17 +466,6 @@ considered equal for the purpose of the above identities. For instance \samp{(a\&c\&b\&!d)->(c\&!d\&b\&a)} will be rewritten to \samp{1} automatically. -\subsection{Unabbreviations}\label{sec:unabbbool} - -The `\verb=unabbreviate_logic()=' function rewrites all Boolean -operators using only the \samp{!}, \samp{\&}, and \samp{|} operators -using the following rewritings: -\begin{align*} - f\IMPLIES g &\equiv (\NOT f)\OR g\\ - f\EQUIV g &\equiv (f\AND g)\OR ((\NOT g)\AND(\NOT f))\\ - f\XOR g &\equiv (f\AND\NOT g)\OR (g\AND\NOT f)\\ -\end{align*} - \section{Temporal Operators}\label{sec:ltlops} Given two temporal formulas $f$, and $g$, the following @@ -554,25 +543,6 @@ $\M$, and $\W$ if you are only familiar with $\X$ and $\U$. f\R f&\equiv f \end{align*} -\subsection{Unabbreviations} - -The `\verb=unabbreviate_ltl()=' function applies all the rewritings from -section~\ref{sec:unabbbool} as well as the following two rewritings: -\begin{align*} - \F f&\equiv \1\U f\\ - \G f&\equiv \0\R f -\end{align*} - -The `\verb=unabbreviate_wm()=` function removes only the $\W$ and $\M$ -operators using the following two rewritings: -\begin{align*} - f \W g&\equiv g \R (g \OR f)\\ - f \M g&\equiv g \U (g \AND f) -\end{align*} -Among all the possible rewritings (see Appendix~\ref{sec:ltl-equiv}) -those two were chosen because they are easier to translate in a -tableau construction~\cite[Fig.~11]{duret.11.vecos}. - \section{SERE Operators}\label{sec:sere} The ``SERE'' acronym will be translated to different word depending on @@ -1349,6 +1319,30 @@ b))\OR(a\AND b))$ if `\verb|nenoform_stop_on_boolean|' is unset, while it will produce $\G\F(\NOT(a \XOR b))$ if `\verb|nenoform_stop_on_boolean|' is set. +\section{Unabbreviations} + +The `\verb=unabbreviate()=' function can apply the following rewriting +rules when passed a string denoting the list of rules to apply. For +instance passing the string \texttt{"\^{}ei"} will rewrite all +occurrences of $\XOR$, $\EQUIV$ and $\IMPLIES$. + +\[ +\begin{array}{lrcl} +``\texttt{i}" & f\IMPLIES g &\equiv& (\NOT f)\OR g\\ +``\texttt{e}" & f\EQUIV g &\equiv& (f\AND g)\OR ((\NOT g)\AND(\NOT f))\\ +``\texttt{\^{}e}" & f\XOR g &\equiv& (f\AND\NOT g)\OR (g\AND\NOT f)\\ +``\texttt{\^{}}"\text{~without~}``\texttt{e}" & f\XOR g &\equiv& \NOT(f\EQUIV g)\\ +``\texttt{F}" & \F f&\equiv& \1\U f\\ +``\texttt{G}" & \G f&\equiv& \0\R f \\ +``\texttt{W}" & f \W g&\equiv& g \R (g \OR f)\\ +``\texttt{M}" & f \M g&\equiv& g \U (g \AND f) +\end{array} +\] + +Among all the possible rewritings (see Appendix~\ref{sec:ltl-equiv}) +for $\W$ and $\M$, those two were chosen because they are easier to +translate in a tableau construction~\cite[Fig.~11]{duret.11.vecos}. + \section{Simplifications} The `\verb|ltl_simplifier::simplify|' method performs several kinds of diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 14c3d66c9..f83a928d7 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -38,7 +38,7 @@ #include "ltlvisit/simplify.hh" #include "ltlvisit/length.hh" #include "ltlvisit/relabel.hh" -#include "ltlvisit/wmunabbrev.hh" +#include "ltlvisit/unabbrev.hh" #include "ltlvisit/remove_x.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/exclusive.hh" @@ -562,7 +562,7 @@ namespace if (remove_wm) { - const spot::ltl::formula* res = spot::ltl::unabbreviate_wm(f); + const spot::ltl::formula* res = spot::ltl::unabbreviate(f, "WM"); f->destroy(); f = res; } diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 15b62810c..e1d6f5e3d 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -33,7 +33,6 @@ ltlvisit_HEADERS = \ dump.hh \ exclusive.hh \ length.hh \ - lunabbrev.hh \ mutation.hh \ nenoform.hh \ print.hh \ @@ -44,8 +43,7 @@ ltlvisit_HEADERS = \ simpfg.hh \ simplify.hh \ snf.hh \ - tunabbrev.hh \ - wmunabbrev.hh + unabbrev.hh noinst_LTLIBRARIES = libltlvisit.la libltlvisit_la_SOURCES = \ @@ -56,7 +54,6 @@ libltlvisit_la_SOURCES = \ dump.cc \ exclusive.cc \ length.cc \ - lunabbrev.cc \ mark.cc \ mark.hh \ mutation.cc \ @@ -69,5 +66,4 @@ libltlvisit_la_SOURCES = \ simpfg.cc \ simplify.cc \ snf.cc \ - tunabbrev.cc \ - wmunabbrev.cc + unabbrev.cc diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index f8ba4e9b4..0b3e87fa7 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -22,7 +22,6 @@ #include "contain.hh" #include "simplify.hh" -#include "tunabbrev.hh" #include "ltlast/unop.hh" #include "ltlast/binop.hh" #include "ltlast/multop.hh" diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc deleted file mode 100644 index db22e6441..000000000 --- a/src/ltlvisit/lunabbrev.cc +++ /dev/null @@ -1,149 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). -// Copyright (C) 2003, 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 3 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 this program. If not, see . - -#include "ltlast/allnodes.hh" -#include "lunabbrev.hh" -#include - -namespace spot -{ - namespace ltl - { - - unabbreviate_logic_visitor::unabbreviate_logic_visitor(const char* opt) - { - while (*opt) - switch (char c = *opt++) - { - case '^': - rewrite_xor = true; - break; - case 'i': - rewrite_i = true; - break; - case 'e': - rewrite_e = true; - break; - default: - throw std::runtime_error - (std::string("unknown option for unabbreviate_logic_visitor(): ") - + c); - } - } - - unabbreviate_logic_visitor::~unabbreviate_logic_visitor() - { - } - - void - unabbreviate_logic_visitor::visit(const binop* bo) - { - const formula* f1 = recurse(bo->first()); - const formula* f2 = recurse(bo->second()); - binop::type op = bo->op(); - switch (op) - { - /* f1 ^ f2 == !(f1 <-> f2) */ - /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ - case binop::Xor: - { - if (!rewrite_xor) - goto no_rewrite; - if (!rewrite_e) - { - result_ = unop::instance(unop::Not, - binop::instance(binop::Equiv, f1, f2)); - return; - } - else - { - const formula* a = - multop::instance(multop::And, f1->clone(), - unop::instance(unop::Not, f2->clone())); - const formula* b = - multop::instance(multop::And, f2, - unop::instance(unop::Not, f1)); - result_ = multop::instance(multop::Or, a, b); - return; - } - } - /* f1 => f2 == !f1 | f2 */ - case binop::Implies: - if (!rewrite_i) - goto no_rewrite; - result_ = multop::instance(multop::Or, - unop::instance(unop::Not, f1), f2); - return; - /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ - case binop::Equiv: - if (!rewrite_e) - goto no_rewrite; - { - const formula* f1c = f1->clone(); - const formula* f2c = f2->clone(); - - result_ = - multop::instance(multop::Or, - multop::instance(multop::And, f1c, f2c), - multop::instance(multop::And, - unop::instance(unop::Not, f1), - unop::instance(unop::Not, f2))); - return; - } - /* f1 U f2 == f1 U f2 */ - /* f1 R f2 == f1 R f2 */ - /* f1 W f2 == f1 W f2 */ - /* f1 M f2 == f1 M f2 */ - /* f1 UConcat f2 == f1 UConcat f2 */ - /* f1 EConcat f2 == f1 EConcat f2 */ - case binop::U: - case binop::R: - case binop::W: - case binop::M: - case binop::UConcat: - case binop::EConcat: - case binop::EConcatMarked: - no_rewrite: - result_ = binop::instance(op, f1, f2); - return; - } - SPOT_UNREACHABLE(); - } - - const formula* - unabbreviate_logic_visitor::recurse(const formula* f) - { - f->accept(*this); - return result_; - } - - const formula* - unabbreviate_logic(const formula* f, const char* xie) - { - if (f->is_sugar_free_boolean()) - return f->clone(); - unabbreviate_logic_visitor v(xie); - f->accept(v); - return v.result(); - } - } -} diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh deleted file mode 100644 index 98c5f7441..000000000 --- a/src/ltlvisit/lunabbrev.hh +++ /dev/null @@ -1,75 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 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 3 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 this program. If not, see . - -#pragma once - -#include "clone.hh" - -namespace spot -{ - namespace ltl - { - /// \ingroup ltl_visitor - /// \brief Clone and rewrite a formula to remove most of the - /// abbreviated logical operators. - /// - /// This will rewrite binary operators such as binop::Implies, - /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, - /// and multop::And. - /// - /// This visitor is public, because it's convenient - /// to derive from it and override some of its methods. - /// But if you just want the functionality, consider using - /// spot::ltl::unabbreviate_logic instead. - class SPOT_API unabbreviate_logic_visitor : public clone_visitor - { - typedef clone_visitor super; - public: - unabbreviate_logic_visitor(const char* opt = "^ie"); - virtual ~unabbreviate_logic_visitor(); - - using super::visit; - void visit(const binop* bo); - - virtual const formula* recurse(const formula* f); - private: - bool rewrite_xor = false; - bool rewrite_i = false; - bool rewrite_e = false; - }; - - /// \ingroup ltl_rewriting - /// \brief Clone and rewrite a formula to remove most of the abbreviated - /// logical operators. - /// - /// This will rewrite binary operators such as binop::Implies, - /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, - /// and multop::And. - /// - /// The optional \a opt argument can be a string containing any - /// subset of the string "^ie" to denote the operators (xor, - /// implication, equivalence) to actually remove. - SPOT_API const formula* unabbreviate_logic(const formula* f, - const char* opt = "^ie"); - - } -} diff --git a/src/ltlvisit/print.cc b/src/ltlvisit/print.cc index c6162d513..36e58b7fe 100644 --- a/src/ltlvisit/print.cc +++ b/src/ltlvisit/print.cc @@ -27,8 +27,7 @@ #include #include "ltlast/allnodes.hh" #include "ltlast/visitor.hh" -#include "lunabbrev.hh" -#include "wmunabbrev.hh" +#include "unabbrev.hh" #include "print.hh" #include "misc/escape.hh" @@ -985,11 +984,7 @@ namespace spot std::ostream& print_spin_ltl(std::ostream& os, const formula* f, bool full_parent) { - // Rewrite xor. - const formula* fu = unabbreviate_logic(f, "^"); - // Also remove W and M. - f = unabbreviate_wm(fu); - fu->destroy(); + f = unabbreviate(f, "^MW"); to_string_visitor v(os, full_parent, false, spin_kw); f->accept(v); f->destroy(); @@ -1007,8 +1002,7 @@ namespace spot std::ostream& print_wring_ltl(std::ostream& os, const formula* f) { - // Remove W and M. - f = unabbreviate_wm(f); + f = unabbreviate(f, "MW"); to_string_visitor v(os, true, false, wring_kw); f->accept(v); f->destroy(); diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc deleted file mode 100644 index 973566fd3..000000000 --- a/src/ltlvisit/tunabbrev.cc +++ /dev/null @@ -1,80 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2003 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 3 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 this program. If not, see . - -#include "ltlast/allnodes.hh" -#include "tunabbrev.hh" - -namespace spot -{ - namespace ltl - { - unabbreviate_ltl_visitor::unabbreviate_ltl_visitor() - { - } - - unabbreviate_ltl_visitor::~unabbreviate_ltl_visitor() - { - } - - void - unabbreviate_ltl_visitor::visit(const unop* uo) - { - switch (uo->op()) - { - case unop::X: - case unop::Not: - case unop::Closure: - case unop::NegClosure: - case unop::NegClosureMarked: - this->super::visit(uo); - return; - case unop::F: - result_ = binop::instance(binop::U, - constant::true_instance(), - recurse(uo->child())); - return; - case unop::G: - result_ = binop::instance(binop::R, - constant::false_instance(), - recurse(uo->child())); - return; - } - } - - const formula* - unabbreviate_ltl_visitor::recurse(const formula* f) - { - return unabbreviate_ltl(f); - } - - const formula* - unabbreviate_ltl(const formula* f) - { - if (f->is_sugar_free_boolean() && f->is_sugar_free_ltl()) - return f->clone(); - unabbreviate_ltl_visitor v; - f->accept(v); - return v.result(); - } - - } -} diff --git a/src/ltlvisit/tunabbrev.hh b/src/ltlvisit/tunabbrev.hh deleted file mode 100644 index c22d68cee..000000000 --- a/src/ltlvisit/tunabbrev.hh +++ /dev/null @@ -1,69 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). -// Copyright (C) 2003, 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 3 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 this program. If not, see . - -#pragma once - -#include "ltlast/formula.hh" -#include "ltlvisit/lunabbrev.hh" - -namespace spot -{ - namespace ltl - { - /// \ingroup ltl_visitor - /// \brief Clone and rewrite a formula to remove most of the - /// abbreviated LTL and logical operators. - /// - /// The rewriting performed on logical operator is - /// the same as the one done by spot::ltl::unabbreviate_logic_visitor. - /// - /// This will also rewrite unary operators such as unop::F, - /// and unop::G, using only binop::U, and binop::R. - /// - /// This visitor is public, because it's convenient - /// to derive from it and override some of its methods. - /// But if you just want the functionality, consider using - /// spot::ltl::unabbreviate_ltl instead. - class SPOT_API unabbreviate_ltl_visitor : public unabbreviate_logic_visitor - { - typedef unabbreviate_logic_visitor super; - public: - unabbreviate_ltl_visitor(); - virtual ~unabbreviate_ltl_visitor(); - - using super::visit; - void visit(const unop* uo); - - const formula* recurse(const formula* f); - }; - - /// \brief Clone and rewrite a formula to remove most of the - /// abbreviated LTL and logical operators. - /// - /// The rewriting performed on logical operator is - /// the same as the one done by spot::ltl::unabbreviate_logic. - /// - /// This will also rewrite unary operators such as unop::F, - /// and unop::G, using only binop::U, and binop::R. - SPOT_API const formula* unabbreviate_ltl(const formula* f); - } -} diff --git a/src/ltlvisit/unabbrev.cc b/src/ltlvisit/unabbrev.cc new file mode 100644 index 000000000..80ae9424f --- /dev/null +++ b/src/ltlvisit/unabbrev.cc @@ -0,0 +1,243 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// 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 3 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 this program. If not, see . + + +#include "unabbrev.hh" +#include "ltlast/allnodes.hh" +#include + +namespace spot +{ + namespace ltl + { + unabbreviator::unabbreviator(const char* opt) + { + while (*opt) + switch (char c = *opt++) + { + case 'e': + re_e_ = true; + re_some_bool_ = true; + break; + case 'F': + re_f_ = true; + re_some_f_g_ = true; + break; + case 'G': + re_g_ = true; + re_some_f_g_ = true; + break; + case 'i': + re_i_ = true; + re_some_bool_ = true; + break; + case 'M': + re_m_ = true; + re_some_other_ = true; + break; + case 'W': + re_w_ = true; + re_some_other_ = true; + break; + case '^': + re_xor_ = true; + re_some_bool_ = true; + break; + default: + throw std::runtime_error + (std::string("unknown unabbreviation option: ") + + c); + } + } + + unabbreviator::~unabbreviator() + { + auto i = cache_.begin(); + auto end = cache_.end(); + while (i != end) + { + auto old = i++; + old->second->destroy(); + old->first->destroy(); + } + } + + + const formula* unabbreviator::run(const formula* in) + { + auto entry = cache_.emplace(in, nullptr); + if (!entry.second) + return entry.first->second->clone(); + in->clone(); + + // Skip recursion whenever possible + bool no_boolean_rewrite = !re_some_bool_ || in->is_sugar_free_boolean(); + bool no_f_g_rewrite = !re_some_f_g_ || in->is_sugar_free_ltl(); + if (no_boolean_rewrite + && (in->is_boolean() || (no_f_g_rewrite && !re_some_other_))) + { + entry.first->second = in->clone(); + return in->clone(); + } + + const formula* out = nullptr; + switch (in->kind()) + { + case formula::AtomicProp: + case formula::Constant: + out = in->clone(); + break; + case formula::UnOp: + { + const unop* uo = static_cast(in); + auto c = run(uo->child()); + switch (auto op = uo->op()) + { + // F f1 = true U f1 + case unop::F: + if (!re_f_) + goto unop_clone; + out = binop::instance(binop::U, constant::true_instance(), c); + break; + // G f1 = false R f1 + case unop::G: + if (!re_g_) + goto unop_clone; + out = binop::instance(binop::R, constant::false_instance(), c); + break; + case unop::Not: + case unop::X: + case unop::Closure: + case unop::NegClosure: + case unop::NegClosureMarked: + unop_clone: + out = unop::instance(op, c); + break; + } + break; + } + case formula::BinOp: + { + const binop* bo = static_cast(in); + auto f1 = run(bo->first()); + auto f2 = run(bo->second()); + switch (auto op = bo->op()) + { + // f1 ^ f2 == !(f1 <-> f2) + // f1 ^ f2 == (f1 & !f2) | (f2 & !f1) + case binop::Xor: + { + if (!re_xor_) + goto binop_clone; + if (!re_e_) + { + out = unop::instance(unop::Not, + binop::instance(binop::Equiv, + f1, f2)); + } + else + { + auto a = multop::instance(multop::And, f1->clone(), + unop::instance(unop::Not, + f2->clone())); + auto b = multop::instance(multop::And, f2, + unop::instance(unop::Not, f1)); + out = multop::instance(multop::Or, a, b); + } + break; + } + // f1 => f2 == !f1 | f2 + case binop::Implies: + if (!re_i_) + goto binop_clone; + out = multop::instance(multop::Or, + unop::instance(unop::Not, f1), f2); + break; + // f1 <=> f2 == (f1 & f2) | (!f1 & !f2) + case binop::Equiv: + if (!re_e_) + goto binop_clone; + { + auto nf1 = unop::instance(unop::Not, f1->clone()); + auto nf2 = unop::instance(unop::Not, f2->clone()); + auto term1 = multop::instance(multop::And, f1, f2); + auto term2 = multop::instance(multop::And, nf1, nf2); + out = multop::instance(multop::Or, term1, term2); + break; + } + // f1 W f2 = f2 R (f2 | f1) + case binop::W: + if (!re_w_) + goto binop_clone; + out = binop::instance(binop::R, f2, + multop::instance(multop::Or, + f2->clone(), f1)); + break; + // f1 M f2 = f2 U (g2 & f1) + case binop::M: + if (!re_m_) + goto binop_clone; + out = binop::instance(binop::U, f2, + multop::instance(multop::And, + f2->clone(), f1)); + break; + case binop::U: + case binop::R: + case binop::UConcat: + case binop::EConcat: + case binop::EConcatMarked: + binop_clone: + out = binop::instance(op, f1, f2); + break; + } + break; + } + case formula::MultOp: + { + const multop* mo = static_cast(in); + multop::vec* res = new multop::vec; + unsigned mos = mo->size(); + res->reserve(mos); + for (unsigned i = 0; i < mos; ++i) + res->push_back(run(mo->nth(i))); + out = multop::instance(mo->op(), res); + break; + } + case formula::BUnOp: + { + const bunop* bo = static_cast(in); + out = bunop::instance(bo->op(), run(bo->child()), + bo->min(), bo->max()); + break; + } + } + + assert(out != nullptr); + + entry.first->second = out; + return out->clone(); + } + + const formula* unabbreviate(const formula* in, const char* opt) + { + unabbreviator un(opt); + return un.run(in); + } + } +} diff --git a/src/ltlvisit/unabbrev.hh b/src/ltlvisit/unabbrev.hh new file mode 100644 index 000000000..047866b91 --- /dev/null +++ b/src/ltlvisit/unabbrev.hh @@ -0,0 +1,72 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// 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 3 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 this program. If not, see . + +#pragma once + +#include "ltlast/formula.hh" +#include + +namespace spot +{ + namespace ltl + { + constexpr const char* default_unabbrev_string = "eFGiMW^"; + + /// \ingroup ltl_rewriting + /// \brief Clone and rewrite a formula to remove specified operators + /// logical operators. + class SPOT_API unabbreviator final + { + private: + // What to rewrite? + bool re_e_ = false; + bool re_f_ = false; + bool re_g_ = false; + bool re_i_ = false; + bool re_m_ = false; + bool re_w_ = false; + bool re_xor_ = false; + bool re_some_bool_ = false; // rewrite xor, i, or e + bool re_some_f_g_ = false; // rewrite F or G + bool re_some_other_ = false; // rewrite W or M + // Cache of rewritten subformulas + std::unordered_map cache_; + public: + /// \brief Constructor + /// + /// The set of operators to remove should be passed as a string + /// which in which each letter denote an operator (using LBT's + /// convention). + unabbreviator(const char* opt = default_unabbrev_string); + const formula* run(const formula* in); + ~unabbreviator(); + }; + + /// \ingroup ltl_rewriting + /// \brief Clone and rewrite a formula to remove specified operators + /// logical operators. + /// + /// The set of operators to remove should be passed as a string + /// which in which each letter denote an operator (using LBT's + /// convention). + SPOT_API const formula* + unabbreviate(const formula* in, const char* opt= default_unabbrev_string); + } + +} diff --git a/src/ltlvisit/wmunabbrev.cc b/src/ltlvisit/wmunabbrev.cc deleted file mode 100644 index 6da3b94f5..000000000 --- a/src/ltlvisit/wmunabbrev.cc +++ /dev/null @@ -1,96 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// 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 3 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 this program. If not, see . - -#include "ltlast/allnodes.hh" -#include "clone.hh" -#include "wmunabbrev.hh" -#include - -namespace spot -{ - namespace ltl - { - namespace - { - class unabbreviate_wm_visitor : public clone_visitor - { - typedef clone_visitor super; - public: - unabbreviate_wm_visitor() - { - } - - virtual - ~unabbreviate_wm_visitor() - { - } - - using super::visit; - void visit(const binop* bo) - { - const formula* f1 = recurse(bo->first()); - const formula* f2 = recurse(bo->second()); - binop::type op = bo->op(); - switch (op) - { - case binop::Xor: - case binop::Implies: - case binop::Equiv: - case binop::U: - case binop::R: - case binop::UConcat: - case binop::EConcat: - case binop::EConcatMarked: - result_ = binop::instance(op, f1, f2); - break; - case binop::W: - // f1 W f2 = f2 R (f2 | f1) - result_ = - binop::instance(binop::R, f2, - multop::instance(multop::Or, - f2->clone(), f1)); - break; - case binop::M: - // f1 M f2 = f2 U (g2 & f1) - result_ = - binop::instance(binop::U, f2, - multop::instance(multop::And, - f2->clone(), f1)); - break; - } - } - - virtual const formula* recurse(const formula* f) - { - if (f->is_boolean()) - return f->clone(); - f->accept(*this); - return this->result(); - } - }; - } - - const formula* - unabbreviate_wm(const formula* f) - { - unabbreviate_wm_visitor v; - return v.recurse(f); - } - } -} diff --git a/src/ltlvisit/wmunabbrev.hh b/src/ltlvisit/wmunabbrev.hh deleted file mode 100644 index 6f755df85..000000000 --- a/src/ltlvisit/wmunabbrev.hh +++ /dev/null @@ -1,41 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// 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 3 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 this program. If not, see . - -#pragma once - -#include "misc/common.hh" - -namespace spot -{ - namespace ltl - { - class formula; - - /// \ingroup ltl_rewriting - /// \brief Rewrite a formula to remove the W and M operators. - /// - /// This is necessary if you want to use the formula with a tool - /// that do not support these operators. - /// - /// a W b is replaced by b R (b | a), - /// and a M b is replaced by b U (b & a). - /// - SPOT_API const formula* unabbreviate_wm(const formula* f); - } -} diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index aaa430374..c89713b08 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -92,7 +92,7 @@ ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY ltl2text_SOURCES = readltl.cc ltlrel_SOURCES = ltlrel.cc lunabbrev_SOURCES = equalsf.cc -lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV +lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ie"' nenoform_SOURCES = equalsf.cc nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM nequals_SOURCES = equalsf.cc @@ -107,9 +107,9 @@ reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR syntimpl_SOURCES = syntimpl.cc tostring_SOURCES = tostring.cc tunabbrev_SOURCES = equalsf.cc -tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV +tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"' tunenoform_SOURCES = equalsf.cc -tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV +tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"' # Keep this sorted by STRENGTH. Test basic things first, diff --git a/src/tests/equalsf.cc b/src/tests/equalsf.cc index 8d4e1238f..6ddcd93a6 100644 --- a/src/tests/equalsf.cc +++ b/src/tests/equalsf.cc @@ -27,10 +27,8 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/lunabbrev.hh" -#include "ltlvisit/tunabbrev.hh" +#include "ltlvisit/unabbrev.hh" #include "ltlvisit/dump.hh" -#include "ltlvisit/wmunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/simplify.hh" @@ -118,26 +116,12 @@ main(int argc, char** argv) int exit_code = 0; { -#if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM +#if defined UNABBREV || defined NENOFORM const spot::ltl::formula* tmp; #endif -#ifdef LUNABBREV +#ifdef UNABBREV tmp = f1; - f1 = spot::ltl::unabbreviate_logic(f1); - tmp->destroy(); - spot::ltl::dump(std::cout, f1); - std::cout << std::endl; -#endif -#ifdef TUNABBREV - tmp = f1; - f1 = spot::ltl::unabbreviate_ltl(f1); - tmp->destroy(); - spot::ltl::dump(std::cout, f1); - std::cout << std::endl; -#endif -#ifdef WM - tmp = f1; - f1 = spot::ltl::unabbreviate_wm(f1); + f1 = spot::ltl::unabbreviate(f1, UNABBREV); tmp->destroy(); spot::ltl::dump(std::cout, f1); std::cout << std::endl; diff --git a/src/tests/syntimpl.cc b/src/tests/syntimpl.cc index 27c999a7a..7c9252112 100644 --- a/src/tests/syntimpl.cc +++ b/src/tests/syntimpl.cc @@ -24,8 +24,6 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/lunabbrev.hh" -#include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/print.hh" #include "ltlvisit/simplify.hh" diff --git a/src/twaalgos/ltl2taa.cc b/src/twaalgos/ltl2taa.cc index 92b484dc0..79c8fba8f 100644 --- a/src/twaalgos/ltl2taa.cc +++ b/src/twaalgos/ltl2taa.cc @@ -21,8 +21,7 @@ #include #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/lunabbrev.hh" -#include "ltlvisit/tunabbrev.hh" +#include "ltlvisit/unabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/contain.hh" #include "ltl2taa.hh" @@ -408,9 +407,9 @@ namespace spot ltl_to_taa(const ltl::formula* f, const bdd_dict_ptr& dict, bool refined_rules) { - // TODO: s/unabbreviate_ltl/unabbreviate_logic/ - const ltl::formula* f1 = ltl::unabbreviate_ltl(f); - const ltl::formula* f2 = ltl::negative_normal_form(f1); + // TODO: implement translation of F and G + auto f1 = ltl::unabbreviate(f, "^ieFG"); + auto f2 = ltl::negative_normal_form(f1); f1->destroy(); auto res = make_taa_tgba_formula(dict); diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 59e7054fd..d6dcfb93f 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -100,11 +100,10 @@ namespace std { #include "ltlvisit/apcollect.hh" #include "ltlvisit/dot.hh" #include "ltlvisit/dump.hh" -#include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/print.hh" #include "ltlvisit/simplify.hh" -#include "ltlvisit/tunabbrev.hh" +#include "ltlvisit/unabbrev.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/length.hh" #include "ltlvisit/remove_x.hh" @@ -265,11 +264,10 @@ namespace std { %include "ltlvisit/apcollect.hh" %include "ltlvisit/dot.hh" %include "ltlvisit/dump.hh" -%include "ltlvisit/lunabbrev.hh" %include "ltlvisit/nenoform.hh" %include "ltlvisit/print.hh" %include "ltlvisit/simplify.hh" -%include "ltlvisit/tunabbrev.hh" +%include "ltlvisit/unabbrev.hh" %include "ltlvisit/randomltl.hh" %include "ltlvisit/length.hh" %include "ltlvisit/remove_x.hh" diff --git a/wrap/python/tests/formulas.ipynb b/wrap/python/tests/formulas.ipynb index dab70972b..df761ef22 100644 --- a/wrap/python/tests/formulas.ipynb +++ b/wrap/python/tests/formulas.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:d2086d4faaecc1d0e5a0e29b958657ed86b034326b89a5513d3df6f35301a3e7" + "signature": "sha256:08d5f61ba93d2879f4f77ca0c4434c1a60ffcb195505e6065dd5a1c79e07c26a" }, "nbformat": 3, "nbformat_minor": 0, @@ -493,7 +493,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -522,6 +522,13 @@ ], "prompt_number": 16 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Etessami's rule for removing X (valid only in stutter-invariant formulas)" + ] + }, { "cell_type": "code", "collapsed": false, @@ -544,6 +551,60 @@ } ], "prompt_number": 17 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Removing abbreviated operators" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.formula(\"G(a xor b) -> F(a <-> b)\")\n", + "spot.unabbreviate(f, \"GF^\")" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "latex": [ + "$(\\bot \\mathbin{\\mathsf{R}} \\lnot (a \\leftrightarrow b)) \\rightarrow (\\top \\mathbin{\\mathsf{U}} (a \\leftrightarrow b))$" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 18, + "text": [ + "(0 R !(a <-> b)) -> (1 U (a <-> b))" + ] + } + ], + "prompt_number": 18 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.unabbreviate(f, \"GF^ei\")" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "latex": [ + "$(\\top \\mathbin{\\mathsf{U}} ((a \\land b) \\lor (\\lnot a \\land \\lnot b))) \\lor \\lnot (\\bot \\mathbin{\\mathsf{R}} ((\\lnot a \\land b) \\lor (a \\land \\lnot b)))$" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 19, + "text": [ + "(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))" + ] + } + ], + "prompt_number": 19 } ], "metadata": {}