diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 3531b846e..2f7360d9b 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -257,6 +257,101 @@ ltl3ba,4,7 Much more readable! +* Transparent renaming + +Have you ever tried to use =spin=, =ltl2ba=, or =ltl3ba=, to translate +a formula such as =[]!Error=, you have noticed that it does not work: + +#+BEGIN_SRC sh :results verbatim :exports code +spin -f '[]!Error' +#+END_SRC +#+RESULTS: + +#+BEGIN_SRC sh :results verbatim :exports results +spin -f '[]!Error' 2>&1 || exit 0 +#+END_SRC +#+RESULTS: +: tl_spin: expected predicate, saw 'E' +: tl_spin: []!Error +: -------------^ + +All these tools are based on the same LTL parser, that allows +only atomic propositions starting with a lowercase letter. + +Running the same command through =ltldo= will work: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo -t 'spin -f %s>%N' -f '[]!Error' -s +#+END_SRC +#+RESULTS: +: never { +: accept_init: +: if +: :: ((!(Error))) -> goto accept_init +: fi; +: } + +What happened is that =ltldo= renamed the atomic propositions in the +formula before calling =spin=. So =spin= actually received the +formula =[]!p0=, produced a never claim using =p0=, and that never +claim was then relabeled by =ltldo= to use =Error= instead of =p0=. + +This renaming occurs any time some command uses =%s= or =%S= and the +formula has atomic propositions incompatible with Spin's conventions; +or when some command uses =%l=, =%L=, or =%T=, and the formula has +atomic propositions incompatible with [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT's conventions]]. + + +There are some cases where the renaming is not completely transparent. +For instance if a translator tool outputs some HOA file named after +the formula translated, the name will be output unmodified (since this +can be any text string, there is not way for =ltldo= to assume it is +an LTL formula). In the following example, you can see that the +automaton uses the atomic proposition =Error=, but its name contains a +reference to =p0=. + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo 'ltl3ba -H -f %s>%H' -f '[]!Error' -H +#+END_SRC +#+RESULTS: +#+begin_example +HOA: v1 +name: "BA for ([](!(p0)))" +States: 1 +Start: 0 +AP: 1 "Error" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 "accept_init" {0} +[!0] 0 +--END-- +#+end_example + +If this is a problem, you can always force a new name with the +=--name= option: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo 'ltl3ba -H -f %s>%H' -f '[]!Error' -H --name='BA for %f' +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +name: "BA for []!Error" +States: 1 +Start: 0 +AP: 1 "Error" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 "accept_init" {0} +[!0] 0 +--END-- +#+end_example + * Controlling and measuring time The run time of each command can be restricted with the =-T NUM= diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index 0399b1f88..4e81c620d 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -35,8 +35,11 @@ #include "common_trans.hh" #include "ltlvisit/tostring.hh" +#include "ltlvisit/relabel.hh" +#include "misc/bareword.hh" #include "misc/timer.hh" #include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/relabel.hh" #include "hoaparse/public.hh" #include "dstarparse/public.hh" @@ -291,7 +294,6 @@ namespace inputf = input; process_formula(f, filename, linenum); - f->destroy(); return 0; } @@ -300,6 +302,21 @@ namespace process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { + std::unique_ptr relmap; + + // If atomic propositions are incompatible with one of the + // output, relabel the formula. + if ((!f->has_lbt_atomic_props() && + (runner.has('l') || runner.has('L') || runner.has('T'))) + || (!f->has_spin_atomic_props() && + (runner.has('s') || runner.has('S')))) + { + relmap.reset(new spot::ltl::relabeling_map); + auto g = spot::ltl::relabel(f, spot::ltl::Pnn, relmap.get()); + f->destroy(); + f = g; + } + static unsigned round = 0; runner.round_formula(f, round); @@ -313,6 +330,8 @@ namespace error_at_line(2, 0, filename, linenum, "aborting here"); if (aut) { + if (relmap) + relabel_here(aut, relmap.get()); aut = post.run(aut, f); cmdname = translators[t].name; roundval = round; @@ -320,6 +339,7 @@ namespace nullptr); }; } + f->destroy(); ++round; return 0; } diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 7fb3d361d..afa45edd3 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -60,6 +60,7 @@ tgbaalgos_HEADERS = \ randomize.hh \ reachiter.hh \ reducerun.hh \ + relabel.hh \ replayrun.hh \ safety.hh \ save.hh \ @@ -111,6 +112,7 @@ libtgbaalgos_la_SOURCES = \ reachiter.cc \ reducerun.cc \ replayrun.cc \ + relabel.cc \ safety.cc \ save.cc \ scc.cc \ diff --git a/src/tgbaalgos/relabel.cc b/src/tgbaalgos/relabel.cc new file mode 100644 index 000000000..e909efc6c --- /dev/null +++ b/src/tgbaalgos/relabel.cc @@ -0,0 +1,43 @@ +// -*- 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. +// +// 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 . + +#include "relabel.hh" + +namespace spot +{ + void + relabel_here(tgba_digraph_ptr& aut, ltl::relabeling_map* relmap) + { + bddPair* pairs = bdd_newpair(); + auto d = aut->get_dict(); + std::vector vars; + vars.reserve(relmap->size()); + for (auto& p: *relmap) + { + int oldv = d->register_proposition(p.first, aut); + int newv = d->register_proposition(p.second, aut); + bdd_setpair(pairs, oldv, newv); + vars.push_back(oldv); + } + for (auto& t: aut->transitions()) + t.cond = bdd_replace(t.cond, pairs); + for (auto v: vars) + d->unregister_variable(v, aut); + } +} diff --git a/src/tgbaalgos/relabel.hh b/src/tgbaalgos/relabel.hh new file mode 100644 index 000000000..98e8237f2 --- /dev/null +++ b/src/tgbaalgos/relabel.hh @@ -0,0 +1,34 @@ +// -*- 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. +// +// 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 . + +#ifndef SPOT_TGBAALGOS_RELABEL_HH +#define SPOT_TGBAALGOS_RELABEL_HH + +#include "ltlvisit/relabel.hh" +#include "tgba/tgbagraph.hh" + +namespace spot +{ + /// replace atomic propositions in an automaton + SPOT_API void + relabel_here(tgba_digraph_ptr& aut, + ltl::relabeling_map* relmap); +} + +#endif // SPOT_TGBAALGOS_RELABEL_HH diff --git a/src/tgbatest/ltldo.test b/src/tgbatest/ltldo.test index b65640d6e..43c643760 100755 --- a/src/tgbatest/ltldo.test +++ b/src/tgbatest/ltldo.test @@ -32,6 +32,14 @@ cat >expected <output +cat >expected <%H" -f GF_foo_ -H >output +cat output +# The HOA output uses _foo_ as atomic proposition, but the name shows +# that GFp0 was actually given to ltl2tgba. +cat >expected <%H" -f GF_foo_ -H --name=%f >output +cat output +cat >expected <