diff --git a/ChangeLog b/ChangeLog index 07938b241..5250db7dc 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2010-04-13 Alexandre Duret-Lutz + + Fix bugs in minimize(), caught by spotlbtt.test. + + * src/tgbaalgos/minimize.cc (minimize): Don't add acceptance + conditions if the final set is empty. + * src/tgbaalgos/powerset.cc (tgba_powerset): Add the initial state + to acc_list if it is accepting. Also do not compute an SCC build + map if we don't have to build acc_list. + 2010-04-13 Alexandre Duret-Lutz "ltl2tgba -Rm" will apply WDBA-minimization only if correct. diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index a2c5cfa32..f986d17dc 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -93,7 +93,8 @@ namespace spot tgba_explicit_number* res = new tgba_explicit_number(a->get_dict()); // For each transition in the initial automaton, add the corresponding // transition in res. - res->declare_acceptance_condition(ltl::constant::true_instance()); + if (!final->empty()) + res->declare_acceptance_condition(ltl::constant::true_instance()); for (sit = sets.begin(); sit != sets.end(); ++sit) { hash_set::iterator hit; diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 4fd0408cb..3dff3f6f4 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -56,7 +56,12 @@ namespace spot ps.insert(s); todo.push_back(ps); seen[ps] = 1; - m.build_map(); + if (acc_list) + { + m.build_map(); + if (m.accepting(m.scc_of_state(s))) + acc_list->push_front(new state_explicit(res->add_state(1))); + } } unsigned state_num = 1; @@ -99,9 +104,12 @@ namespace spot { states.insert(s); } - unsigned scc_num = m.scc_of_state(s); - if (m.accepting(scc_num)) - accepting = true; + if (acc_list) + { + unsigned scc_num = m.scc_of_state(s); + if (m.accepting(scc_num)) + accepting = true; + } dest.insert(s); } delete si; @@ -123,7 +131,7 @@ namespace spot seen[dest] = dest_num; todo.push_back(dest); t = res->create_transition(seen[src], dest_num); - if (acc_list && accepting) + if (accepting) { const state* dst = new state_explicit(t->dest); acc_list->push_front(dst); diff --git a/src/tgbatest/minimize.cc b/src/tgbatest/minimize.cc index 5f193de42..4008fe1a1 100644 --- a/src/tgbatest/minimize.cc +++ b/src/tgbatest/minimize.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library.