alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/tests/core/autcross5.test
Alexandre Duret-Lutz 150f815c87 sccinfo: fix generation of self-loop accepting runs 
Reported by Juraj Major.

* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Do not
assume TRACK_STATES is enabled.
* tests/core/autcross5.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
2020-03-12 17:06:03 +01:00

200 lines
12 KiB
Bash
Executable file
Raw Blame History

#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2020 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
# Based on a report by Juraj Major.
cat >a7.hoa <<EOF
HOA: v1 States: 34 Start: 0 AP: 5 "a" "b" "c" "d" "e" Acceptance:
7 (Fin(1) | Inf(2)) & (Fin(0) | Inf(5)) & (Inf(3)&Inf(4)&Inf(6))
properties: trans-labels explicit-labels trans-acc --BODY-- State:
0 [1&!2&4] 1 [0&1&2 | 1&!2&!4 | 1&2&3] 2 [!0&1&2&!3&4] 3 [0&1&2&4 |
1&2&3&4] 4 [!0&1&2&!3&!4] 5 [0&1&2&!4 | 1&2&3&!4] 6 [!1&!2&!4] 7 [!1&2&!4]
8 [!1&2&4] 9 [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11 [!1&2&!4] 12 [!1&!2] 13
[0&!1&2 | !1&2&3] 14 State: 1 [1&!2&4] 1 {3 4 6} [0&1&2&!4 | 1&2&3&!4]
2 {6} [0&1&2&4 | 1&2&3&4] 2 {3 6} [1&!2&!4] 2 {4 6} [!0&1&2&!3&4]
3 {3 6} [0&1&2&4 | 1&2&3&4] 4 {3 6} [!0&1&2&!3&!4] 5 {6} [0&1&2&!4 |
1&2&3&!4] 6 {6} [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11 State: 2 [1&!2&4]
1 {3 4 6} [0&1&2&!4 | 1&2&3&!4] 2 {6} [0&1&2&4 | 1&2&3&4] 2 {3 6}
[1&!2&!4] 2 {4 6} [!0&1&2&!3&4] 3 {3 6} [0&1&2&4 | 1&2&3&4] 4 {3 6}
[!0&1&2&!3&!4] 5 {6} [0&1&2&!4 | 1&2&3&!4] 6 {6} State: 3 [1&!2&4]
1 {3 4 6} [0&1&2&!4 | 1&2&3&!4] 2 {6} [0&1&2&4 | 1&2&3&4] 2 {3 6}
[1&!2&!4] 2 {4 6} [!0&1&2&!3&4] 3 {3 6} [0&1&2&4 | 1&2&3&4] 4 {3 6}
[!0&1&2&!3&!4] 5 {6} [0&1&2&!4 | 1&2&3&!4] 6 {6} [!1&!2&!4] 7 [!1&2&!4]
8 [!1&!2] 13 [0&!1&2 | !1&2&3] 15 State: 4 [!0&1&!2&!3&4] 1 {3 4 5 6}
[!0&1&!2&!3&!4] 2 {4 5 6} [!0&1&2&!3&4] 3 {3 5 6} [!0&1&2&!3&!4] 5 {5 6}
[!0&!1&!2&!3&!4] 7 [!0&!1&2&!3&!4] 8 [!0&!1&!2&!3] 13 [!0&1&!2&3&4] 16
{3 4 6} [0&1&!2&4] 16 {0 3 4 6} [!0&1&!2&3&!4] 17 {4 6} [0&1&!2&!4] 17
{0 4 6} [0&!1&!2&!4 | !1&!2&3&!4] 18 [0&!1&!2 | !1&!2&3] 19 [0&!1&2&!4 |
!1&2&3&!4] 20 State: 5 [1&!2&4] 1 {3 4 6} [0&1&2&!4 | 1&2&3&!4] 2 {6}
[0&1&2&4 | 1&2&3&4] 2 {3 6} [1&!2&!4] 2 {4 6} [!0&1&2&!3&4] 3 {3 6}
[0&1&2&4 | 1&2&3&4] 4 {3 6} [!0&1&2&!3&!4] 5 {6} [0&1&2&!4 | 1&2&3&!4]
6 {6} [!1&!2&4] 13 [0&!1&2&4 | !1&2&3&4] 15 [!1&!2&!4] 21 [0&!1&2&!4 |
!1&2&3&!4] 22 State: 6 [!0&1&!2&!3&4] 1 {3 4 5 6} [!0&1&!2&!3&!4] 2 {4
5 6} [!0&1&2&!3&4] 3 {3 5 6} [!0&1&2&!3&!4] 5 {5 6} [!0&!1&!2&!3&4] 13
[!0&1&!2&3&4] 16 {3 4 6} [0&1&!2&4] 16 {0 3 4 6} [!0&1&!2&3&!4] 17 {4 6}
[0&1&!2&!4] 17 {0 4 6} [0&!1&!2&4 | !1&!2&3&4] 19 [!0&!1&!2&!3&!4] 21
[0&!1&!2&!4 | !1&!2&3&!4] 23 State: 7 [!1&!2&!4] 7 {3 4 6} [!1&2&!4]
8 {3 6} [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11 [0&!1&2&!4 | !1&2&3&!4]
24 State: 8 [!1&!2&!4] 7 {3 4 6} [!1&2&!4] 8 {3 6} State: 9 [!1&2&4] 9
{3 4 6} [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11 [!1&2&!4] 12 {4 6} [0&!1&2 |
!1&2&3] 25 State: 10 [1&2&!4] 10 {3 4 6} [0&1&2&!4 | 1&2&3&!4] 11 {3 4 6}
State: 11 [!0&1&2&!3&!4] 10 {3 4 5 6} [!0&1&2&3&!4] 11 {3 4 6} [0&1&2&!4]
11 {0 3 4 6} State: 12 [!1&2&4] 9 {3 4 6} [!1&2&!4] 12 {4 6} State: 13
[!1&!2&!4] 7 [!1&2&!4] 8 [!1&2&4] 9 [!1&2&!4] 12 [!1&!2] 13 [0&!1&2 |
!1&2&3] 14 State: 14 [0&!1] 14 [!0&!1&3] 14 {1} [0&!1&!2&!4 | !1&!2&3&!4]
26 [0&!1&2&!4 | !1&2&3&!4] 27 [0&!1&2&4 | !1&2&3&4] 28 [0&!1&2&!4 |
!1&2&3&!4] 29 State: 15 [0&!1&!2 | !1&!2&3] 14 [0&!1&2] 15 [!0&!1&2&3]
15 {1} [0&!1&!2&!4 | !1&!2&3&!4] 26 [0&!1&2&!4 | !1&2&3&!4] 27 State:
16 [!0&1&!2&!3&4] 1 {3 4 5 6} [!0&1&!2&!3&!4] 2 {4 5 6} [!0&1&2&!3&4]
3 {3 5 6} [!0&1&2&!3&!4] 5 {5 6} [!0&1&2&!3&!4] 10 [!0&1&!2&3&4] 16
{3 4 6} [0&1&!2&4] 16 {0 3 4 6} [!0&1&!2&3&!4] 17 {4 6} [0&1&!2&!4] 17
{0 4 6} State: 17 [!0&1&!2&!3&4] 1 {3 4 5 6} [!0&1&!2&!3&!4] 2 {4 5 6}
[!0&1&2&!3&4] 3 {3 5 6} [!0&1&2&!3&!4] 5 {5 6} [!0&1&!2&3&4] 16 {3 4 6}
[0&1&!2&4] 16 {0 3 4 6} [!0&1&!2&3&!4] 17 {4 6} [0&1&!2&!4] 17 {0 4 6}
State: 18 [!0&!1&!2&!3&!4] 7 [!0&!1&2&!3&!4] 8 [!0&1&2&!3&!4] 10 [0&1&2&!4
| 1&2&3&!4] 11 [!0&!1&!2&3&!4] 18 {3 4 6} [0&!1&!2&!4] 18 {0 3 4 6}
[!0&!1&2&3&!4] 20 {3 6} [0&!1&2&!4] 20 {0 3 6} State: 19 [!0&!1&!2&!3&!4]
7 [!0&!1&2&!3&!4] 8 [!0&!1&2&!3&4] 9 [!0&!1&2&!3&!4] 12 [!0&!1&!2&!3] 13
[0&!1&!2&!4 | !1&!2&3&!4] 18 [!0&!1&!2&3] 19 [0&!1&!2] 19 {0} [0&!1&2&!4 |
!1&2&3&!4] 20 [0&!1&2&4 | !1&2&3&4] 30 [0&!1&2&!4 | !1&2&3&!4] 31 State:
20 [!0&!1&!2&!3&!4] 7 [!0&!1&2&!3&!4] 8 [!0&!1&!2&3&!4] 18 {3 4 6}
[0&!1&!2&!4] 18 {0 3 4 6} [!0&!1&2&3&!4] 20 {3 6} [0&!1&2&!4] 20 {0 3 6}
State: 21 [!1&2&4] 9 [!1&2&!4] 12 [!1&!2&4] 13 [0&!1&2&4 | !1&2&3&4] 14
[!1&!2&!4] 21 [0&!1&2&!4 | !1&2&3&!4] 32 State: 22 [0&!1&!2&4 | !1&!2&3&4]
14 [0&!1&2&4 | !1&2&3&4] 15 [0&!1&2&!4] 22 [!0&!1&2&3&!4] 22 {1}
[0&!1&!2&!4 | !1&!2&3&!4] 32 State: 23 [!0&!1&2&!3&4] 9 [!0&!1&2&!3&!4]
12 [!0&!1&!2&!3&4] 13 [0&!1&!2&4 | !1&!2&3&4] 19 [!0&!1&!2&!3&!4] 21
[!0&!1&!2&3&!4] 23 [0&!1&!2&!4] 23 {0} [0&!1&2&4 | !1&2&3&4] 30 [0&!1&2&!4
| !1&2&3&!4] 31 State: 24 [!0&!1&2&3&!4] 24 {1 3 4} [0&!1&2&!4] 24 {2 3 4}
[!0&!1&!2&3&!4] 26 {1 3 4 6} [0&!1&!2&!4] 26 {2 3 4 6} [!0&!1&2&3&!4]
27 {1 3 6} [0&!1&2&!4] 27 {2 3 6} State: 25 [!0&!1&2&3&!4] 25 {1 3 4}
[0&!1&2&!4] 25 {2 3 4} [!0&!1&2&3&4] 28 {1 3 4 6} [0&!1&2&4] 28 {2
3 4 6} [!0&!1&2&3&!4] 29 {1 4 6} [0&!1&2&!4] 29 {2 4 6} State: 26
[!0&!1&2&3&!4] 24 {1 3 4} [0&!1&2&!4] 24 {2 3 4} [!0&!1&!2&3&!4] 26 {1
3 4 6} [0&!1&!2&!4] 26 {2 3 4 6} [!0&!1&2&3&!4] 27 {1 3 6} [0&!1&2&!4]
27 {2 3 6} [0&1&2&!4 | 1&2&3&!4] 33 State: 27 [!0&!1&!2&3&!4] 26 {1 3 4 6}
[0&!1&!2&!4] 26 {2 3 4 6} [!0&!1&2&3&!4] 27 {1 3 6} [0&!1&2&!4] 27 {2 3 6}
State: 28 [!0&!1&2&3&!4] 25 {1 3 4} [0&!1&2&!4] 25 {2 3 4} [!0&!1&2&3&4]
28 {1 3 4 6} [0&!1&2&4] 28 {2 3 4 6} [!0&!1&2&3&!4] 29 {1 4 6} [0&!1&2&!4]
29 {2 4 6} [0&1&2&!4 | 1&2&3&!4] 33 State: 29 [!0&!1&2&3&4] 28 {1 3 4 6}
[0&!1&2&4] 28 {2 3 4 6} [!0&!1&2&3&!4] 29 {1 4 6} [0&!1&2&!4] 29 {2 4
6} State: 30 [!0&!1&2&!3&4] 9 [!0&1&2&!3&!4] 10 [0&1&2&!4 | 1&2&3&!4]
11 [!0&!1&2&!3&!4] 12 [!0&!1&2&3&4] 30 {3 4 6} [0&!1&2&4] 30 {0 3 4 6}
[!0&!1&2&3&!4] 31 {4 6} [0&!1&2&!4] 31 {0 4 6} State: 31 [!0&!1&2&!3&4]
9 [!0&!1&2&!3&!4] 12 [!0&!1&2&3&4] 30 {3 4 6} [0&!1&2&4] 30 {0 3 4 6}
[!0&!1&2&3&!4] 31 {4 6} [0&!1&2&!4] 31 {0 4 6} State: 32 [0&!1&4 |
!1&3&4] 14 [0&!1&2&4 | !1&2&3&4] 28 [0&!1&2&!4 | !1&2&3&!4] 29 [0&!1&!4]
32 [!0&!1&3&!4] 32 {1} State: 33 [!0&1&2&3&!4] 33 {1 3 4 6} [0&1&2&!4]
33 {2 3 4 6} --END--
EOF
cat >_a7.hoa <<EOF
HOA: v1 States: 34 Start: 0 AP: 5 "a" "b" "c" "d" "e" Acceptance:
6 (Fin(0) & (Inf(1)&Inf(2))) | (Inf(3)&Inf(4)&Inf(5)) properties:
trans-labels explicit-labels trans-acc --BODY-- State: 0 [1&!2&4]
1 [0&1&2 | 1&!2&!4 | 1&2&3] 2 [!0&1&2&!3&4] 3 [0&1&2&4 | 1&2&3&4]
4 [!0&1&2&!3&!4] 5 [0&1&2&!4 | 1&2&3&!4] 6 [!1&!2&!4] 7 [!1&2&!4] 8
[!1&2&4] 9 [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11 [!1&2&!4] 12 [!1&!2] 13
[0&!1&2 | !1&2&3] 14 State: 1 [1&!2&4] 1 {1 2 3 4} [0&1&2&!4 | 1&2&3&!4]
2 [0&1&2&4 | 1&2&3&4] 2 {1 3} [1&!2&!4] 2 {2 4} [!0&1&2&!3&4] 3 {1 3}
[0&1&2&4 | 1&2&3&4] 4 {1 3} [!0&1&2&!3&!4] 5 [0&1&2&!4 | 1&2&3&!4]
6 [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11 State: 2 [1&!2&4] 1 {1 2 3 4}
[0&1&2&!4 | 1&2&3&!4] 2 [0&1&2&4 | 1&2&3&4] 2 {1 3} [1&!2&!4] 2 {2 4}
[!0&1&2&!3&4] 3 {1 3} [0&1&2&4 | 1&2&3&4] 4 {1 3} [!0&1&2&!3&!4]
5 [0&1&2&!4 | 1&2&3&!4] 6 State: 3 [1&!2&4] 1 {1 2 3 4} [0&1&2&!4 |
1&2&3&!4] 2 [0&1&2&4 | 1&2&3&4] 2 {1 3} [1&!2&!4] 2 {2 4} [!0&1&2&!3&4] 3
{1 3} [0&1&2&4 | 1&2&3&4] 4 {1 3} [!0&1&2&!3&!4] 5 [0&1&2&!4 | 1&2&3&!4]
6 [!1&!2&!4] 7 [!1&2&!4] 8 [!1&!2] 13 [0&!1&2 | !1&2&3] 15 State: 4
[!0&1&!2&!3&4] 1 {1 2 3 4 5} [!0&1&!2&!3&!4] 2 {2 4 5} [!0&1&2&!3&4]
3 {1 3 5} [!0&1&2&!3&!4] 5 {5} [!0&!1&!2&!3&!4] 7 [!0&!1&2&!3&!4] 8
[!0&!1&!2&!3] 13 [!0&1&!2&3&4] 16 {1 2 3 4} [0&1&!2&4] 16 {0 1 2 3 4}
[!0&1&!2&3&!4] 17 {2 4} [0&1&!2&!4] 17 {0 2 4} [0&!1&!2&!4 | !1&!2&3&!4]
18 [0&!1&!2 | !1&!2&3] 19 [0&!1&2&!4 | !1&2&3&!4] 20 State: 5 [1&!2&4]
1 {1 2 3 4} [0&1&2&!4 | 1&2&3&!4] 2 [0&1&2&4 | 1&2&3&4] 2 {1 3} [1&!2&!4]
2 {2 4} [!0&1&2&!3&4] 3 {1 3} [0&1&2&4 | 1&2&3&4] 4 {1 3} [!0&1&2&!3&!4] 5
[0&1&2&!4 | 1&2&3&!4] 6 [!1&!2&4] 13 [0&!1&2&4 | !1&2&3&4] 15 [!1&!2&!4]
21 [0&!1&2&!4 | !1&2&3&!4] 22 State: 6 [!0&1&!2&!3&4] 1 {1 2 3 4 5}
[!0&1&!2&!3&!4] 2 {2 4 5} [!0&1&2&!3&4] 3 {1 3 5} [!0&1&2&!3&!4]
5 {5} [!0&!1&!2&!3&4] 13 [!0&1&!2&3&4] 16 {1 2 3 4} [0&1&!2&4] 16 {0
1 2 3 4} [!0&1&!2&3&!4] 17 {2 4} [0&1&!2&!4] 17 {0 2 4} [0&!1&!2&4 |
!1&!2&3&4] 19 [!0&!1&!2&!3&!4] 21 [0&!1&!2&!4 | !1&!2&3&!4] 23 State:
7 [!1&!2&!4] 7 {1 2} [!1&2&!4] 8 {2} [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4]
11 [0&!1&2&!4 | !1&2&3&!4] 24 State: 8 [!1&!2&!4] 7 {1 2} [!1&2&!4]
8 {2} State: 9 [!1&2&4] 9 {1 2} [1&2&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11
[!1&2&!4] 12 {2} [0&!1&2 | !1&2&3] 25 State: 10 [1&2&!4] 10 {1 2 4 5}
[0&1&2&!4 | 1&2&3&!4] 11 {1 2 4 5} State: 11 [!0&1&2&!3&!4] 10 {1 2 3 4 5}
[!0&1&2&3&!4] 11 {1 2 4 5} [0&1&2&!4] 11 {0 1 2 4 5} State: 12 [!1&2&4]
9 {1 2} [!1&2&!4] 12 {2} State: 13 [!1&!2&!4] 7 [!1&2&!4] 8 [!1&2&4] 9
[!1&2&!4] 12 [!1&!2] 13 [0&!1&2 | !1&2&3] 14 State: 14 [0&!1] 14 [!0&!1&3]
14 [0&!1&!2&!4 | !1&!2&3&!4] 26 [0&!1&2&!4 | !1&2&3&!4] 27 [0&!1&2&4 |
!1&2&3&4] 28 [0&!1&2&!4 | !1&2&3&!4] 29 State: 15 [0&!1&!2 | !1&!2&3]
14 [0&!1&2] 15 [!0&!1&2&3] 15 [0&!1&!2&!4 | !1&!2&3&!4] 26 [0&!1&2&!4 |
!1&2&3&!4] 27 State: 16 [!0&1&!2&!3&4] 1 {1 2 3 4 5} [!0&1&!2&!3&!4]
2 {2 4 5} [!0&1&2&!3&4] 3 {1 3 5} [!0&1&2&!3&!4] 5 {5} [!0&1&2&!3&!4]
10 [!0&1&!2&3&4] 16 {1 2 3 4} [0&1&!2&4] 16 {0 1 2 3 4} [!0&1&!2&3&!4]
17 {2 4} [0&1&!2&!4] 17 {0 2 4} State: 17 [!0&1&!2&!3&4] 1 {1 2 3 4 5}
[!0&1&!2&!3&!4] 2 {2 4 5} [!0&1&2&!3&4] 3 {1 3 5} [!0&1&2&!3&!4] 5 {5}
[!0&1&!2&3&4] 16 {1 2 3 4} [0&1&!2&4] 16 {0 1 2 3 4} [!0&1&!2&3&!4] 17 {2
4} [0&1&!2&!4] 17 {0 2 4} State: 18 [!0&!1&!2&!3&!4] 7 [!0&!1&2&!3&!4]
8 [!0&1&2&!3&!4] 10 [0&1&2&!4 | 1&2&3&!4] 11 [!0&!1&!2&3&!4] 18 {1 2}
[0&!1&!2&!4] 18 {0 1 2} [!0&!1&2&3&!4] 20 {2} [0&!1&2&!4] 20 {0 2} State:
19 [!0&!1&!2&!3&!4] 7 [!0&!1&2&!3&!4] 8 [!0&!1&2&!3&4] 9 [!0&!1&2&!3&!4]
12 [!0&!1&!2&!3] 13 [0&!1&!2&!4 | !1&!2&3&!4] 18 [!0&!1&!2&3] 19
[0&!1&!2] 19 [0&!1&2&!4 | !1&2&3&!4] 20 [0&!1&2&4 | !1&2&3&4] 30
[0&!1&2&!4 | !1&2&3&!4] 31 State: 20 [!0&!1&!2&!3&!4] 7 [!0&!1&2&!3&!4]
8 [!0&!1&!2&3&!4] 18 {1 2} [0&!1&!2&!4] 18 {0 1 2} [!0&!1&2&3&!4] 20 {2}
[0&!1&2&!4] 20 {0 2} State: 21 [!1&2&4] 9 [!1&2&!4] 12 [!1&!2&4] 13
[0&!1&2&4 | !1&2&3&4] 14 [!1&!2&!4] 21 [0&!1&2&!4 | !1&2&3&!4] 32 State:
22 [0&!1&!2&4 | !1&!2&3&4] 14 [0&!1&2&4 | !1&2&3&4] 15 [0&!1&2&!4] 22
[!0&!1&2&3&!4] 22 [0&!1&!2&!4 | !1&!2&3&!4] 32 State: 23 [!0&!1&2&!3&4]
9 [!0&!1&2&!3&!4] 12 [!0&!1&!2&!3&4] 13 [0&!1&!2&4 | !1&!2&3&4] 19
[!0&!1&!2&!3&!4] 21 [!0&!1&!2&3&!4] 23 [0&!1&!2&!4] 23 [0&!1&2&4 |
!1&2&3&4] 30 [0&!1&2&!4 | !1&2&3&!4] 31 State: 24 [!0&!1&2&3&!4]
24 {0 1 2 4} [0&!1&2&!4] 24 {1 2 3 4} [!0&!1&!2&3&!4] 26 {0 1 2 4 5}
[0&!1&!2&!4] 26 {1 2 3 4 5} [!0&!1&2&3&!4] 27 {0 1 2 5} [0&!1&2&!4] 27
{1 2 3 5} State: 25 [!0&!1&2&3&!4] 25 {0 1 2 4} [0&!1&2&!4] 25 {1 2 3 4}
[!0&!1&2&3&4] 28 {0 1 2 4 5} [0&!1&2&4] 28 {1 2 3 4 5} [!0&!1&2&3&!4] 29
{0 1 2 5} [0&!1&2&!4] 29 {1 2 3 5} State: 26 [!0&!1&2&3&!4] 24 {0 1 2 4}
[0&!1&2&!4] 24 {1 2 3 4} [!0&!1&!2&3&!4] 26 {0 1 2 4 5} [0&!1&!2&!4] 26 {1
2 3 4 5} [!0&!1&2&3&!4] 27 {0 1 2 5} [0&!1&2&!4] 27 {1 2 3 5} [0&1&2&!4
| 1&2&3&!4] 33 State: 27 [!0&!1&!2&3&!4] 26 {0 1 2 4 5} [0&!1&!2&!4] 26
{1 2 3 4 5} [!0&!1&2&3&!4] 27 {0 1 2 5} [0&!1&2&!4] 27 {1 2 3 5} State:
28 [!0&!1&2&3&!4] 25 {0 1 2 4} [0&!1&2&!4] 25 {1 2 3 4} [!0&!1&2&3&4]
28 {0 1 2 4 5} [0&!1&2&4] 28 {1 2 3 4 5} [!0&!1&2&3&!4] 29 {0 1 2 5}
[0&!1&2&!4] 29 {1 2 3 5} [0&1&2&!4 | 1&2&3&!4] 33 State: 29 [!0&!1&2&3&4]
28 {0 1 2 4 5} [0&!1&2&4] 28 {1 2 3 4 5} [!0&!1&2&3&!4] 29 {0 1 2 5}
[0&!1&2&!4] 29 {1 2 3 5} State: 30 [!0&!1&2&!3&4] 9 [!0&1&2&!3&!4]
10 [0&1&2&!4 | 1&2&3&!4] 11 [!0&!1&2&!3&!4] 12 [!0&!1&2&3&4] 30 {1 2}
[0&!1&2&4] 30 {0 1 2} [!0&!1&2&3&!4] 31 {2} [0&!1&2&!4] 31 {0 2} State:
31 [!0&!1&2&!3&4] 9 [!0&!1&2&!3&!4] 12 [!0&!1&2&3&4] 30 {1 2} [0&!1&2&4]
30 {0 1 2} [!0&!1&2&3&!4] 31 {2} [0&!1&2&!4] 31 {0 2} State: 32 [0&!1&4 |
!1&3&4] 14 [0&!1&2&4 | !1&2&3&4] 28 [0&!1&2&!4 | !1&2&3&!4] 29 [0&!1&!4]
32 [!0&!1&3&!4] 32 State: 33 [!0&1&2&3&!4] 33 {0 1 2 4 5} [0&1&2&!4]
33 {1 2 3 4 5} --END--
EOF
# The following command used to do segfault or loop infinitely
# due to an incorrectly generated counterexample.
autcross -F a7.hoa 'autfilt' ': %H && cat _a7.hoa > %O' 2>stderr && exit 2
cat stderr
grep 'both automata accept the infinite word:' stderr
Reference in a new issue View git blame Copy permalink