diff --git a/NEWS b/NEWS index 55b5eb26dff1092cf991fa949652e34db67e40b1..8148db94303cf02f1e385b1e478986b4d1f5d0ff 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index acabd545df212f37ca0f259e856d493ddb71ff11..9eeac1b13a9afdc32c1b465de3393830705892fa 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -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); - } + t.acc = acc; } - //res->merge_edges(); return res; } } @@ -507,9 +488,9 @@ namespace spot if (!aut->acc().uses_fin_acceptance()) return std::const_pointer_cast(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; diff --git a/tests/core/explprod.test b/tests/core/explprod.test index d216784dbc8aea2f4cb79b19cce6934a2dfed388..e994e2f1c88929bbef63596eff8af7fbd7215355 100755 --- a/tests/core/explprod.test +++ b/tests/core/explprod.test @@ -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