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

relabel: do not unregister old AP that are also new

Reported by Ayrat Khalimov against the trans.html page when using
ltl3ba.

* spot/twaalgos/relabel.cc: Here.
* tests/core/ltl3dra.test: Test it.
* NEWS: Mention it.
* THANKS: Add Ayrat.
parent 91e8493c
...@@ -91,6 +91,10 @@ New in spot 2.0.2a (not yet released) ...@@ -91,6 +91,10 @@ New in spot 2.0.2a (not yet released)
* The generalized testing automata displayed by the on-line * The generalized testing automata displayed by the on-line
translator were incorrect (those output by ltl2tgta were OK). translator were incorrect (those output by ltl2tgta were OK).
* ltl2tgta should not offer options --ba, --monitor, --tgba and such. * ltl2tgta should not offer options --ba, --monitor, --tgba and such.
* the relabel() function could incorrectly unregister old atomic
propositions even if they are still used in the output (e.g., if
a&p0 is relabeled to p0&p1). This could cause ltldo and on-line
translator to report errors.
New in spot 2.0.2 (2016-06-17) New in spot 2.0.2 (2016-06-17)
......
...@@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or ...@@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or
suggestions. suggestions.
Akim Demaille Akim Demaille
Ayrat Khalimov
Caroline Lemieux Caroline Lemieux
Christian Dax Christian Dax
Christopher Ziegler Christopher Ziegler
......
...@@ -27,6 +27,7 @@ namespace spot ...@@ -27,6 +27,7 @@ namespace spot
bddPair* pairs = bdd_newpair(); bddPair* pairs = bdd_newpair();
auto d = aut->get_dict(); auto d = aut->get_dict();
std::vector<int> vars; std::vector<int> vars;
std::set<int> newvars;
vars.reserve(relmap->size()); vars.reserve(relmap->size());
for (auto& p: *relmap) for (auto& p: *relmap)
{ {
...@@ -34,10 +35,15 @@ namespace spot ...@@ -34,10 +35,15 @@ namespace spot
int newv = aut->register_ap(p.second); int newv = aut->register_ap(p.second);
bdd_setpair(pairs, oldv, newv); bdd_setpair(pairs, oldv, newv);
vars.push_back(oldv); vars.push_back(oldv);
newvars.insert(newv);
} }
for (auto& t: aut->edges()) for (auto& t: aut->edges())
t.cond = bdd_replace(t.cond, pairs); t.cond = bdd_replace(t.cond, pairs);
// Erase all the old variable that are not reused in the new set.
// (E.g., if we relabel a&p0 into p0&p1 we should not unregister
// p0)
for (auto v: vars) for (auto v: vars)
aut->unregister_ap(v); if (newvars.find(v) == newvars.end())
aut->unregister_ap(v);
} }
} }
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et # Copyright (C) 2015, 2016 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -35,3 +35,9 @@ ltlcross 'ltl2tgba' 'ltl3dra' -f '(<>((((p0) && ...@@ -35,3 +35,9 @@ ltlcross 'ltl2tgba' 'ltl3dra' -f '(<>((((p0) &&
&& ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1))
&& ([](p3))) || ((p1) && (!([](p3))))))))) && (((p0) && (!(<>(p2)))) && ([](p3))) || ((p1) && (!([](p3))))))))) && (((p0) && (!(<>(p2))))
|| ((!(p0)) && (<>(p2)))))))' || ((!(p0)) && (<>(p2)))))))'
# This used to trigger an assertion because the formula "a=0"&p0 was
# relabeled p0&p1, and then p0 was unregistered despite being one of
# the new variables.
ltldo ltl3dra -f '"a=0" & p0' | grep 'AP: 2.*p0'
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