diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 6dbdff4af..9828541c0 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -193,7 +193,7 @@ namespace spot case acc_cond::acc_op::Inf: return (pos[-1].mark & inf) == pos[-1].mark; case acc_cond::acc_op::Fin: - return (pos[-1].mark & inf) == 0U; + return (pos[-1].mark & inf) != pos[-1].mark; case acc_cond::acc_op::FinNeg: case acc_cond::acc_op::InfNeg: SPOT_UNREACHABLE(); @@ -413,6 +413,7 @@ namespace spot bdd_allocator ba; int base = ba.allocate_variables(c); + assert(base == 0); std::vector r; std::vector sets(c); for (unsigned i = 0; r.size() < c; ++i) @@ -483,6 +484,7 @@ namespace spot bdd_allocator ba; int base = ba.allocate_variables(c); + assert(base == 0); std::vector r; std::vector sets(c); for (unsigned i = 0; r.size() < c; ++i) @@ -543,6 +545,61 @@ namespace spot return rescode; } + std::pair + acc_cond::acc_code::unsat_mark() const + { + if (empty()) + return {false, 0U}; + + auto used = acc_cond::acc_code::used_sets(); + unsigned c = used.count(); + + bdd_allocator ba; + int base = ba.allocate_variables(c); + assert(base == 0); + std::vector r; + std::vector sets(c); + for (unsigned i = 0; r.size() < c; ++i) + { + if (used.has(i)) + { + sets[base] = i; + r.push_back(bdd_ithvar(base++)); + } + else + { + r.push_back(bddfalse); + } + } + + bdd res = to_bdd_rec(&back(), &r[0]); + + if (res == bddtrue) + return {false, 0U}; + if (res == bddfalse) + return {true, 0U}; + + bdd cube = bdd_satone(!res); + mark_t i = 0U; + while (cube != bddtrue) + { + // The acceptance set associated to this BDD variable + int s = sets[bdd_var(cube)]; + + bdd h = bdd_high(cube); + if (h == bddfalse) // Negative variable? -> skip + { + cube = bdd_low(cube); + } + else // Positive variable? -> Inf + { + i.set(s); + cube = h; + } + } + return {true, i}; + } + bool acc_cond::acc_code::is_dnf() const { if (empty() || size() == 2) diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 96bd6cfc9..bccd3937a 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -659,6 +659,10 @@ namespace spot // Return the set of sets appearing in the condition. acc_cond::mark_t used_sets() const; + // Return (true, m) if there exist some m that does not satisfy + // the acceptance condition. Return (false, 0U) otherwise. + std::pair unsat_mark() const; + // Return the sets used as Inf or Fin in the acceptance condition std::pair used_inf_fin_sets() const; diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index ecd44dbb8..54e0b73e7 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -25,21 +25,26 @@ namespace spot { unsigned n = aut->num_states(); unsigned sink = -1U; - acc_cond::mark_t allacc = aut->acc().all_sets(); - if (allacc == 0U) + + // UM is a pair (bool, mark). If the Boolean is false, the + // acceptance is always satisfiable. Otherwise, MARK is an + // example of unsatisfiable mark. + auto um = aut->get_acceptance().unsat_mark(); + if (!um.first) { - // We cannot safely complete an automaton if it has no - // acceptance set as the added sink would become accepting. - // In this case, add an acceptance set to all transitions. - allacc = aut->set_buchi(); + // We cannot safely complete an automaton if its + // acceptance is always satisfiable. + auto acc = aut->set_buchi(); for (auto& t: aut->transition_vector()) - t.acc = allacc; + t.acc = acc; } else { - // If some acceptance sets were used, loop over the states and - // seek a state that has only self loops, and that is not - // accepting. This will be our sink state. + // Loop over the states and seek a state that has only self + // loops, and that is not accepting. This will be our sink + // state. Note that we do not even have to ensure that the + // state is complete as we will complete the whole automaton + // in a second pass. for (unsigned i = 0; i < n; ++i) { bool selfloop = true; @@ -53,8 +58,9 @@ namespace spot } accsum |= t.acc; } - if (selfloop && accsum != allacc) // We have found a sink! + if (selfloop && !aut->acc().accepting(accsum)) { + // We have found a sink! sink = i; break; } @@ -63,7 +69,7 @@ namespace spot unsigned t = aut->num_transitions(); - // Now complete all states (including the sink). + // Now complete all states (excluding any newly added the sink). for (unsigned i = 0; i < n; ++i) { bdd missingcond = bddtrue; @@ -94,7 +100,7 @@ namespace spot if (sink == -1U) { sink = aut->new_state(); - ++n; + aut->new_transition(sink, sink, bddtrue, um.second); } // In case the automaton use state-based acceptance, propagate // the acceptance of the first transition to the one we add. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 07968d46c..97a87b3d2 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -72,6 +72,7 @@ TESTS = \ det.test \ neverclaimread.test \ hoaparse.test \ + complete.test \ remfin.test \ dstar.test \ readsave.test \ diff --git a/src/tgbatest/complete.test b/src/tgbatest/complete.test new file mode 100755 index 000000000..a1a06aa57 --- /dev/null +++ b/src/tgbatest/complete.test @@ -0,0 +1,117 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + + +. ./defs || exit 1 + +set -e + +cat >automaton <expected <out +cat out +diff out expected