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

remfin: cleanup acceptance

Browse source 
* src/tgbaalgos/remfin.cc: Call cleanup_acceptance().
* src/tgbatest/remfin.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-24 21:51:20 +01:00
parent d597050f6d
commit 83dfb4a971
2 changed files with 41 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tgbaalgos/remfin.cc
View file

@ -20,6 +20,7 @@
#include "remfin.hh"
#include "sccinfo.hh"
#include <iostream>
#include "cleanacc.hh"
//#define TRACE
#ifdef TRACE
@ -303,6 +304,7 @@ namespace spot
}
cleanup_acceptance(res);
return res;
}
}

92
src/tgbatest/remfin.test
View file

@ -30,7 +30,7 @@ cat >test1 <<EOF
** This was a TGBA for GFa & GFb, but
** the acceptance has been changed to Fin(0)|Fin(1)
** so this is now the complement automaton.
**/
*/
HOA: v1
States: 1
Start: 0
@ -46,18 +46,18 @@ State: 0
/*
** This one has a mix of Inf and Fin acceptance, but no interference
** between the Fin sets
**/
*/
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 5 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(4)
--BODY--
State: 0
State: 0 {3 4}
[t] 0
[0] 1 {1}
[!0] 2 {0}
State: 1
State: 1 {3}
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2}
@ -67,9 +67,9 @@ State: 2
[!0&!1] 2 {0}
--END--
/*
** This one is similar, but Inf(0) is ised in two terms, so
** we to introduce extra sets in the output.
**/
** This one is similar, but Inf(0) is used in two terms, so
** we need to introduce extra sets in the output.
*/
HOA: v1
States: 3
Start: 0
@ -77,11 +77,11 @@ AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(0)
--BODY--
State: 0
State: 0 {3}
[t] 0
[0] 1 {1}
[!0] 2 {0}
State: 1
State: 1 {3}
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2}
@ -132,7 +132,8 @@ HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 3 Inf(2)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
@ -144,10 +145,10 @@ State: 0
[!0&1] 1
[!0&!1] 2
[0&!1] 2
State: 1 {2}
State: 1 {0}
[!0&!1] 1
[!0&1] 1
State: 2 {2}
State: 2 {0}
[!0&!1] 2
[0&!1] 2
--END--
@ -155,20 +156,17 @@ HOA: v1
States: 6
Start: 0
AP: 2 "a" "b"
Acceptance: 5 Inf(0) | Inf(4) | (Inf(2)&Inf(3))
Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0
[0] 1
[!0] 2
[t] 3
[t] 0 {2 3}
[0] 1 {2 3}
[!0] 2 {2 3}
State: 1
[1] 0
[0&1] 1
[!0&1] 2 {2}
[1] 3
[0&1] 4
[1] 0 {2}
[0&1] 1 {2}
[!0&1] 2 {1 2}
State: 2
[!1] 0
[0&!1] 1
@ -177,12 +175,7 @@ State: 2
[0&!1] 4
[!0&!1] 5
State: 3
[t] 3
[!0] 5 {0}
State: 4
[1] 3
[0&1] 4 {0}
[!0&1] 5
State: 5
[!1] 3
[0&!1] 4 {0}
@ -192,38 +185,30 @@ HOA: v1
States: 6
Start: 0
AP: 2 "a" "b"
Acceptance: 6 (Inf(0)&Inf(5)) | ((Inf(0) | (Inf(2)&Inf(3))) & Inf(4))
Acceptance: 5 (Inf(0)&Inf(4)) | ((Inf(0) | (Inf(1)&Inf(2))) & Inf(3))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {4}
[0] 1 {4}
[!0] 2 {0 4}
[t] 3 {4}
[t] 0 {2 3}
[0] 1 {2 3}
[!0] 2 {0 2 3}
State: 1
[1] 0 {4}
[0&1] 1 {0 4}
[!0&1] 2 {2 4}
[1] 3 {4}
[0&1] 4 {0 4}
[1] 0 {2 3}
[0&1] 1 {0 2 3}
[!0&1] 2 {1 2 3}
State: 2
[!1] 0 {4}
[0&!1] 1 {0 4}
[!0&!1] 2 {0 4}
[!1] 0 {3}
[0&!1] 1 {0 3}
[!0&!1] 2 {0 3}
[!1] 3 {3}
[0&!1] 4 {0 3}
[!0&!1] 5 {0 3}
State: 3
State: 4
State: 5
[!1] 3 {4}
[0&!1] 4 {0 4}
[!0&!1] 5 {0 4}
State: 3
[t] 3 {5}
[!0] 5 {0 5}
State: 4
[1] 3 {5}
[0&1] 4 {0 5}
[!0&1] 5 {5}
State: 5
[!1] 3 {5}
[0&!1] 4 {0 5}
[!0&!1] 5 {0 5}
--END--
HOA: v1
States: 1
@ -249,13 +234,14 @@ HOA: v1
States: 2
Start: 0
AP: 1 "p0"
Acceptance: 2 Inf(1)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete deterministic
--BODY--
State: 0
[!0] 0
[0] 1
State: 1 {1}
State: 1 {0}
[!0] 1
[0] 1
--END--