alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

fix complete

Browse source 
Alexandre Lewkowicz reported a case where complete() would peek an
existing state that is accepting, and wrongly use it as a sink.

* spot/twaalgos/complete.cc: Fix the function.
* tests/core/complete.test: Add two more tests.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2016-01-14 17:14:01 +01:00
parent 6c62362fe9
commit 51483b9b7f
3 changed files with 85 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -130,6 +130,8 @@ New in spot 1.99.6a (not yet released)
was registered several times.
* product() would incorrectly mark the product of two
sttuter-sensitive automata as stutter-sensitive as well.
* complete() could incorrectly reuse an existing (but accepting!)
state as a sink.
New in spot 1.99.6 (2015-12-04)

34
spot/twaalgos/complete.cc
View file

@ -45,27 +45,38 @@ namespace spot
}
else
{
// 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.
// Loop over the states and search a state that has only self
// loop labeled by the same non-accepting mark. 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;
acc_cond::mark_t accsum = 0U;
bool sinkable = true;
bool first = true;
acc_cond::mark_t commonacc = 0U;
for (auto& t: aut->out(i))
{
if (t.dst != i) // Not a self-loop
{
selfloop = false;
sinkable = false;
break;
}
accsum |= t.acc;
if (first)
{
commonacc = t.acc;
first = false;
}
if (selfloop && !aut->acc().accepting(accsum))
else if (t.acc != commonacc)
{
sinkable = false;
break;
}
}
if (sinkable && !aut->acc().accepting(commonacc))
{
// We have found a sink!
um.second = commonacc;
sink = i;
break;
}
@ -74,8 +85,7 @@ namespace spot
unsigned t = aut->num_edges();
// If the automaton is empty,
// pretend that state
// If the automaton is empty, pretend that state 0 is a sink.
if (t == 0)
sink = init;

63
tests/core/complete.test
View file

@ -1,7 +1,7 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -57,6 +57,31 @@ State: 0
State: 1
[0] 1
--END--
/* This example comes from Alexandre Lewkowicz */
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 Fin(0)&Inf(1)
--BODY--
State: 0
[0] 1
State: 1
[0] 1 {0}
[!0] 1 {1}
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 2 Fin(0)&Inf(1)
--BODY--
State: 0
[0] 1
State: 1
[0] 1 {0}
[!0] 1 {0}
--END--
EOF
cat >expected <<EOF
@ -112,6 +137,40 @@ State: 1
[0] 1
[!0] 1
--END--
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 1
[!0] 2
State: 1
[0] 1 {0}
[!0] 1 {1}
State: 2
[t] 2
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[0] 1
[!0] 1
State: 1 {0}
[0] 1
[!0] 1
--END--
EOF
run 0 autfilt -CH automaton >out