alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

relabel: do not create automata with false labels

Browse source 
* spot/twaalgos/relabel.cc: Remove false transitions if
some of the propositions are equivalent to true or false.
* NEWS: Mention the bug.
* tests/core/ltl2tgba2.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2020-02-10 12:05:36 +01:00
parent cf2cfcd2fb
commit 9365f8de1b
3 changed files with 22 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -11,6 +11,9 @@ New in spot 2.8.5.dev (not yet released)
consequence, some correct output could be larger than necessary consequence, some correct output could be larger than necessary
(but still correct). (but still correct).
- Some formulas with Boolean sub-formulas equivalent to true or
false could be translated into automata with false labels.
New in spot 2.8.5 (2020-01-04) New in spot 2.8.5 (2020-01-04)
Bugs fixed: Bugs fixed:

15
spot/twaalgos/relabel.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement // Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et
// 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.
// //
@ -32,6 +32,7 @@ namespace spot
std::set<int> newvars; std::set<int> newvars;
vars.reserve(relmap->size()); vars.reserve(relmap->size());
bool bool_subst = false; bool bool_subst = false;
bool need_cleanup = false;
for (auto& p: *relmap) for (auto& p: *relmap)
{ {
@ -61,6 +62,8 @@ namespace spot
bdd newb = formula_to_bdd(p.second, d, aut); bdd newb = formula_to_bdd(p.second, d, aut);
bdd_setbddpair(pairs, oldv, newb); bdd_setbddpair(pairs, oldv, newb);
bool_subst = true; bool_subst = true;
if (newb == bddtrue || newb == bddfalse)
need_cleanup = true;
} }
} }
if (!bool_subst) if (!bool_subst)
@ -76,5 +79,13 @@ namespace spot
for (auto v: vars) for (auto v: vars)
if (newvars.find(v) == newvars.end()) if (newvars.find(v) == newvars.end())
aut->unregister_ap(v); aut->unregister_ap(v);
// If some of the proposition are equivalent to true or false,
// it's possible that we have introduced edges with false labels.
if (need_cleanup)
{
aut->merge_edges(); // remove any edge labeled by 0
aut->purge_dead_states(); // remove useless states
}
} }
} }

7
tests/core/ltl2tgba2.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2009-2019 Laboratoire de Recherche et Développement de # Copyright (C) 2009-2020 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -431,3 +431,8 @@ cat >expected <<EOF
8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) 8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1))
8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) & (Fin(0) | Inf(2)) 8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) & (Fin(0) | Inf(2))
EOF EOF
# This formula used to produce translation with false label.
ltl2tgba -D -G 'F(G(a | !a) & ((b <-> c) W d))' | grep '\[f\]' && exit 1
: