...
 
Commits (3)
......@@ -34,6 +34,10 @@ API:
* OmegaAcceptanceCast enables casting and conversion of different types of
omega-acceptance.
* EquivalenceClass always maintains the representative. This is made
possible by major performance improvements in the EquivalenceClass
implementation.
Bugfixes:
......
......@@ -16,6 +16,7 @@ G (F (a & X (F b)))
(G a) U (b U (G a))
(G a) U (b & G F b)
F (a & (!a | G F b))
(F a) xor X (b W F a)
G (G a | (F b & G b))
G (a | (a U (a U b)))
G (a | (F (b & X c)))
......
......@@ -1931,6 +1931,9 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -2064,6 +2067,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1931,6 +1931,9 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -2064,6 +2067,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -2187,6 +2187,17 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -2384,6 +2395,17 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4047,6 +4047,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -4432,6 +4443,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4047,6 +4047,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -4432,6 +4443,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4047,6 +4047,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -4432,6 +4443,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4047,6 +4047,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -4432,6 +4443,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -1387,6 +1387,9 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -1512,6 +1515,9 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1387,6 +1387,9 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -1512,6 +1515,9 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1323,6 +1323,9 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -1440,6 +1443,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1395,6 +1395,9 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -1536,6 +1539,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1395,6 +1395,9 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -1536,6 +1539,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1395,6 +1395,9 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -1536,6 +1539,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1395,6 +1395,9 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -1536,6 +1539,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 9,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 9,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 9,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 9,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4707,6 +4707,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -4234,6 +4234,17 @@
"deterministic": true
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 5,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -4630,6 +4641,17 @@
"deterministic": true
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 5,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -3610,7 +3610,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......@@ -4234,6 +4234,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -4630,6 +4641,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......@@ -7721,4 +7743,4 @@
"deterministic": true
}
}
]
\ No newline at end of file
]
......@@ -3951,7 +3951,7 @@
{
"formula": "G(a | ((!a) U (Xa)))",
"properties": {
"size": 7,
"size": 8,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
......@@ -4707,6 +4707,17 @@
"deterministic": false
}
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 7,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))",
"properties": {
......@@ -5136,6 +5147,17 @@
"deterministic": false
}
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 5,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))",
"properties": {
......@@ -7721,4 +7743,4 @@
"deterministic": true
}
}
]
\ No newline at end of file
]
......@@ -1939,6 +1939,9 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -2088,6 +2091,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -1939,6 +1939,9 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))"
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -2088,6 +2091,9 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))"
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -2195,6 +2195,17 @@
{
"formula": "(GF(!a \u0026 b) \u0026 GF(a \u0026 Xb))"
},
{
"formula": "((Fa | X(F!b \u0026 G!a)) \u0026 (G!a | X(Fa | Gb)))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a) R (b)) | (FGa \u0026 GFb) | (FGc \u0026 GFd)) \u0026 (((a) R (c)) | (FGa \u0026 GFd) | (FGc \u0026 GFb)))"
},
......@@ -2384,6 +2395,17 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))"
},
{
"formula": "((Fa \u0026 X(F!b \u0026 G!a)) | (G!a \u0026 X(Fa | Gb)))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((a) U (b)) \u0026 (FGb | GFa) \u0026 (FGc | GFd)) | (((a) U (d)) \u0026 (FGb | GFd) \u0026 (FGc | GFa)))"
},
......
......@@ -6,6 +6,7 @@ namespace owl {
ManagedJObject(env, "owl/cinterface/DeterministicAutomaton", handle),
acceptanceID(get_methodID(env, clazz, "acceptance", "()I")),
acceptanceSetCountID(get_methodID(env, clazz, "acceptanceSetCount", "()I")),
decomposeID(get_methodID(env, clazz, "decompose", "(I)[I")),
edgesID(get_methodID(env, clazz, "edges", "(I)[I")),
qualityScoreID(get_methodID(env, clazz, "qualityScore", "(II)D")) {}
......@@ -13,6 +14,7 @@ namespace owl {
ManagedJObject(std::move(automaton)),
acceptanceID(automaton.acceptanceID),
acceptanceSetCountID(automaton.acceptanceSetCountID),
decomposeID(automaton.decomposeID),
edgesID(automaton.edgesID),
qualityScoreID(automaton.qualityScoreID) {}
......@@ -24,6 +26,18 @@ namespace owl {
return call_int_method<>(env, handle, acceptanceSetCountID);
}
std::vector<int32_t> Automaton::decompose(int state) const {
auto result = call_method<jintArray>(env, handle, decomposeID, state);
// Provide an array to copy into...
jsize length = env->GetArrayLength(result);
std::vector<int32_t> decomposed_state = std::vector<int32_t>(static_cast<unsigned long>(length));
env->GetIntArrayRegion(result, 0, length, &decomposed_state[0]);
deref(env, result);
return decomposed_state;
}
EdgeTree Automaton::edges(int state) const {
auto result = call_method<jintArray>(env, handle, edgesID, state);
......@@ -65,4 +79,16 @@ namespace owl {
deref(env, jintArrayStates);
return (RealizabilityStatus)status;
}
void Automaton::describeDecompose() const {
jclass clazz = get_class(env, handle);
jmethodID toString = get_methodID(env, clazz, "describeDecompose", "()Ljava/lang/String;");
auto string = call_method<jstring>(env, handle, toString);
// Get a C-style string
const char* str = env->GetStringUTFChars(string, JNI_FALSE);
std::cout << str << std::endl;
env->ReleaseStringUTFChars(string, str);
deref(env, clazz, string);
}
}
......@@ -125,10 +125,10 @@ namespace owl {
}
Formula FormulaFactory::parseFinite(const std::string &formula_string, const std::vector<std::string>& apMapping) {
jstring string = copy_to_java(env, formula_string);
jobject mapping = copy_to_java(env, apMapping);
Formula formula = copy_from_java(env, call_static_method<jobject, jstring, jobject>(env, ltlfParser, ltlfParseID, string, mapping));
deref(env, string, mapping);
return formula;
}
}
\ No newline at end of file
jstring string = copy_to_java(env, formula_string);
jobject mapping = copy_to_java(env, apMapping);
Formula formula = copy_from_java(env, call_static_method<jobject, jstring, jobject>(env, ltlfParser, ltlfParseID, string, mapping));
deref(env, string, mapping);
return formula;
}
}
......@@ -140,6 +140,7 @@ namespace owl {
private:
jmethodID acceptanceID;
jmethodID acceptanceSetCountID;
jmethodID decomposeID;
jmethodID edgesID;
jmethodID qualityScoreID;
......@@ -153,6 +154,8 @@ namespace owl {
Acceptance acceptance() const;
int acceptance_set_count() const;
std::vector<int32_t> decompose(int state) const;
void describeDecompose() const;
EdgeTree edges(int state) const;
double quality_score(int successor, int colour) const;
};
......
......@@ -60,6 +60,11 @@ public interface EdgeTreeAutomatonMixin<S, A extends OmegaAcceptance> extends Au
return edgeTree(state).get(valuation);
}
@Override
default Set<S> successors(S state) {
return edgeTree(state).values(Edge::successor);