Commit 1b2f2a79 authored by Maximilien Colange's avatar Maximilien Colange
Browse files

Fix a bug in spot.complete()

spot.complete() could complete an empty co-Büchi automaton into an
automaton accepting everything.

* NEWS: Document it
* spot/twaalgos/complete.cc: Fix it
* tests/core/complete.test, tests/core/prodor.test: Test it
parent eb91ecf6
......@@ -215,6 +215,9 @@ New in spot 2.3.5.dev (not yet released)
generalized co-Büchi), it would sometimes output an automaton with
transition-based acceptance but marked as state-based.
- The complete() function could complete an empty co-Büchi automaton into an
automaton accepting everything.
Backward-incompatible changes:
- spot::acc_cond::mark_t::operator bool() has been marked as
......
......@@ -69,7 +69,7 @@ namespace spot
loopmark = t.acc;
first = false;
}
// If this this not the first self loop and it as a
// If this this not the first self loop and it has a
// different acceptance mark, do not consider this
// state as a sink candidate: combining loops with
// different marks might be used to build an accepting
......@@ -107,7 +107,7 @@ namespace spot
for (unsigned i = 0; i < n; ++i)
{
bdd missingcond = bddtrue;
acc_cond::mark_t acc = 0U;
acc_cond::mark_t acc = um.second;
unsigned edge_to_sink = 0;
for (auto& t: aut->out(i))
{
......@@ -121,6 +121,8 @@ namespace spot
// In case the automaton uses edge-based acceptance,
// it does not matter what acceptance set we put the new
// edge into.
// EXCEPT if there is an incomplete sinkable state: completing it
// creates self-loops that must be rejecting.
//
// So in both cases, we put the edge in the same
// acceptance sets as the last outgoing edge of the
......@@ -147,10 +149,11 @@ namespace spot
}
else // otherwise, create the new edge.
{
// in case the automaton use state-based acceptance, propagate
// in case the automaton uses state-based acceptance, propagate
// the acceptance of the first edge to the one we add.
if (!aut->prop_state_acc().is_true())
if (!aut->prop_state_acc().is_true() && i != sink)
acc = 0U;
aut->new_edge(i, sink, missingcond, acc);
}
}
......
......@@ -25,6 +25,14 @@ set -e
cat >automaton <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 1 Fin(0)
--BODY--
State: 0
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
......@@ -107,6 +115,18 @@ EOF
cat >expected <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic
--BODY--
State: 0 {0}
[t] 0
--END--
HOA: v1
States: 3
Start: 0
AP: 1 "a"
......@@ -210,12 +230,12 @@ Start: 0&1
AP: 0
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic univ-branch
--BODY--
State: 0
State: 0 {0}
[t] 0
State: 1
State: 1 {0}
[t] 0
--END--
EOF
......
......@@ -24,6 +24,32 @@ set -e
ltl2tgba=ltl2tgba
autfilt=autfilt
# Two empty automata
cat >a1.hoa <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 1 Fin(0)
--BODY--
State: 0
--END--
EOF
cat >a2.hoa <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 0 f
--BODY--
State: 0
[t] 0
--END--
EOF
# the OR product of two empty automata should be empty
$autfilt --product-or a1.hoa a2.hoa -H | $autfilt --is-empty
$ltl2tgba -DH 'GFa' > gfa.hoa
$ltl2tgba -DH 'FGb' > fgb.hoa
$autfilt --product-or gfa.hoa fgb.hoa -H > por.hoa
......
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