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

remfin: fix tra_to_tba

Browse source 
This fixes a complementation bug reported by Juraj Major and Tereza
Šťastná.

* spot/twaalgos/remfin.cc (is_scc_tba_type): Fix the condition for
handling Fin-alone pairs.
* tests/core/complement.test: Add Juraj & Tereza's test case.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2019-12-05 22:27:19 +01:00
parent e778965730
commit c36b1588fc
3 changed files with 28 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -54,6 +54,15 @@ New in spot 2.8.3.dev (not yet released)
parity_min_odd(n) = parity_min(true, n)
parity_min_even(n) = parity_min(false, n)
Bugs fixed:
- The Rabin-to-Büchi conversion could misbehave when applied to
Rabin-like acceptance with where some pairs have missing Inf(.)
(e.g. Fin(0)|(Inf(1)&Fin(2))) and when some of the SCCs do not
visit the remaining Inf(.). This indirectly caused the
complementation algorithm to produce incorrect results on such
inputs, causing false positives in ltlcross and autcross.
New in spot 2.8.3 (2019-11-06)
Build:

5
spot/twaalgos/remfin.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -126,7 +126,8 @@ namespace spot
auto scc_pairs = rs_pairs_view(aut_pairs.pairs(), scc_acc);
// If there is one aut_fin_alone that is not in the SCC,
// any cycle in the SCC is accepting.
if (scc_pairs.fins_alone().proper_subset(aut_pairs.fins_alone()))
auto aut_fin_alone = aut_pairs.fins_alone();
if ((scc_acc & aut_fin_alone) != aut_fin_alone)
{
for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e)
{

16
tests/core/complement.test
View file

@ -142,3 +142,19 @@ State: 1
--END--
EOF
diff out expected
# The following automaton used to be badly complemented due
# to a bug in the Rabin-to-BA conversion.
# Reported by Juraj Major and Tereza Šťastná.
cat >pos.hoa <<EOF
HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c" Acceptance: 3 Fin(0) |
(Inf(1) & Fin(2)) properties: trans-labels explicit-labels trans-acc
--BODY-- State: 0 [0&1&2] 5 {2} State: 1 [0&1&!2] 1 {0} [0&1&2]
2 [0&!1&!2] 6 State: 2 [!0&1&2] 4 State: 3 [!0&1&2] 2 {0} [0&1&2] 3
[0&1&2] 1 State: 4 [!0&!1&!2] 7 {2} State: 5 [!0&1&!2] 3 [!0&!1&2]
5 [!0&!1&!2] 2 {0} State: 6 [!0&1&2] 7 {0 1 2} [!0&!1&!2] 6 State: 7
[!0&1&2] 4 [0&!1&2] 7 --END--
EOF
autfilt --complement pos.hoa >neg.hoa
autfilt -q --intersect=pos.hoa neg.hoa && exit 1
: