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

sepsets: fix infinite loop

Browse source 
* tests/core/sepsets.test: New test case.
* spot/twaalgos/sepsets.cc: Fix the code.
* NEWS: Mention the problem.
This commit is contained in:
Alexandre Duret-Lutz 2019-04-26 11:27:11 +02:00
parent 936481dcbd
commit 26e2f9cec8
3 changed files with 34 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -1,6 +1,9 @@
New in spot 2.7.3.dev (not yet released) New in spot 2.7.3.dev (not yet released)
Nothing yet. Bugs fixed:
- separate_sets_here() (and therefore autfilt --separate-sets) could
loop infinitely on some inputs.
New in spot 2.7.3 (2019-04-19) New in spot 2.7.3 (2019-04-19)

19
spot/twaalgos/sepsets.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015-2018 Laboratoire de Recherche et // Copyright (C) 2015-2019 Laboratoire de Recherche et
// Développement de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -56,7 +56,7 @@ namespace spot
// Fix the acceptance condition // Fix the acceptance condition
auto& code = aut->acc().get_acceptance(); auto& code = aut->acc().get_acceptance();
// If code were empty, then common would have been 0. // If code were empty, then common would have been 0.
assert (!code.empty()); assert(!code.empty());
acc_cond::acc_word* pos = &code.back(); acc_cond::acc_word* pos = &code.back();
acc_cond::acc_word* start = &code.front(); acc_cond::acc_word* start = &code.front();
while (pos > start) while (pos > start)
@ -69,14 +69,13 @@ namespace spot
break; break;
case acc_cond::acc_op::Fin: case acc_cond::acc_op::Fin:
case acc_cond::acc_op::FinNeg: case acc_cond::acc_op::FinNeg:
if (!(pos[-1].mark & common)) if (pos[-1].mark & common)
break; for (auto p: map)
for (auto p: map) if (pos[-1].mark & p.first)
if (pos[-1].mark & p.first) {
{ pos[-1].mark -= p.first;
pos[-1].mark -= p.first; pos[-1].mark |= p.second;
pos[-1].mark |= p.second; }
}
SPOT_FALLTHROUGH; SPOT_FALLTHROUGH;
case acc_cond::acc_op::Inf: case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg: case acc_cond::acc_op::InfNeg:

22
tests/core/sepsets.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement de # Copyright (C) 2015, 2019 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -39,6 +39,16 @@ State: 2
[!0&1&!2] 1 [!0&1&!2] 1
[0&!2] 2 {0 1} [0&!2] 2 {0 1}
--END-- --END--
HOA: v1
States: 1
Start: 0
AP: 3 "p0" "p1" "p2"
Acceptance: 3 (Fin(1) | Inf(0)) & (Fin(2) | Inf(1))
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {0 1 2}
[0&!1&!2] 0
--END--
EOF EOF
cat >expected <<EOF cat >expected <<EOF
@ -60,6 +70,16 @@ State: 2
[!0&1&!2] 1 [!0&1&!2] 1
[0&!2] 2 {0 1 2 3} [0&!2] 2 {0 1 2 3}
--END-- --END--
HOA: v1
States: 1
Start: 0
AP: 3 "p0" "p1" "p2"
Acceptance: 4 (Fin(3) | Inf(0)) & (Fin(2) | Inf(1))
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {0 1 2 3}
[0&!1&!2] 0
--END--
EOF EOF
run 0 autfilt --separate-sets in -H > out run 0 autfilt --separate-sets in -H > out