fix Python bindings for relabeling_map, and document them
This fixes #61, and addresses one item of #14. * src/ltlvisit/relabel.hh: Use a map rather than a unordered_map, because the Swig binding for unordered_map do not seem functional. * wrap/python/spot_impl.i: Adjust. * wrap/python/tests/relabel.py: New file. * wrap/python/tests/Makefile.am: Add it. * doc/org/tut02.org: New file. * doc/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz
parent
a8f5e7fd8b
commit
6c2985e753
6 changed files with 225 additions and 22 deletions
|
|
@ -79,6 +79,7 @@ ORG_FILES = \
|
|||
org/randltl.org \
|
||||
org/tools.org \
|
||||
org/tut01.org \
|
||||
org/tut02.org \
|
||||
org/satmin.org \
|
||||
org/satmin.tex \
|
||||
org/setup.org \
|
||||
|
|
|
|||
159
doc/org/tut02.org
Normal file
159
doc/org/tut02.org
Normal file
|
|
@ -0,0 +1,159 @@
|
|||
#+TITLE: Relabeling Formulas
|
||||
#+SETUPFILE: setup.org
|
||||
#+HTML_LINK_UP: tut.html
|
||||
|
||||
The task is to read an LTL formula, relabel all (possibly complex)
|
||||
atomic propositions, and provide =#define= statements for each of
|
||||
these renamings, writing everything in Spin's syntax.
|
||||
|
||||
|
||||
* Shell
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltlfilt -ps --relabel=pnn --define -f '"Proc@Here" U ("var > 10" | "var < 4")'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: #define p0 ((Proc@Here))
|
||||
: #define p1 ((var < 4))
|
||||
: #define p2 ((var > 10))
|
||||
: (p0) U ((p1) || (p2))
|
||||
|
||||
When is this output interesting, you may ask? It is useful for
|
||||
instance if you want to call =ltl2ba= (or any other LTL-to-Büchi
|
||||
translator) using a formula with complex atomic propositions it cannot
|
||||
parse. Then you can pass the rewritten formula to =ltl2ba=, and
|
||||
prepend all those =#define= to its output. For instance:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltlfilt -ps --relabel=pnn --define=tmp.defs -f '"Proc@Here" U ("var > 10" | "var < 4")' >tmp.ltl
|
||||
cat tmp.defs; ltl2ba -F tmp.ltl
|
||||
rm tmp.defs tmp.ltl
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
#define p0 ((Proc@Here))
|
||||
#define p1 ((var < 4))
|
||||
#define p2 ((var > 10))
|
||||
never { /* (p0) U ((p1) || (p2))
|
||||
*/
|
||||
T0_init:
|
||||
if
|
||||
:: (p0) -> goto T0_init
|
||||
:: (p1) || (p2) -> goto accept_all
|
||||
fi;
|
||||
accept_all:
|
||||
skip
|
||||
}
|
||||
#+end_example
|
||||
|
||||
|
||||
* Python
|
||||
|
||||
The =spot.relabel= function takes an optional third parameter that
|
||||
should be a =relabeling_map=. If supplied, this map is filled with
|
||||
pairs of atomic propositions of the form (new-name, old-name).
|
||||
|
||||
#+BEGIN_SRC python :results output :exports both
|
||||
import spot
|
||||
f = spot.formula('"Proc@Here" U ("var > 10" | "var < 4")')
|
||||
m = spot.relabeling_map()
|
||||
g = spot.relabel(f, spot.Pnn, m)
|
||||
for newname, oldname in m.items():
|
||||
print("#define {} ({})".format(newname.to_str(), oldname.to_str('spin', True)))
|
||||
print(g.to_str('spin', True))
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: #define p0 ((Proc@Here))
|
||||
: #define p1 ((var < 4))
|
||||
: #define p2 ((var > 10))
|
||||
: (p0) U ((p1) || (p2))
|
||||
|
||||
* C++
|
||||
|
||||
The =spot::ltl::relabeling_map= is just a =std::map= with a custom
|
||||
destructor.
|
||||
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both
|
||||
#include <string>
|
||||
#include <iostream>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/print.hh"
|
||||
#include "ltlvisit/relabel.hh"
|
||||
|
||||
int main()
|
||||
{
|
||||
std::string input = "\"Proc@Here\" U (\"var > 10\" | \"var < 4\")";
|
||||
spot::ltl::parse_error_list pel;
|
||||
const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, input, pel))
|
||||
{
|
||||
if (f)
|
||||
f->destroy();
|
||||
return 1;
|
||||
}
|
||||
spot::ltl::relabeling_map m;
|
||||
const spot::ltl::formula* g = spot::ltl::relabel(f, spot::ltl::Pnn, &m);
|
||||
for (auto& i: m)
|
||||
{
|
||||
std::cout << "#define ";
|
||||
print_psl(std::cout, i.first) << " (";
|
||||
print_spin_ltl(std::cout, i.second, true) << ")\n";
|
||||
}
|
||||
print_spin_ltl(std::cout, g, true) << '\n';
|
||||
g->destroy();
|
||||
f->destroy();
|
||||
return 0;
|
||||
}
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: #define p0 ((Proc@Here))
|
||||
: #define p1 ((var < 4))
|
||||
: #define p2 ((var > 10))
|
||||
: (p0) U ((p1) || (p2))
|
||||
|
||||
|
||||
* Additional comments
|
||||
|
||||
** Two ways to name atomic propositions
|
||||
|
||||
Instead of =--relabel=pnn= (or =spot.Pnn=, or =spot::ltl::Pnn=), you can
|
||||
actually use =--relabel=abc= (or =spot.Abc=, or =spot::ltl::Abc=) to have
|
||||
the atomic propositions named =a=, =b=, =c=, etc.
|
||||
|
||||
** Relabeling Boolean sub-expressions
|
||||
|
||||
Instead of relabeling each atomic proposition, you could decide to
|
||||
relabel each Boolean sub-expression:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltlfilt -ps --relabel-bool=pnn --define -f '"Proc@Here" U ("var > 10" | "var < 4")'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: #define p0 ((Proc@Here))
|
||||
: #define p1 ((var < 4) || (var > 10))
|
||||
: (p0) U (p1)
|
||||
|
||||
The relabeling routine is smart enough to not give different names
|
||||
to Boolean expressions that have some sub-expression in common.
|
||||
|
||||
For instance =a U (a & b)= will not be relabeled into =(p0) U (p1)=
|
||||
because that would hide the fact that both =p0= and =p1= check for
|
||||
=a=. Instead we get this:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltlfilt -ps --relabel-bool=pnn --define -f 'a U (a & b)'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: #define p0 ((a))
|
||||
: #define p1 ((b))
|
||||
: (p0) U ((p0) && (p1))
|
||||
|
||||
This "Boolean sub-expression" relabeling is available in Python and
|
||||
C++ via the =relabel_bse= function. The interface is identical to
|
||||
=relabel=.
|
||||
|
|
@ -21,6 +21,7 @@
|
|||
|
||||
#include "ltlast/formula.hh"
|
||||
#include "misc/hash.hh"
|
||||
#include <map>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -29,16 +30,17 @@ namespace spot
|
|||
enum relabeling_style { Abc, Pnn };
|
||||
|
||||
|
||||
struct relabeling_map: public std::unordered_map<const formula*,
|
||||
struct relabeling_map: public std::map<const formula*,
|
||||
const formula*,
|
||||
ptr_hash<formula>>
|
||||
formula_ptr_less_than>
|
||||
{
|
||||
void clear()
|
||||
{
|
||||
for (iterator i = begin(); i != end(); ++i)
|
||||
i->second->destroy();
|
||||
this->std::unordered_map<const formula*,
|
||||
const formula*, ptr_hash<formula>>::clear();
|
||||
iterator i = begin();
|
||||
while (i != end())
|
||||
i++->second->destroy();
|
||||
this->std::map<const formula*, const formula*,
|
||||
formula_ptr_less_than>::clear();
|
||||
}
|
||||
|
||||
~relabeling_map()
|
||||
|
|
|
|||
|
|
@ -32,6 +32,7 @@
|
|||
%include "std_string.i"
|
||||
%include "std_list.i"
|
||||
%include "std_set.i"
|
||||
%include "std_map.i"
|
||||
%include "exception.i"
|
||||
%include "typemaps.i"
|
||||
|
||||
|
|
@ -223,6 +224,28 @@ using namespace spot;
|
|||
%include "ltlast/unop.hh"
|
||||
%include "ltlast/visitor.hh"
|
||||
|
||||
namespace std {
|
||||
%template(atomic_prop_set) set<const spot::ltl::atomic_prop*,
|
||||
spot::ltl::formula_ptr_less_than>;
|
||||
|
||||
%template(mapff) map<const spot::ltl::formula*, const spot::ltl::formula*,
|
||||
spot::ltl::formula_ptr_less_than>;
|
||||
}
|
||||
|
||||
%{
|
||||
namespace swig {
|
||||
template <> struct traits<atomic_prop> {
|
||||
typedef pointer_category category;
|
||||
static const char* type_name() { return "spot::ltl::atomic_prop"; }
|
||||
};
|
||||
template <> struct traits<formula> {
|
||||
typedef pointer_category category;
|
||||
static const char* type_name() { return "spot::ltl::formula"; }
|
||||
};
|
||||
}
|
||||
%}
|
||||
|
||||
|
||||
%include "ltlenv/environment.hh"
|
||||
%include "ltlenv/defaultenv.hh"
|
||||
|
||||
|
|
@ -299,21 +322,6 @@ using namespace spot;
|
|||
|
||||
#undef ltl
|
||||
|
||||
|
||||
namespace std {
|
||||
%template(atomic_prop_set) set<const spot::ltl::atomic_prop*,
|
||||
spot::ltl::formula_ptr_less_than>;
|
||||
}
|
||||
|
||||
%{
|
||||
namespace swig {
|
||||
template <> struct traits<atomic_prop> {
|
||||
typedef pointer_category category;
|
||||
static const char* type_name() { return"atomic_prop const *"; }
|
||||
};
|
||||
}
|
||||
%}
|
||||
|
||||
%extend spot::ltl::formula {
|
||||
|
||||
// When comparing formula, make sure Python compare our
|
||||
|
|
|
|||
|
|
@ -49,5 +49,6 @@ TESTS = \
|
|||
piperead.ipynb \
|
||||
randaut.ipynb \
|
||||
randltl.ipynb \
|
||||
relabel.py \
|
||||
setxor.py \
|
||||
testingaut.ipynb
|
||||
|
|
|
|||
32
wrap/python/tests/relabel.py
Normal file
32
wrap/python/tests/relabel.py
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
# -*- mode: python; coding: utf-8 -*-
|
||||
# Copyright (C) 2015 Laboratoire de Recherche et Développement
|
||||
# de l'Epita
|
||||
#
|
||||
# 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/>.
|
||||
|
||||
import spot
|
||||
|
||||
f = spot.formula('GF(a & b) -> (FG(a & b) & Gc)')
|
||||
m = spot.relabeling_map()
|
||||
g = spot.relabel_bse(f, spot.Pnn, m)
|
||||
res = ""
|
||||
for old, new in m.items():
|
||||
res += "#define {} {}\n".format(old, new)
|
||||
res += str(g)
|
||||
print(res)
|
||||
assert(res == """#define p0 a & b
|
||||
#define p1 c
|
||||
GFp0 -> (FGp0 & Gp1)""")
|
||||
Loading…
Add table
Add a link
Reference in a new issue