Add a cleanup_acceptance() algorithm

* src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh: New file.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgba/acc.hh, src/tgba/tgba.hh (get_acceptance): Return a
reference.
* src/bin/autfilt.cc: Add a --cleanup-acceptance option.
* src/tgbatest/hoaparse.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-24 20:02:44 +01:00
parent 85508a0ea6
commit 659107a000
7 changed files with 226 additions and 47 deletions

View file

@ -1394,48 +1394,48 @@ State: 0
EOF
# FIXME: Test removal of useless acceptance sets
#
# # The mapping of acceptance sets for the second automaton is
# # input -> output
# # 0 -> 0
# # 1 -> removed
# # 2 -> 1
# # 3 -> removed
# # 4 -> 2
# # !2 -> 3
# expectok input <<EOF
# HOA: v1
# name: "TGBA for Fa"
# States: 2
# Start: 0
# AP: 1 "a"
# acc-name: all
# Acceptance: 0 t
# properties: trans-labels explicit-labels state-acc complete deterministic
# --BODY--
# State: 0 "F(a)"
# [0] 1
# [!0] 0
# State: 1 "t"
# [t] 1
# --END--
# HOA: v1
# States: 1
# Start: 0
# AP: 3 "a" "b" "c"
# acc-name: generalized-Buchi 4
# Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
# properties: trans-labels explicit-labels trans-acc complete deterministic
# --BODY--
# State: 0
# [0&1&2] 0 {0 1 2}
# [!0&1&2] 0 {1 2}
# [0&!1&2] 0 {0 1}
# [!0&!1&2] 0 {1}
# [0&1&!2] 0 {0 2 3}
# [!0&1&!2] 0 {2 3}
# [0&!1&!2] 0 {0 3}
# [!0&!1&!2] 0 {3}
# --END--
# EOF
# Test removal of useless acceptance sets
# The mapping of acceptance sets for the second automaton is
# input -> output
# 0 -> 0
# 1 -> removed
# 2 -> 1
# 3 -> removed
# 4 -> 2
# !2 -> 3
expectok input --cleanup-acc <<EOF
HOA: v1
name: "TGBA for Fa"
States: 2
Start: 0
AP: 1 "a"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete deterministic
--BODY--
State: 0 "F(a)"
[0] 1
[!0] 0
State: 1 "t"
[t] 1
--END--
HOA: v1
States: 1
Start: 0
AP: 3 "a" "b" "c"
acc-name: generalized-Buchi 4
Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
[0&1&2] 0 {0 1 2}
[!0&1&2] 0 {1 2}
[0&!1&2] 0 {0 1}
[!0&!1&2] 0 {1}
[0&1&!2] 0 {0 2 3}
[!0&1&!2] 0 {2 3}
[0&!1&!2] 0 {0 3}
[!0&!1&!2] 0 {3}
--END--
EOF