Commit a09ad6b4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent e64a1bf5
......@@ -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
......
......@@ -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}
......
......@@ -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
......@@ -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;
}
......
// -*- 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 <cassert>
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<formula*>(f));
}
}
}
// -*- 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.
///
/// <code>a W b</code> is replaced by <code>b R (b | a)</code>,
/// and <code>a M b</code> is replaced by <code>b U (b & a)</code>.
///
/// \ingroup ltl_rewriting
formula* unabbreviate_wm(const formula* f);
}
}
#endif // SPOT_LTLVISIT_WMUNABBREV_HH
......@@ -402,11 +402,11 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<div>
<div id="tabs-of">
Output the (simplified) formula as:<br>
<label class="rtip" title="Use letter operators (such as <span class='formula'>G</span> or <span class='formula'>F</span>) when possible.">
<label class="rtip" title="Use letter operators (such as <span class='formula'>G</span> or <span class='formula'>F</span>) when possible, and unless UTF-8 output is activated.">
<INPUT type="radio" name="ff" value="o" checked>
text in Spot's syntax
</label><br>
<label class="rtip" title="This output can be given to Spin or any other tool using a similar syntax. Spot can also read it back.">
<label class="rtip" title="This output can be given to Spin or any other tool using a similar syntax. Spot can also read it back. Operators such as such as <span class='formula'>M</span> and <span class='formula'>W</span>, which are not supported by Spin are rewritten away.">
<INPUT type="radio" name="ff" value="i">
text in Spin's syntax
</label><br>
......
......@@ -395,6 +395,11 @@ if output_type == 'f':
elif formula_format == 'i':
unbufprint('<div class="formula spin-format">'
+ spot.to_spin_string(f) + '</div>')
if f.is_psl_formula() and not f.is_ltl_formula():
s = ''
if simpopt.reduce_size_strictly:
s = '<br><b>Try enabling larger formula rewritings.</b>'
unbufprint('<div class="error">The above formula contains PSL operators that Spin will not understand.%s</div>' % s)
elif formula_format == 'g':
render_formula(f)
elif formula_format == 'p':
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment