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

ltldo: automatic renaming of AP

* src/bin/ltldo.cc: Relabel formula and output automata as needed.
* src/tgbaalgos/relabel.cc, src/tgbaalgos/relabel.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltldo.test: Add some tests.
* doc/org/ltldo.org: Document this.
parent a4a0cf3b
......@@ -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=
......
......@@ -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<spot::ltl::relabeling_map> 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;
}
......
......@@ -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 \
......
// -*- 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 <http://www.gnu.org/licenses/>.
#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<int> 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);
}
}
// -*- 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 <http://www.gnu.org/licenses/>.
#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
......@@ -32,6 +32,14 @@ cat >expected <<EOF
EOF
diff output expected
# Renaming
run 0 $ltldo -f a -f 'a&_b' -t 'echo %f,%s' >output
cat >expected <<EOF
(a),(a)
(p0) & (p1),(p0) && (p1)
EOF
diff output expected
# Test timeouts. This test should take 2*2 seconds.
$genltl --or-g=1..2 |
......@@ -52,3 +60,46 @@ ba,1,GFp1 & GFp2,3,12,8
tgba,2,GFp1 & GFp2 & GFp3,1,8,8
ba,2,GFp1 & GFp2 & GFp3,4,32,13
EOF
diff output expected
# Renaming
run 0 $ltldo "$ltl2tgba -H %s>%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 <<EOF
HOA: v1
name: "GFp0"
States: 1
Start: 0
AP: 1 "_foo_"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
[0] 0 {0}
[!0] 0
--END--
EOF
diff output expected
# But we can force the name in the output:
run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H --name=%f >output
cat output
cat >expected <<EOF
HOA: v1
name: "GF_foo_"
States: 1
Start: 0
AP: 1 "_foo_"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
[0] 0 {0}
[!0] 0
--END--
EOF
diff output expected
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