Commit d1f915c7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 314a0165
...@@ -10,6 +10,11 @@ New in spot 1.99.2a (not yet released) ...@@ -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, but it now does remove Fin marks from transitions between
SCCs. 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 * Bugs fixed
- Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3) - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
were not detected as generalized-Rabin. were not detected as generalized-Rabin.
......
...@@ -466,17 +466,6 @@ considered equal for the purpose of the above identities. For ...@@ -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 instance \samp{(a\&c\&b\&!d)->(c\&!d\&b\&a)} will be rewritten to
\samp{1} automatically. \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} \section{Temporal Operators}\label{sec:ltlops}
Given two temporal formulas $f$, and $g$, the following 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$. ...@@ -554,25 +543,6 @@ $\M$, and $\W$ if you are only familiar with $\X$ and $\U$.
f\R f&\equiv f f\R f&\equiv f
\end{align*} \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} \section{SERE Operators}\label{sec:sere}
The ``SERE'' acronym will be translated to different word depending on 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 ...@@ -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 it will produce $\G\F(\NOT(a \XOR b))$ if
`\verb|nenoform_stop_on_boolean|' is set. `\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} \section{Simplifications}
The `\verb|ltl_simplifier::simplify|' method performs several kinds of The `\verb|ltl_simplifier::simplify|' method performs several kinds of
......
...@@ -38,7 +38,7 @@ ...@@ -38,7 +38,7 @@
#include "ltlvisit/simplify.hh" #include "ltlvisit/simplify.hh"
#include "ltlvisit/length.hh" #include "ltlvisit/length.hh"
#include "ltlvisit/relabel.hh" #include "ltlvisit/relabel.hh"
#include "ltlvisit/wmunabbrev.hh" #include "ltlvisit/unabbrev.hh"
#include "ltlvisit/remove_x.hh" #include "ltlvisit/remove_x.hh"
#include "ltlvisit/apcollect.hh" #include "ltlvisit/apcollect.hh"
#include "ltlvisit/exclusive.hh" #include "ltlvisit/exclusive.hh"
...@@ -562,7 +562,7 @@ namespace ...@@ -562,7 +562,7 @@ namespace
if (remove_wm) 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->destroy();
f = res; f = res;
} }
......
...@@ -33,7 +33,6 @@ ltlvisit_HEADERS = \ ...@@ -33,7 +33,6 @@ ltlvisit_HEADERS = \
dump.hh \ dump.hh \
exclusive.hh \ exclusive.hh \
length.hh \ length.hh \
lunabbrev.hh \
mutation.hh \ mutation.hh \
nenoform.hh \ nenoform.hh \
print.hh \ print.hh \
...@@ -44,8 +43,7 @@ ltlvisit_HEADERS = \ ...@@ -44,8 +43,7 @@ ltlvisit_HEADERS = \
simpfg.hh \ simpfg.hh \
simplify.hh \ simplify.hh \
snf.hh \ snf.hh \
tunabbrev.hh \ unabbrev.hh
wmunabbrev.hh
noinst_LTLIBRARIES = libltlvisit.la noinst_LTLIBRARIES = libltlvisit.la
libltlvisit_la_SOURCES = \ libltlvisit_la_SOURCES = \
...@@ -56,7 +54,6 @@ libltlvisit_la_SOURCES = \ ...@@ -56,7 +54,6 @@ libltlvisit_la_SOURCES = \
dump.cc \ dump.cc \
exclusive.cc \ exclusive.cc \
length.cc \ length.cc \
lunabbrev.cc \
mark.cc \ mark.cc \
mark.hh \ mark.hh \
mutation.cc \ mutation.cc \
...@@ -69,5 +66,4 @@ libltlvisit_la_SOURCES = \ ...@@ -69,5 +66,4 @@ libltlvisit_la_SOURCES = \
simpfg.cc \ simpfg.cc \
simplify.cc \ simplify.cc \
snf.cc \ snf.cc \
tunabbrev.cc \ unabbrev.cc
wmunabbrev.cc
...@@ -22,7 +22,6 @@ ...@@ -22,7 +22,6 @@
#include "contain.hh" #include "contain.hh"
#include "simplify.hh" #include "simplify.hh"
#include "tunabbrev.hh"
#include "ltlast/unop.hh" #include "ltlast/unop.hh"
#include "ltlast/binop.hh" #include "ltlast/binop.hh"
#include "ltlast/multop.hh" #include "ltlast/multop.hh"
......
// -*- 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 <http://www.gnu.org/licenses/>.
#include "ltlast/allnodes.hh"
#include "lunabbrev.hh"
#include <cassert>
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();
}
}
}
// -*- 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 <http://www.gnu.org/licenses/>.
#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");
}
}
...@@ -27,8 +27,7 @@ ...@@ -27,8 +27,7 @@
#include <cstring> #include <cstring>
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh" #include "ltlast/visitor.hh"
#include "lunabbrev.hh" #include "unabbrev.hh"
#include "wmunabbrev.hh"
#include "print.hh" #include "print.hh"
#include "misc/escape.hh" #include "misc/escape.hh"
...@@ -985,11 +984,7 @@ namespace spot ...@@ -985,11 +984,7 @@ namespace spot
std::ostream& std::ostream&
print_spin_ltl(std::ostream& os, const formula* f, bool full_parent) print_spin_ltl(std::ostream& os, const formula* f, bool full_parent)
{ {
// Rewrite xor. f = unabbreviate(f, "^MW");
const formula* fu = unabbreviate_logic(f, "^");
// Also remove W and M.
f = unabbreviate_wm(fu);
fu->destroy();
to_string_visitor v(os, full_parent, false, spin_kw); to_string_visitor v(os, full_parent, false, spin_kw);
f->accept(v); f->accept(v);
f->destroy(); f->destroy();
...@@ -1007,8 +1002,7 @@ namespace spot ...@@ -1007,8 +1002,7 @@ namespace spot
std::ostream& std::ostream&
print_wring_ltl(std::ostream& os, const formula* f) print_wring_ltl(std::ostream& os, const formula* f)
{ {
// Remove W and M. f = unabbreviate(f, "MW");
f = unabbreviate_wm(f);
to_string_visitor v(os, true, false, wring_kw); to_string_visitor v(os, true, false, wring_kw);
f->accept(v); f->accept(v);
f->destroy(); f->destroy();
......
// -*- 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 <http://www.gnu.org/licenses/>.
#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();
}
}
}
// -*- 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 <http://www.gnu.org/licenses/>.
#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);
}
}
// -*- 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.