complement: fix a regression with 2.9.8

Reported by Reuben Rowe.

* spot/twaalgos/complement.cc (complement): Remove the hard-coded
simul=0 option on automata with >32 states.  In 2.10 simul=0 now
implies det-simul=0, causing the regression, and most importantly it
is not needed anymore, because we have other threashold like simul-max
and simul-trans-pruning in place.
* tests/core/complement.test: Add Reuben's automaton as test case.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2021-12-17 12:05:33 +01:00
parent c0a43cd92b
commit d8f245a7de
3 changed files with 334 additions and 6 deletions

5
NEWS
View file

@ -6,6 +6,11 @@ New in spot 2.10.2.dev (not yet released)
(e.g. co-Büchi) and where the initial state was in a rejecting
SCC, sbacc() could output a superflous state. (Issue #492)
- Compared to 2.9.8, complement() (and many functions using it) was
slower and produced larger outputs on some automata with more than
32 states due to an optimization of the determinization being
unintentionally disabled.
New in spot 2.10.2 (2021-12-03)
Bugs fixed:

View file

@ -522,11 +522,10 @@ namespace spot
m.set("det-max-states", aborter->max_states());
m.set("det-max-edges", aborter->max_edges());
}
if (aut->num_states() > 32)
{
m.set("ba-simul", 0);
m.set("simul", 0);
}
// In addition to the above options, the simulation-based
// optimization of the determinization is already restricted by
// the default values of simul-max and simul-trans-pruning.
// (See spot-x(7) for details.)
spot::postprocessor p(&m);
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);

View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015-2019 Laboratoire de Recherche et Développement de
# Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -157,4 +157,328 @@ HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c" Acceptance: 3 Fin(0) |
EOF
autfilt --complement pos.hoa >neg.hoa
autfilt -q --intersect=pos.hoa neg.hoa && exit 1
# The following automaton, generated by the Cyclist theorem prover was
# sent by Reuben Rowe to show a regression between Spot 2.9.8 and Spot
# 2.10. In the latter version, complementation was slower and larger,
# because the simulation-based optimization of the determinization was
# turned off. Here we do not check the runtime, but we can check the output
# size, which should be 4 and not 153.
cat >large.hoa<<EOF
HOA: v1
States: 102
Start: 0
AP: 8 "a" "b" "c" "d" "e" "f" "g" "h"
acc-name: Buchi
Acceptance: 1 Inf(0)
Alias: @x 0 & !1 & !2 & !3 & !4 & !5 & !6 & !7
--BODY--
State: 0
[0 & 1 & !2 & 3 & 4 & 5 & !6 & !7] 1
[!0 & !1 & !2 & 3 & 4 & !5 & 6 & !7] 2
[0 & !1 & !2 & 3 & 4 & 5 & !6 & !7] 3
[!0 & 1 & 2 & !3 & 4 & 5 & !6 & !7] 4
[0 & !1 & 2 & !3 & 4 & 5 & !6 & !7] 5
[0 & 1 & !2 & !3 & 4 & 5 & !6 & !7] 6
[!0 & 1 & 2 & 3 & 4 & !5 & !6 & !7] 7
[!0 & 1 & !2 & !3 & 4 & 5 & !6 & !7] 8
[@x] 9
[!0 & !1 & 2 & 3 & !4 & !5 & 6 & !7] 10
[!0 & !1 & !2 & !3 & 4 & 5 & !6 & !7] 11
[!0 & !1 & 2 & 3 & 4 & !5 & !6 & !7] 12
[0 & !1 & 2 & 3 & !4 & 5 & !6 & !7] 13
[0 & !1 & !2 & 3 & 4 & !5 & !6 & !7] 14
[!0 & !1 & 2 & 3 & !4 & 5 & !6 & !7] 15
[0 & 1 & !2 & !3 & !4 & !5 & 6 & !7] 16
[0 & 1 & !2 & 3 & !4 & 5 & !6 & !7] 17
[!0 & !1 & !2 & 3 & !4 & !5 & !6 & !7] 18
[!0 & !1 & !2 & !3 & !4 & 5 & 6 & !7] 19
[0 & !1 & !2 & 3 & !4 & 5 & !6 & !7] 20
[!0 & !1 & !2 & 3 & !4 & 5 & !6 & !7] 21
[!0 & 1 & 2 & !3 & 4 & !5 & !6 & !7] 22
[0 & 1 & 2 & 3 & 4 & !5 & 6 & !7] 23
[0 & 1 & 2 & !3 & !4 & 5 & !6 & !7] 24
[!0 & !1 & 2 & !3 & 4 & !5 & !6 & !7] 25
[!0 & !1 & 2 & !3 & !4 & 5 & !6 & !7] 26
[0 & 1 & !2 & !3 & 4 & !5 & !6 & !7] 27
[0 & !1 & !2 & !3 & !4 & 5 & !6 & !7] 28
[0 & 1 & 2 & 3 & 4 & !5 & !6 & !7] 29
[0 & !1 & !2 & !3 & 4 & 5 & !6 & !7] 30
[0 & 1 & !2 & 3 & !4 & !5 & 6 & !7] 31
[0 & !1 & 2 & !3 & 4 & !5 & !6 & !7] 32
[0 & 1 & 2 & !3 & !4 & !5 & !6 & !7] 33
[!0 & !1 & 2 & 3 & 4 & !5 & 6 & !7] 34
[0 & !1 & !2 & 3 & !4 & !5 & !6 & !7] 35
[!0 & 1 & 2 & 3 & !4 & 5 & !6 & !7] 36
[0 & 1 & 2 & 3 & !4 & 5 & !6 & !7] 37
[!0 & 1 & 2 & !3 & !4 & !5 & 6 & !7] 38
[0 & 1 & 2 & !3 & 4 & 5 & !6 & !7] 39
[!0 & 1 & !2 & !3 & 4 & !5 & 6 & !7] 40
[!0 & 1 & !2 & !3 & 4 & !5 & !6 & !7] 41
[0 & 1 & 2 & !3 & 4 & !5 & !6 & !7] 42
[!0 & !1 & !2 & 3 & 4 & 5 & !6 & !7] 43
[0 & !1 & 2 & 3 & !4 & !5 & !6 & !7] 44
[0 & !1 & 2 & 3 & 4 & !5 & !6 & !7] 45
[!0 & 1 & !2 & 3 & !4 & 5 & !6 & !7] 46
[!0 & 1 & !2 & 3 & !4 & !5 & !6 & !7] 47
[!0 & !1 & 2 & !3 & !4 & !5 & 6 & !7] 48
[!0 & !1 & 2 & !3 & !4 & !5 & !6 & !7] 49
[!0 & 1 & 2 & !3 & 4 & !5 & 6 & !7] 50
[!0 & !1 & 2 & 3 & !4 & !5 & !6 & !7] 51
[!0 & 1 & 2 & !3 & !4 & !5 & !6 & !7] 52
[0 & 1 & !2 & 3 & 4 & !5 & 6 & !7] 53
[0 & 1 & !2 & 3 & 4 & !5 & !6 & !7] 54
[!0 & 1 & 2 & !3 & !4 & 5 & !6 & !7] 55
[!0 & 1 & 2 & 3 & !4 & !5 & !6 & !7] 56
[!0 & !1 & !2 & !3 & !4 & 5 & !6 & !7] 57
[0 & 1 & !2 & 3 & !4 & !5 & !6 & !7] 58
[!0 & 1 & !2 & 3 & 4 & !5 & !6 & !7] 59
[0 & !1 & !2 & !3 & 4 & !5 & !6 & !7] 60
[!0 & 1 & !2 & !3 & !4 & 5 & !6 & !7] 61
[0 & !1 & 2 & !3 & 4 & !5 & 6 & !7] 62
[0 & 1 & 2 & 3 & !4 & !5 & !6 & !7] 63
[!0 & !1 & 2 & !3 & 4 & 5 & !6 & !7] 64
[!0 & !1 & !2 & !3 & 4 & !5 & !6 & !7] 65
[0 & 1 & !2 & !3 & !4 & 5 & !6 & !7] 66
[0 & !1 & 2 & !3 & !4 & 5 & !6 & !7] 67
[0 & 1 & !2 & !3 & !4 & !5 & !6 & !7] 68
[0 & !1 & !2 & !3 & 4 & !5 & 6 & !7] 69
[!0 & !1 & !2 & 3 & 4 & !5 & !6 & !7] 70
[0 & 1 & !2 & !3 & !4 & 5 & 6 & !7] 71
[0 & !1 & 2 & !3 & !4 & !5 & !6 & !7] 72
[!0 & 1 & !2 & 3 & 4 & 5 & !6 & !7] 73
[!0 & 1 & !2 & !3 & !4 & !5 & !6 & !7] 74
[!0 & !1 & 2 & 3 & 4 & 5 & !6 & !7] 75
[0 & !1 & 2 & 3 & 4 & 5 & !6 & !7] 76
[!0 & 1 & 2 & 3 & 4 & 5 & !6 & !7] 77
[0 & 1 & 2 & 3 & 4 & 5 & !6 & !7] 78
[!0 & !1 & !2 & !3 & !4 & !5 & 6 & !7] 79
[0 & !1 & !2 & !3 & !4 & !5 & 6 & !7] 80
[!0 & 1 & !2 & !3 & !4 & !5 & 6 & !7] 81
[0 & !1 & 2 & !3 & !4 & !5 & 6 & !7] 82
[0 & 1 & 2 & !3 & !4 & !5 & 6 & !7] 83
[!0 & !1 & !2 & 3 & !4 & !5 & 6 & !7] 84
[0 & !1 & !2 & 3 & !4 & !5 & 6 & !7] 85
[!0 & 1 & !2 & 3 & !4 & !5 & 6 & !7] 86
[0 & !1 & 2 & 3 & !4 & !5 & 6 & !7] 87
[!0 & 1 & 2 & 3 & !4 & !5 & 6 & !7] 88
[0 & 1 & 2 & 3 & !4 & !5 & 6 & !7] 89
[!0 & !1 & !2 & !3 & 4 & !5 & 6 & !7] 90
[0 & 1 & !2 & !3 & 4 & !5 & 6 & !7] 91
[!0 & !1 & 2 & !3 & 4 & !5 & 6 & !7] 92
[0 & 1 & 2 & !3 & 4 & !5 & 6 & !7] 93
[0 & !1 & !2 & 3 & 4 & !5 & 6 & !7] 94
[!0 & 1 & !2 & 3 & 4 & !5 & 6 & !7] 95
[0 & !1 & 2 & 3 & 4 & !5 & 6 & !7] 96
[!0 & 1 & 2 & 3 & 4 & !5 & 6 & !7] 97
[0 & !1 & !2 & !3 & !4 & 5 & 6 & !7] 98
[!0 & 1 & !2 & !3 & !4 & 5 & 6 & !7] 99
[!0 & !1 & 2 & !3 & !4 & 5 & 6 & !7] 100
[0 & !1 & 2 & !3 & !4 & 5 & 6 & !7] 101
[1] 0
State: 1 [@x] 9
State: 2 [@x] 9
State: 3 [@x] 9
State: 4 [@x] 9
State: 5 [@x] 9
State: 6 [@x] 9
State: 7 [@x] 9
State: 8 [@x] 9
State: 9 {0}
[0 & 1 & !2 & 3 & 4 & 5 & !6 & !7] 1
[!0 & !1 & !2 & 3 & 4 & !5 & 6 & !7] 2
[0 & !1 & !2 & 3 & 4 & 5 & !6 & !7] 3
[!0 & 1 & 2 & !3 & 4 & 5 & !6 & !7] 4
[0 & !1 & 2 & !3 & 4 & 5 & !6 & !7] 5
[0 & 1 & !2 & !3 & 4 & 5 & !6 & !7] 6
[!0 & 1 & 2 & 3 & 4 & !5 & !6 & !7] 7
[!0 & 1 & !2 & !3 & 4 & 5 & !6 & !7] 8
[!0 & !1 & 2 & 3 & !4 & !5 & 6 & !7] 10
[!0 & !1 & !2 & !3 & 4 & 5 & !6 & !7] 11
[!0 & !1 & 2 & 3 & 4 & !5 & !6 & !7] 12
[!0 & 1 & 2 & 3 & !4 & 5 & !6 & !7] 36
[0 & !1 & 2 & 3 & !4 & 5 & !6 & !7] 13
[0 & !1 & !2 & 3 & 4 & !5 & !6 & !7] 14
[!0 & !1 & 2 & 3 & !4 & 5 & !6 & !7] 15
[0 & 1 & !2 & !3 & !4 & !5 & 6 & !7] 16
[0 & 1 & !2 & 3 & !4 & 5 & !6 & !7] 17
[!0 & !1 & !2 & 3 & !4 & !5 & !6 & !7] 18
[!0 & !1 & !2 & !3 & !4 & 5 & 6 & !7] 19
[0 & !1 & !2 & 3 & !4 & 5 & !6 & !7] 20
[!0 & !1 & !2 & 3 & !4 & 5 & !6 & !7] 21
[!0 & 1 & 2 & !3 & 4 & !5 & !6 & !7] 22
[0 & 1 & 2 & 3 & 4 & !5 & 6 & !7] 23
[0 & 1 & 2 & !3 & !4 & 5 & !6 & !7] 24
[!0 & !1 & 2 & !3 & 4 & !5 & !6 & !7] 25
[!0 & !1 & 2 & !3 & !4 & 5 & !6 & !7] 26
[0 & 1 & !2 & !3 & 4 & !5 & !6 & !7] 27
[0 & !1 & !2 & !3 & !4 & 5 & !6 & !7] 28
[!0 & !1 & 2 & 3 & 4 & 5 & !6 & !7] 75
[0 & 1 & 2 & 3 & 4 & !5 & !6 & !7] 29
[!0 & 1 & 2 & !3 & !4 & 5 & !6 & !7] 55
[!0 & 1 & 2 & 3 & !4 & !5 & !6 & !7] 56
[!0 & !1 & !2 & !3 & !4 & 5 & !6 & !7] 57
[0 & !1 & !2 & !3 & 4 & !5 & !6 & !7] 60
[!0 & 1 & !2 & !3 & !4 & 5 & !6 & !7] 61
[0 & !1 & 2 & !3 & 4 & !5 & 6 & !7] 62
[0 & 1 & !2 & 3 & !4 & !5 & !6 & !7] 58
[!0 & 1 & !2 & 3 & 4 & !5 & !6 & !7] 59
[0 & !1 & 2 & !3 & 4 & !5 & !6 & !7] 32
[0 & 1 & 2 & !3 & !4 & !5 & !6 & !7] 33
[!0 & !1 & 2 & 3 & 4 & !5 & 6 & !7] 34
[0 & !1 & !2 & 3 & !4 & !5 & !6 & !7] 35
[0 & 1 & 2 & 3 & !4 & 5 & !6 & !7] 37
[!0 & 1 & 2 & !3 & !4 & !5 & 6 & !7] 38
[0 & 1 & 2 & !3 & 4 & 5 & !6 & !7] 39
[!0 & 1 & !2 & !3 & 4 & !5 & 6 & !7] 40
[!0 & 1 & !2 & !3 & 4 & !5 & !6 & !7] 41
[0 & 1 & 2 & !3 & 4 & !5 & !6 & !7] 42
[!0 & !1 & !2 & 3 & 4 & 5 & !6 & !7] 43
[0 & !1 & 2 & 3 & !4 & !5 & !6 & !7] 44
[0 & !1 & 2 & 3 & 4 & !5 & !6 & !7] 45
[!0 & 1 & !2 & 3 & !4 & 5 & !6 & !7] 46
[!0 & 1 & !2 & 3 & !4 & !5 & !6 & !7] 47
[!0 & !1 & 2 & !3 & !4 & !5 & 6 & !7] 48
[!0 & !1 & 2 & !3 & !4 & !5 & !6 & !7] 49
[!0 & 1 & 2 & !3 & 4 & !5 & 6 & !7] 50
[!0 & !1 & 2 & 3 & !4 & !5 & !6 & !7] 51
[!0 & 1 & 2 & !3 & !4 & !5 & !6 & !7] 52
[0 & 1 & !2 & 3 & 4 & !5 & 6 & !7] 53
[0 & 1 & !2 & 3 & 4 & !5 & !6 & !7] 54
[0 & 1 & 2 & 3 & !4 & !5 & !6 & !7] 63
[!0 & !1 & 2 & !3 & 4 & 5 & !6 & !7] 64
[!0 & !1 & !2 & !3 & 4 & !5 & !6 & !7] 65
[0 & 1 & !2 & !3 & !4 & 5 & !6 & !7] 66
[0 & !1 & 2 & !3 & !4 & 5 & !6 & !7] 67
[0 & 1 & !2 & !3 & !4 & !5 & !6 & !7] 68
[0 & !1 & !2 & !3 & 4 & !5 & 6 & !7] 69
[!0 & !1 & !2 & 3 & 4 & !5 & !6 & !7] 70
[0 & 1 & !2 & !3 & !4 & 5 & 6 & !7] 71
[0 & !1 & 2 & !3 & !4 & !5 & !6 & !7] 72
[!0 & 1 & !2 & 3 & 4 & 5 & !6 & !7] 73
[!0 & 1 & !2 & !3 & !4 & !5 & !6 & !7] 74
[0 & !1 & !2 & !3 & 4 & 5 & !6 & !7] 30
[0 & 1 & !2 & 3 & !4 & !5 & 6 & !7] 31
[0 & !1 & 2 & 3 & 4 & 5 & !6 & !7] 76
[!0 & 1 & 2 & 3 & 4 & 5 & !6 & !7] 77
[0 & 1 & 2 & 3 & 4 & 5 & !6 & !7] 78
[!0 & !1 & !2 & !3 & !4 & !5 & 6 & !7] 79
[0 & !1 & !2 & !3 & !4 & !5 & 6 & !7] 80
[!0 & 1 & !2 & !3 & !4 & !5 & 6 & !7] 81
[0 & !1 & 2 & !3 & !4 & !5 & 6 & !7] 82
[0 & 1 & 2 & !3 & !4 & !5 & 6 & !7] 83
[!0 & !1 & !2 & 3 & !4 & !5 & 6 & !7] 84
[0 & !1 & !2 & 3 & !4 & !5 & 6 & !7] 85
[!0 & 1 & !2 & 3 & !4 & !5 & 6 & !7] 86
[0 & !1 & 2 & 3 & !4 & !5 & 6 & !7] 87
[!0 & 1 & 2 & 3 & !4 & !5 & 6 & !7] 88
[0 & 1 & 2 & 3 & !4 & !5 & 6 & !7] 89
[!0 & !1 & !2 & !3 & 4 & !5 & 6 & !7] 90
[0 & 1 & !2 & !3 & 4 & !5 & 6 & !7] 91
[!0 & !1 & 2 & !3 & 4 & !5 & 6 & !7] 92
[0 & 1 & 2 & !3 & 4 & !5 & 6 & !7] 93
[0 & !1 & !2 & 3 & 4 & !5 & 6 & !7] 94
[!0 & 1 & !2 & 3 & 4 & !5 & 6 & !7] 95
[0 & !1 & 2 & 3 & 4 & !5 & 6 & !7] 96
[!0 & 1 & 2 & 3 & 4 & !5 & 6 & !7] 97
[0 & !1 & !2 & !3 & !4 & 5 & 6 & !7] 98
[!0 & 1 & !2 & !3 & !4 & 5 & 6 & !7] 99
[!0 & !1 & 2 & !3 & !4 & 5 & 6 & !7] 100
[0 & !1 & 2 & !3 & !4 & 5 & 6 & !7] 101
State: 10 [@x] 9
State: 11 [@x] 9
State: 12 [@x] 9
State: 13 [@x] 9
State: 14 [@x] 9
State: 15 [@x] 9
State: 16 [@x] 9
State: 17 [@x] 9
State: 18 [@x] 9
State: 19 [@x] 9
State: 20 [@x] 9
State: 21 [@x] 9
State: 22 [@x] 9
State: 23 [@x] 9
State: 24 [@x] 9
State: 25 [@x] 9
State: 26 [@x] 9
State: 27 [@x] 9
State: 28 [@x] 9
State: 29 [@x] 9
State: 30 [@x] 9
State: 31 [@x] 9
State: 32 [@x] 9
State: 33 [@x] 9
State: 34 [@x] 9
State: 35 [@x] 9
State: 36 [@x] 9
State: 37 [@x] 9
State: 38 [@x] 9
State: 39 [@x] 9
State: 40 [@x] 9
State: 41 [@x] 9
State: 42 [@x] 9
State: 43 [@x] 9
State: 44 [@x] 9
State: 45 [@x] 9
State: 46 [@x] 9
State: 47 [@x] 9
State: 48 [@x] 9
State: 49 [@x] 9
State: 50 [@x] 9
State: 51 [@x] 9
State: 52 [@x] 9
State: 53 [@x] 9
State: 54 [@x] 9
State: 55 [@x] 9
State: 56 [@x] 9
State: 57 [@x] 9
State: 58 [@x] 9
State: 59 [@x] 9
State: 60 [@x] 9
State: 61 [@x] 9
State: 62 [@x] 9
State: 63 [@x] 9
State: 64 [@x] 9
State: 65 [@x] 9
State: 66 [@x] 9
State: 67 [@x] 9
State: 68 [@x] 9
State: 69 [@x] 9
State: 70 [@x] 9
State: 71 [@x] 9
State: 72 [@x] 9
State: 73 [@x] 9
State: 74 [@x] 9
State: 75 [@x] 9
State: 76 [@x] 9
State: 77 [@x] 9
State: 78 [@x] 9
State: 79 [@x] 9
State: 80 [@x] 9
State: 81 [@x] 9
State: 82 [@x] 9
State: 83 [@x] 9
State: 84 [@x] 9
State: 85 [@x] 9
State: 86 [@x] 9
State: 87 [@x] 9
State: 88 [@x] 9
State: 89 [@x] 9
State: 90 [@x] 9
State: 91 [@x] 9
State: 92 [@x] 9
State: 93 [@x] 9
State: 94 [@x] 9
State: 95 [@x] 9
State: 96 [@x] 9
State: 97 [@x] 9
State: 98 [@x] 9
State: 99 [@x] 9
State: 100 [@x] 9
State: 101 [@x] 9
--END--
EOF
test 4 = `autfilt --complement large.hoa --stats=%s`
: