From a09ad6b4c6f5d513b98b15a2fb3733a2affd16bb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 29 Apr 2012 21:21:03 +0200 Subject: [PATCH] Implement W,M removal for Spin output. * src/ltlvisit/wmunabbrev.hh, src/ltlvisit/wmunabbrev.cc: New files. * src/ltlvisit/Makefile.am: Add them. * src/ltlvisit/tostring.cc (to_spin_string): Use the new rewriting. * wrap/python/ajax/spot.in: Warn when a "Spin" still contain PSL operators. * wrap/python/ajax/ltl2tgba.html: Adjust help text. * doc/tl/tl.tex, NEWS: Document the new rewriting. --- NEWS | 6 +++ doc/tl/tl.tex | 18 ++++--- src/ltlvisit/Makefile.am | 6 ++- src/ltlvisit/tostring.cc | 12 +++-- src/ltlvisit/wmunabbrev.cc | 96 ++++++++++++++++++++++++++++++++++ src/ltlvisit/wmunabbrev.hh | 44 ++++++++++++++++ wrap/python/ajax/ltl2tgba.html | 4 +- wrap/python/ajax/spot.in | 5 ++ 8 files changed, 176 insertions(+), 15 deletions(-) create mode 100644 src/ltlvisit/wmunabbrev.cc create mode 100644 src/ltlvisit/wmunabbrev.hh diff --git a/NEWS b/NEWS index 7a7e4c11a..0018b9125 100644 --- a/NEWS +++ b/NEWS @@ -33,6 +33,12 @@ New in spot 0.8.3a: - A new direct simulation reduction has been implemented. It works directly on TGBAs. It is in src/tgbaalgos/simlation.hh, and it can be tested via ltl2tgba's -RDS option. + - unabbreviate_wm() is a function that rewrite the W and M operators + of LTL formulae using R and U. This is called whenever we output + a formula in Spin syntax. By combining this with the aforementioned + PSL rewriting rules, many PSL formulae that use simple SERE can be + converted into LTL formulae that can be feed to tools that only + understand U and R. The web interface will let you do this. - changes to the on-line translator: + SVG output is available + can display some properties of a formula diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 8690bcb08..900f6e626 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -456,9 +456,9 @@ instance \samp{(a\&c\&b\&!d)->(c\&!d\&b\&a)} will be rewritten to \subsection{Unabbreviations}\label{sec:unabbbool} -The `\verb=unabbreviate_logic_visitor=' rewrites all Boolean operators -using only the \samp{!}, \samp{\&}, and \samp{|} operators using the -following rewritings: +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))\\ @@ -544,16 +544,20 @@ and $\W$ if you are only familiar with $\X$ and $\U$. \subsection{Unabbreviations} -The `\verb=unabbreviate_ltl_visitor=' applies all the rewritings from +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*} -\spottodo[inline]{Spot should offer some way to rewrite a formula to - selectively remove $\U$, $\R$, $\M$, or $\W$, using the equivalences - from Appendix~\ref{sec:ltl-equiv}.} +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*} \section{SERE Operators} diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 2b17b61c2..22457c3fe 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -45,7 +45,8 @@ ltlvisit_HEADERS = \ simplify.hh \ snf.hh \ tostring.hh \ - tunabbrev.hh + tunabbrev.hh \ + wmunabbrev.hh noinst_LTLIBRARIES = libltlvisit.la libltlvisit_la_SOURCES = \ @@ -66,4 +67,5 @@ libltlvisit_la_SOURCES = \ simplify.cc \ snf.cc \ tostring.cc \ - tunabbrev.cc + tunabbrev.cc \ + wmunabbrev.cc diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 173250bdb..1fc33950a 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -30,6 +30,7 @@ #include "ltlast/allnodes.hh" #include "ltlast/visitor.hh" #include "lunabbrev.hh" +#include "wmunabbrev.hh" #include "tostring.hh" @@ -108,8 +109,8 @@ namespace spot " <-> ", // rewritten " U ", " V ", - " W ", // not supported - " M ", // not supported + " W ", // rewritten + " M ", // rewritten "<>-> ", // not supported "<>=> ", // not supported "<>+> ", // not supported @@ -754,9 +755,12 @@ namespace spot { // Remove xor, ->, and <-> first. formula* fu = unabbreviate_logic(f); - to_string_visitor v(os, full_parent, false, spin_kw); - fu->accept(v); + // Also remove W and M. + f = unabbreviate_wm(fu); fu->destroy(); + to_string_visitor v(os, full_parent, false, spin_kw); + f->accept(v); + f->destroy(); return os; } diff --git a/src/ltlvisit/wmunabbrev.cc b/src/ltlvisit/wmunabbrev.cc new file mode 100644 index 000000000..f16a6196a --- /dev/null +++ b/src/ltlvisit/wmunabbrev.cc @@ -0,0 +1,96 @@ +// -*- 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 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "ltlast/allnodes.hh" +#include "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(binop* bo) + { + formula* f1 = recurse(bo->first()); + 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->clone(), + multop::instance(multop::Or, f2, f1)); + break; + case binop::M: + // f1 M f2 = f2 U (g2 & f1) + result_ = + binop::instance(binop::U, f2->clone(), + multop::instance(multop::And, f2, f1)); + break; + } + } + + virtual formula* recurse(formula* f) + { + if (f->is_boolean()) + return f->clone(); + f->accept(*this); + return this->result(); + } + }; + } + + formula* + unabbreviate_wm(const formula* f) + { + unabbreviate_wm_visitor v; + return v.recurse(const_cast(f)); + } + } +} diff --git a/src/ltlvisit/wmunabbrev.hh b/src/ltlvisit/wmunabbrev.hh new file mode 100644 index 000000000..3b1e90b26 --- /dev/null +++ b/src/ltlvisit/wmunabbrev.hh @@ -0,0 +1,44 @@ +// -*- 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 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_LTLVISIT_WMUNABBREV_HH +# define SPOT_LTLVISIT_WMUNABBREV_HH + +namespace spot +{ + namespace ltl + { + class formula; + + /// \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). + /// + /// \ingroup ltl_rewriting + formula* unabbreviate_wm(const formula* f); + } +} + +#endif // SPOT_LTLVISIT_WMUNABBREV_HH diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 71ab39b27..ff09002b5 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -402,11 +402,11 @@ an identifier: aUb is an atomic proposition, unlike
Output the (simplified) formula as:
-