...
 
Commits (2)
......@@ -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)))"
},
......
......@@ -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);
}
@Override
default List<PreferredEdgeAccess> preferredEdgeAccess() {
return ACCESS_MODES;
......
......@@ -101,11 +101,13 @@ final class HoaConsumerExtended<S> {
}
}
// TODO: global scope?
private static String tool() {
String title = HoaConsumerExtended.class.getPackage().getImplementationTitle();
return title == null ? "owl" : title;
}
// TODO: global scope?
private static String version() {
String version = HoaConsumerExtended.class.getPackage().getImplementationVersion();
return version == null ? "development" : version;
......
......@@ -24,6 +24,7 @@ import static owl.ltl.SyntacticFragment.SINGLE_STEP;
import com.google.common.primitives.ImmutableIntArray;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
......@@ -41,10 +42,9 @@ import owl.ltl.Conjunction;
import owl.ltl.Disjunction;
import owl.ltl.Formula;
import owl.ltl.GOperator;
import owl.ltl.PropositionalFormula;
import owl.ltl.Literal;
import owl.ltl.SyntacticFragment;
import owl.ltl.SyntacticFragments;
import owl.ltl.UnaryModalOperator;
import owl.ltl.XOperator;
import owl.ltl.rewriter.LiteralMapper;
import owl.ltl.rewriter.PullUpXVisitor;
......@@ -118,7 +118,7 @@ public final class DecomposedDPA {
private static boolean isSingleStep(Formula formula) {
if (formula instanceof Conjunction) {
return ((Conjunction) formula).children.stream().allMatch(DecomposedDPA::isSingleStep);
return formula.children().stream().allMatch(DecomposedDPA::isSingleStep);
}
return formula instanceof GOperator && SINGLE_STEP.contains(((GOperator) formula).operand);
......@@ -199,7 +199,8 @@ public final class DecomposedDPA {
return new LabelledTree.Leaf<>(newReference);
}
private List<LabelledTree<Tag, Reference>> createLeaves(PropositionalFormula formula) {
private List<LabelledTree<Tag, Reference>> createLeaves(
Formula.NaryPropositionalOperator formula) {
// Partition elements.
var safety = new Clusters();
var safetySingleStep = new HashMap<Integer, Clusters>();
......@@ -208,7 +209,7 @@ public final class DecomposedDPA {
var weakOrBuchiOrCoBuchi = new TreeSet<Formula>();
var parity = new TreeSet<Formula>();
for (Formula x : formula.children) {
for (Formula x : formula.children()) {
switch (annotatedTree.get(x)) {
case SAFETY:
PullUpXVisitor.XFormula rewrittenX = x.accept(PullUpXVisitor.INSTANCE);
......@@ -240,7 +241,7 @@ public final class DecomposedDPA {
// Process elements.
List<LabelledTree<Tag, Reference>> children = new ArrayList<>();
Function<Iterable<Formula>, Formula> merger = formula instanceof Conjunction
Function<Collection<Formula>, Formula> merger = formula instanceof Conjunction
? Conjunction::of
: Disjunction::of;
......@@ -278,8 +279,13 @@ public final class DecomposedDPA {
return createLeaf(formula);
}
@Override
public LabelledTree<Tag, Reference> visit(Literal literal) {
return createLeaf(literal);
}
private boolean keepTreeStructureBiconditional(Formula formula) {
if (formula instanceof PropositionalFormula) {
if (formula instanceof Conjunction || formula instanceof Disjunction) {
if (formula.children().stream()
.filter(x -> annotatedTree.get(x) == Acceptance.PARITY).count() > 1) {
return false;
......@@ -293,8 +299,12 @@ public final class DecomposedDPA {
protected Boolean visit(Formula.TemporalOperator formula) {
return (SyntacticFragments.isAlmostAll(formula)
|| SyntacticFragments.isInfinitelyOften(formula))
&& SyntacticFragment.SINGLE_STEP
.contains(((UnaryModalOperator) ((UnaryModalOperator) formula).operand).operand);
&& SyntacticFragment.SINGLE_STEP.contains(formula.children().get(0).children().get(0));