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

sccsimpl: Remove Fin sets between SCCs

Browse source 
We do not remove them in rejecting SCCs (as it might make the SCC
accepting), but we can remove them between SCCs.

Fixes #101.

* src/twaalgos/sccfilter.cc: Here.
* src/tests/sccsimpl.test: Add test case.
* NEWS: Mention this.
This commit is contained in:
Alexandre Duret-Lutz 2015-08-14 11:31:25 +02:00
parent 2eab0344b9
commit 0143f0d435
3 changed files with 46 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -6,6 +6,10 @@ New in spot 1.99.2a (not yet released)
* The html documentation now includes a HTML copies of the man * The html documentation now includes a HTML copies of the man
pages, and HTML copies of the Python notebooks. pages, and HTML copies of the Python notebooks.
* scc_filter(aut, true) does not remove Fin marks from rejecting
SCCs, but it now does remove Fin marks from transitions between
SCCs.
* Bugs fixed * Bugs fixed
- Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3) - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
were not detected as generalized-Rabin. were not detected as generalized-Rabin.

72
src/tests/sccsimpl.test
View file

@ -255,7 +255,7 @@ State: 0
[t] 0 [t] 0
State: 1 State: 1
[!0] 1 {0} [!0] 1 {0}
[0] 0 [0] 0 {0}
--END-- --END--
HOA: v1 HOA: v1
States: 2 States: 2
@ -271,41 +271,41 @@ State: 1
--END-- --END--
EOF EOF
# run 0 ../../bin/autfilt -C -H --any --high input >output run 0 ../../bin/autfilt -H --any --medium -x scc-filter=2 input >output
# cat >expected <<EOF cat >expected <<EOF
# HOA: v1 HOA: v1
# States: 2 States: 2
# Start: 1 Start: 1
# AP: 1 "p0" AP: 1 "p0"
# acc-name: Buchi acc-name: co-Buchi
# Acceptance: 1 Inf(0) Acceptance: 1 Fin(0)
# properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels trans-acc complete
# properties: deterministic inherently-weak properties: deterministic
# --BODY-- --BODY--
# State: 0 {0} State: 0
# [t] 0 [t] 0
# State: 1 State: 1
# [0] 0 [0] 0
# [!0] 1 [!0] 1 {0}
# --END-- --END--
# HOA: v1 HOA: v1
# States: 2 States: 2
# Start: 1 Start: 1
# AP: 1 "p0" AP: 1 "p0"
# acc-name: Buchi acc-name: Rabin 1
# Acceptance: 1 Inf(0) Acceptance: 2 Fin(0) & Inf(1)
# properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels trans-acc complete
# properties: deterministic inherently-weak properties: deterministic
# --BODY-- --BODY--
# State: 0 {0} State: 0
# [t] 0 [t] 0 {1}
# State: 1 State: 1
# [0] 0 [0] 0
# [!0] 1 [!0] 1 {0}
# --END-- --END--
# EOF EOF
# cat output cat output
# diff output expected diff output expected
run 0 ../../bin/autfilt -C -H --det --high input >output run 0 ../../bin/autfilt -C -H --det --high input >output
cat >expected <<EOF cat >expected <<EOF

10
src/twaalgos/sccfilter.cc
View file

@ -155,10 +155,12 @@ namespace spot
if (keep) if (keep)
{ {
unsigned u = this->si->scc_of(dst); unsigned u = this->si->scc_of(dst);
// If the edge is between two SCCs, or in a // If the edge is between two SCCs, we can simplify
// non-accepting SCC. Remove the acceptance sets. // remove the acceptance sets. If the SCC is non-accepting,
if ((this->si->is_rejecting_scc(u)) // we can only remove the Inf sets.
|| (RemoveAll && u != this->si->scc_of(src))) if (RemoveAll && u != this->si->scc_of(src))
acc = 0U;
else if (this->si->is_rejecting_scc(u))
acc &= accmask; acc &= accmask;
} }