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

remfin: fix handling of weak automata

Browse source 
* spot/twaalgos/remfin.cc: Do not add a sink states to deterministic
weak automata, and actually apply the "weak" Fin-removal to any weak
automaton.
* tests/core/explprod.test: Add a test case for the previous patch,
but that used to fail because of this bug.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-11 12:30:13 +01:00
parent 49266dee7f
commit a70589fe13
3 changed files with 14 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -63,6 +63,9 @@ New in spot 2.1.2.dev (not yet released)
already opened file descriptor, it will not close the file
anymore.
* remove_fin() could produce incorrect result on incomplete
automata tagged as weak and deterministic.
New in spot 2.1.2 (2016-10-14)
Command-line tools:

31
spot/twaalgos/remfin.cc
View file

@ -452,7 +452,7 @@ namespace spot
}
static twa_graph_ptr
remove_fin_det_weak(const const_twa_graph_ptr& aut)
remove_fin_weak(const const_twa_graph_ptr& aut)
{
// Clone the original automaton.
auto res = make_twa_graph(aut,
@ -462,42 +462,23 @@ namespace spot
true, // determinisitic
true, // stutter inv.
});
res->purge_dead_states();
scc_info si(res);
// We will modify res in place, and the resulting
// automaton will only have one acceptance set.
acc_cond::mark_t all_acc = res->set_buchi();
res->prop_state_acc(true);
res->prop_deterministic(true);
unsigned n = res->num_states();
unsigned sink = res->num_states();
for (unsigned src = 0; src < sink; ++src)
for (unsigned src = 0; src < n; ++src)
{
acc_cond::mark_t acc = 0U;
unsigned scc = si.scc_of(src);
if (si.is_accepting_scc(scc) && !si.is_trivial(scc))
acc = all_acc;
// Keep track of all conditions on edge leaving state
// SRC, so we can complete it.
bdd missingcond = bddtrue;
for (auto& t: res->out(src))
{
missingcond -= t.cond;
t.acc = acc;
}
// Complete the original automaton.
if (missingcond != bddfalse)
{
if (res->num_states() == sink)
{
res->new_state();
res->new_acc_edge(sink, sink, bddtrue);
}
res->new_edge(src, sink, missingcond);
}
}
//res->merge_edges();
return res;
}
}
@ -507,9 +488,9 @@ namespace spot
if (!aut->acc().uses_fin_acceptance())
return std::const_pointer_cast<twa_graph>(aut);
// FIXME: we should check whether the automaton is weak.
if (aut->prop_inherently_weak().is_true() && is_deterministic(aut))
return remove_fin_det_weak(aut);
// FIXME: we should check whether the automaton is inherently weak.
if (aut->prop_weak().is_true())
return remove_fin_weak(aut);
if (auto maybe = streett_to_generalized_buchi_maybe(aut))
return maybe;

6
tests/core/explprod.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2008, 2009, 2013, 2014 Laboratoire de Recherche et
# Copyright (C) 2008, 2009, 2013, 2014, 2016 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -99,4 +99,6 @@ EOF
run 0 autfilt input1 --product input2 --hoa --small | tee stdout
run 0 autfilt -F stdout --isomorph expected
rm input1 input2 stdout expected
# Reading two automata from stdin
ltl2tgba '!a' 'a U b' | autfilt --product=- - > aut1
ltl2tgba '!a&b' | autfilt -q --equivalent-to=aut1