diff --git a/doc/Makefile.am b/doc/Makefile.am index c7176c4509d3d4dbae3b6b5aae0a0f0742f05250..59adeb6f2d61c4589ee70f5a270d10543efee97f 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -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 \ diff --git a/doc/org/tut02.org b/doc/org/tut02.org new file mode 100644 index 0000000000000000000000000000000000000000..06584971d7ab786eb627b0449ceff77f4b9b249f --- /dev/null +++ b/doc/org/tut02.org @@ -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 + #include + #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=. diff --git a/src/ltlvisit/relabel.hh b/src/ltlvisit/relabel.hh index 924efd177ffad1028a18455db9ffbdcbb6ed244e..17be94e43bd2c16b282b3b232b314c8bdbe67443 100644 --- a/src/ltlvisit/relabel.hh +++ b/src/ltlvisit/relabel.hh @@ -21,6 +21,7 @@ #include "ltlast/formula.hh" #include "misc/hash.hh" +#include namespace spot { @@ -29,16 +30,17 @@ namespace spot enum relabeling_style { Abc, Pnn }; - struct relabeling_map: public std::unordered_map> + struct relabeling_map: public std::map { void clear() { - for (iterator i = begin(); i != end(); ++i) - i->second->destroy(); - this->std::unordered_map>::clear(); + iterator i = begin(); + while (i != end()) + i++->second->destroy(); + this->std::map::clear(); } ~relabeling_map() diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 46242e717c9af510551131fafcd22d768dec2f1a..fb4c74e1ae6c998d3315cc318bce4c0c253b899d 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -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; + + %template(mapff) map; +} + +%{ + namespace swig { + template <> struct traits { + typedef pointer_category category; + static const char* type_name() { return "spot::ltl::atomic_prop"; } + }; + template <> struct traits { + 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; -} - -%{ - namespace swig { - template <> struct traits { - 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 diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 139dd5e6bd960802a83c50ef5a712fe7d8b4e3a8..bec3f22dabbcc7f956404c6d69f14758e94da32b 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -49,5 +49,6 @@ TESTS = \ piperead.ipynb \ randaut.ipynb \ randltl.ipynb \ + relabel.py \ setxor.py \ testingaut.ipynb diff --git a/wrap/python/tests/relabel.py b/wrap/python/tests/relabel.py new file mode 100644 index 0000000000000000000000000000000000000000..14bbb009174ae1c517a459d946abefe245ecafae --- /dev/null +++ b/wrap/python/tests/relabel.py @@ -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 . + +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)""")