to_tgba: fix handling of CNF with multiple unit clauses

Fixes #313, reported by František Blahoudek.

* spot/twaalgos/totgba.cc (to_generalized_buchi): Fix it.
* tests/core/remfin.test: Test it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2017-12-22 17:53:30 +01:00
parent 19348c8938
commit 9ec7df670e
3 changed files with 99 additions and 2 deletions

View file

@ -268,6 +268,29 @@ HOA: v1 States: 3 Start: 0 AP: 2 "b" "c" Acceptance: 3 Fin(0) &
complete --BODY-- State: 0 [!0] 0 {1 2} [0] 0 {0 1 2} [0&!1] 1 [0&1] 2
State: 1 [!0 | !1] 1 {1 2} [0&1] 2 {1} State: 2 [!1] 1 {1 2} [1] 2 {1}
--END--
/*
** Issue #313. The TGBA conversion of this automaton was wrong.
*/
HOA: v1
States: 2
Start: 0
AP: 3 "a" "b" "c"
Acceptance: 4 (Fin(1)|Fin(2)) & Fin(0) & Inf(3)
properties: trans-labels explicit-labels trans-acc complete
--BODY--
State: 0
[t] 0 {0 3}
[1 | 2] 0 {1 3}
[0] 0 {2 3}
[!1&!2] 1 {1}
State: 1
[2] 0 {0 3}
[2] 0 {1 3}
[0&2] 0 {2 3}
[!2] 1 {0}
[!2] 1 {1}
[0&!2] 1 {2}
--END--
EOF
acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)'
@ -842,6 +865,37 @@ State: 3
[!1] 2 {0 1}
[1] 3 {0}
--END--
HOA: v1
States: 6
Start: 0
AP: 3 "a" "b" "c"
Acceptance: 4 (Inf(0)&Inf(2)&Inf(3)) | (Inf(0)&Inf(1)&Inf(3))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0
[!1&!2] 1
[0] 2
[1 | 2] 4
State: 1
[2] 0
[!2] 1
[0&2] 2
[0&!2] 3
[2] 4
[!2] 5
State: 2
[0] 2 {0 1 3}
State: 3
[0&2] 2 {0 1 3}
[0&!2] 3 {0 1}
State: 4
[1 | 2] 4 {0 2 3}
[!1&!2] 5 {0 2}
State: 5
[2] 4 {0 2 3}
[!2] 5 {0 2}
--END--
EOF
cat >expected-tgba <<EOF
@ -1408,6 +1462,38 @@ State: 3
[!1] 2 {0}
[1] 3
--END--
HOA: v1
States: 6
Start: 0
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0
[!1&!2] 1
[0] 2
[1 | 2] 4
State: 1
[2] 0
[!2] 1
[0&2] 2
[0&!2] 3
[2] 4
[!2] 5
State: 2
[0] 2 {0}
State: 3
[0&2] 2
[0&!2] 3
State: 4
[1 | 2] 4 {0}
[!1&!2] 5
State: 5
[2] 4 {0}
[!2] 5
--END--
EOF
run 0 autfilt -H --remove-fin test1 > output