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

to_dca/to_nca: fix handling of co-Büchi input

Browse source 
* spot/twaalgos/cobuchi.cc (to_dca, to_nca): Do not process
the input if it is already co-Büchi.
* tests/core/dca.test: Test this.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2018-03-28 10:26:10 +02:00
parent fc205c1883
commit 7957a231a1
3 changed files with 36 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

22
tests/core/dca.test
View file

@ -369,3 +369,25 @@ State: 1 [!1] 1 {0 2} [!0&!1] 2 [1] 3 [!0&1] 4 State: 2 [!0&!1] 2 {0 3}
[1] 7 {2} [!1] 8 {2} State: 9 [1] 3 {2} [!0] 4 [!1] 9 {2} State: 10 [1]
7 [!1] 10 {0 2} --END--
EOF
cat >in.hoa <<EOF
HOA: v1
name: "FGa"
States: 1
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0] 0
[!0] 0 {0}
--END--
EOF
# We had a problem that to_nca()/to_dca() would call sbacc()
# even if the input was already of the good shape. Make sure
# this is not the case anymore.
test '1,co-Buchi' = "`autfilt --cobuchi --small --stats='%s,%[]g' in.hoa`"
test '1,co-Buchi' = "`autfilt --cobuchi --det --stats='%s,%[]g' in.hoa`"