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 13a3f6d72d
commit 48ecb903c5
3 changed files with 35 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -46,6 +46,11 @@ New in spot 2.7.3.dev (not yet released)
acceptance condition. The output can be alternating only if the acceptance condition. The output can be alternating only if the
input was alternating. input was alternating.
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)
Bugs fixed: Bugs fixed:

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