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": {}