a325de8678
* spot/twaalgos/postproc.cc: Here. * spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Fix some bug uncovered by the new simplified automata. * tests/core/satmin2.test, tests/core/sccdot.test, tests/core/sim3.test, tests/python/decompose.ipynb, tests/python/satmin.ipynb: Update expected results. * NEWS: Mention the simplification and the bug.
208 lines
3.7 KiB
Bash
Executable file
208 lines
3.7 KiB
Bash
Executable file
#!/bin/sh
|
|
# -*- coding: utf-8 -*-
|
|
# Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et
|
|
# Développement de l'Epita
|
|
#
|
|
# 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
|
|
|
|
# Check the scc_info categorization of SCCs as accepting/rejecting
|
|
# by looking at the dot output.
|
|
cat <<EOF > in.hoa
|
|
HOA: v1
|
|
States: 11
|
|
Start: 1
|
|
AP: 2 "a" "b"
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 3 Inf(0)&Inf(1)&Fin(2)
|
|
--BODY--
|
|
State: 0 {2}
|
|
[0&1] 0 {0 1}
|
|
[!0&!1] 0
|
|
[0] 5
|
|
State: 1
|
|
[1] 4
|
|
[0&!1] 3
|
|
State: 4
|
|
[!1] 4 {1 2}
|
|
[1] 2
|
|
State: 2
|
|
[0] 0
|
|
[1] 7
|
|
State: 3
|
|
[0&1] 1 {1 0}
|
|
State: 5
|
|
[t] 6
|
|
State: 6
|
|
[t] 5
|
|
State: 7
|
|
[!0&1] 7 {0 1} /* This state and the next one differs by */
|
|
[0&1] 7 {0 2} /* the order of the self loops. */
|
|
[t] 8
|
|
State: 8
|
|
[!0&1] 8 {0 2}
|
|
[0&1] 8 {0 1}
|
|
[t] 9
|
|
State: 9
|
|
[!0&1] 9 {0 2}
|
|
[0&1] 10 {0 1}
|
|
State: 10
|
|
[!0&1] 9 {0 1}
|
|
[0&1] 10 {0 2}
|
|
--END--
|
|
EOF
|
|
|
|
run 0 autfilt --dot=as in.hoa > out.dot
|
|
|
|
# The important stuff is the color=xxx lines
|
|
cat <<EOF >expected
|
|
digraph "" {
|
|
rankdir=LR
|
|
label="(Inf(0)&Inf(1)) & Fin(2)\n[Streett-like 3]"
|
|
labelloc="t"
|
|
node [shape="circle"]
|
|
I [label="", style=invis, width=0]
|
|
I -> 1
|
|
subgraph cluster_0 {
|
|
color=grey
|
|
label=""
|
|
5 [label="5"]
|
|
6 [label="6"]
|
|
}
|
|
subgraph cluster_1 {
|
|
color=grey
|
|
label=""
|
|
0 [label="0"]
|
|
}
|
|
subgraph cluster_2 {
|
|
color=green
|
|
label=""
|
|
9 [label="9"]
|
|
10 [label="10"]
|
|
}
|
|
subgraph cluster_3 {
|
|
color=green
|
|
label=""
|
|
8 [label="8"]
|
|
}
|
|
subgraph cluster_4 {
|
|
color=green
|
|
label=""
|
|
7 [label="7"]
|
|
}
|
|
subgraph cluster_5 {
|
|
color=black
|
|
label=""
|
|
2 [label="2"]
|
|
}
|
|
subgraph cluster_6 {
|
|
color=red
|
|
label=""
|
|
4 [label="4"]
|
|
}
|
|
subgraph cluster_7 {
|
|
color=green
|
|
label=""
|
|
1 [label="1"]
|
|
3 [label="3"]
|
|
}
|
|
0 -> 0 [label="a & b\n{0,1,2}"]
|
|
0 -> 0 [label="!a & !b\n{2}"]
|
|
0 -> 5 [label="a\n{2}"]
|
|
1 -> 4 [label="b"]
|
|
1 -> 3 [label="a & !b"]
|
|
2 -> 0 [label="a"]
|
|
2 -> 7 [label="b"]
|
|
3 -> 1 [label="a & b\n{0,1}"]
|
|
4 -> 4 [label="!b\n{1,2}"]
|
|
4 -> 2 [label="b"]
|
|
5 -> 6 [label="1"]
|
|
6 -> 5 [label="1"]
|
|
7 -> 7 [label="!a & b\n{0,1}"]
|
|
7 -> 7 [label="a & b\n{0,2}"]
|
|
7 -> 8 [label="1"]
|
|
8 -> 8 [label="!a & b\n{0,2}"]
|
|
8 -> 8 [label="a & b\n{0,1}"]
|
|
8 -> 9 [label="1"]
|
|
9 -> 9 [label="!a & b\n{0,2}"]
|
|
9 -> 10 [label="a & b\n{0,1}"]
|
|
10 -> 9 [label="!a & b\n{0,1}"]
|
|
10 -> 10 [label="a & b\n{0,2}"]
|
|
}
|
|
EOF
|
|
|
|
diff out.dot expected
|
|
|
|
# While we are here, make sure scc_filter remove those grey SCCs.
|
|
autfilt --small -x simul=0 in.hoa -H > out.hoa
|
|
cat >expected.hoa <<EOF
|
|
HOA: v1
|
|
States: 8
|
|
Start: 0
|
|
AP: 2 "a" "b"
|
|
Acceptance: 3 Fin(2) & (Inf(0)&Inf(1))
|
|
properties: trans-labels explicit-labels trans-acc
|
|
--BODY--
|
|
State: 0
|
|
[0&!1] 2
|
|
[1] 3
|
|
State: 1
|
|
[1] 4
|
|
State: 2
|
|
[0&1] 0 {0 1}
|
|
State: 3
|
|
[1] 1
|
|
[!1] 3 {2}
|
|
State: 4
|
|
[!0&1] 4 {0 1}
|
|
[0&1] 4 {0 2}
|
|
[t] 5
|
|
State: 5
|
|
[0&1] 5 {0 1}
|
|
[!0&1] 5 {0 2}
|
|
[t] 6
|
|
State: 6
|
|
[!0&1] 6 {0 2}
|
|
[0&1] 7 {0 1}
|
|
State: 7
|
|
[!0&1] 6 {0 1}
|
|
[0&1] 7 {0 2}
|
|
--END--
|
|
EOF
|
|
diff expected.hoa out.hoa
|
|
|
|
|
|
cat >input <<'EOF'
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0&1
|
|
AP: 2 "a" "b"
|
|
acc-name: Buchi
|
|
Acceptance: 2 Inf(0) & Fin(1)
|
|
--BODY--
|
|
State: 0 {0 1}
|
|
[0&1] 0
|
|
[!0&1] 1
|
|
State: 1 {0 1}
|
|
[0&!1] 0
|
|
[!0&!1] 1
|
|
--END--
|
|
EOF
|
|
# This has one useless component
|
|
autfilt --dot=s input | grep grey
|