Skip to content

owl
owl

11.08., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

Commit db21b56e authored by Salomon Sickert's avatar Salomon Sickert
Browse files
Options

Improve performance of BDD-based equivalence class and retain representative.

parent 01321303
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 2078 additions and 1800 deletions
CHANGELOG.md
View file @ db21b56e
......@@ -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:
......
data/formulas/regressions.ltl
View file @ db21b56e
......@@ -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)))
......
data/formulas/sizes/coSafety.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/coSafety.nondeterministic.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/coSafetySafety.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/dgra.symmetric.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dgra.symmetric.optimizations.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dgra.symmetric.portfolio.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dpa.asymmetric.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dpa.asymmetric.portfolio.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dpa.symmetric.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dpa.symmetric.portfolio.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dra.symmetric.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dra.symmetric.optimizations.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/dra.symmetric.portfolio.json
View file @ db21b56e
......@@ -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": {
......
data/formulas/sizes/fgSafety.generalized.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/fgSafety.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/fgSafety.nondeterministic.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/gfCoSafety.generalized.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/gfCoSafety.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/gfCoSafety.nondeterministic.generalized.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/gfCoSafety.nondeterministic.json
View file @ db21b56e
......@@ -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)))"
},
......
data/formulas/sizes/ldba.asymmetric.json
View file @ db21b56e
......@@ -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": {
......