Commit 23bcbb5b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

complete: Fix completion of automata using Fin-acceptance

* src/tgba/acc.cc, src/tgba/acc.hh: Add a way to extract
an unstatisfiable mark, and fix the eval() function for
Fin acceptance.
* src/tgbaalgos/complete.cc: Label the sink state using
an unsatisfiable mark.  Do not assume generalized Büchi.
* src/tgbatest/complete.test: New test.
* src/tgbatest/Makefile.am: Add it.
parent 7353e47f
......@@ -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<bdd> r;
std::vector<unsigned> 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<bdd> r;
std::vector<unsigned> sets(c);
for (unsigned i = 0; r.size() < c; ++i)
......@@ -543,6 +545,61 @@ namespace spot
return rescode;
}
std::pair<bool, acc_cond::mark_t>
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<bdd> r;
std::vector<unsigned> 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)
......
......@@ -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<bool, acc_cond::mark_t> unsat_mark() const;
// Return the sets used as Inf or Fin in the acceptance condition
std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
......
......@@ -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.
......
......@@ -72,6 +72,7 @@ TESTS = \
det.test \
neverclaimread.test \
hoaparse.test \
complete.test \
remfin.test \
dstar.test \
readsave.test \
......
#! /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 <http://www.gnu.org/licenses/>.
. ./defs || exit 1
set -e
cat >automaton <<EOF
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 1 Fin(0)
--BODY--
State: 0
[0] 1
State: 1
[0] 1
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 t
--BODY--
State: 0
[0] 1
State: 1
[0] 1
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 0 f
--BODY--
State: 0
[0] 1
State: 1
[0] 1
--END--
EOF
cat >expected <<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[0] 1
[!0] 2
State: 1
[0] 1
[!0] 2
State: 2 {0}
[t] 2
--END--
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0 {0}
[0] 1
[!0] 2
State: 1 {0}
[0] 1
[!0] 2
State: 2
[t] 2
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 0 f
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[0] 1
[!0] 1
State: 1
[0] 1
[!0] 1
--END--
EOF
run 0 ../../bin/autfilt -CH automaton >out
cat out
diff out expected
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment