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 09bb61db33
commit 443f638b9c
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

@ -96,6 +96,9 @@ New in spot 2.8.5.dev (not yet released)
spot.translate(..., 'det', 'any') triggered a syntax error in the spot.translate(..., 'det', 'any') triggered a syntax error in the
Python code to handle this error. Python code to handle this error.
- 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
: