Commit 108ff8e3 authored by Salomon Sickert-Zehnter's avatar Salomon Sickert-Zehnter

Merge branch 'ltl2dra-regression' into 'master'

Fix a bug in ltl2{ldba,ldbga,dra,dgra,dpa}.

See merge request i7/owl!361
parents d2e4a797 8bf15515
......@@ -12,6 +12,7 @@ G (F (a & (G a)))
G (a | (!a U X a))
(a | X !b) W (F c)
F (a & GF (b W a))
F G (a <-> (b W a))
G (F (a & (a U b)))
G (F (a & X (F b)))
(G a) U (b U (G a))
......@@ -39,6 +40,7 @@ F ((a U b) & (G a | F c))
F G a | F (b & G (b | c))
G a | G (F b & F (a | c))
F ((G F a) | G (a | X a))
a <-> (F G(a <-> (b W a)))
(G a) | ((F b) W (b & X b))
G (G a | (F b & G (b | c)))
F (a & ((!a & !c) | G F c))
......@@ -59,6 +61,7 @@ G ((a W G b) -> (a <-> G (a U b)))
(G a & F (F b & G a)) | (F b & G a)
G ((a M (G b)) | ((c W d) & (a W c)))
(a & (b R X !a)) | ((G c) & (b U X a))
a <-> ((G b) U (G(a <-> (c | (b W a)))))
((G a) | ((F b) W (c & X b))) -> (b U c)
G F ((a | (G b)) & ((G c) R (a | (G c))))
(a | GFb) & (c | GFd) & (FGc | GFa) & GFc
......
......@@ -501,6 +501,9 @@
{
"formula": "(Ga \u0026 GFb)"
},
{
"formula": "(G!a \u0026 ((a \u0026 b) | (!a \u0026 !b)))"
},
{
"formula": "((Fa | Gb) \u0026 (Fb | Gc))"
},
......@@ -611,6 +614,17 @@
"deterministic": true
}
},
{
"formula": "(Fa | ((a | b) \u0026 (!a | !b)))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "(Fa | F(b \u0026 c))",
"properties": {
......@@ -1883,6 +1897,9 @@
{
"formula": "(FGa \u0026 G(a | XGa))"
},
{
"formula": "(FGa \u0026 GF(a \u0026 Xa))"
},
{
"formula": "(FG!a \u0026 (F(b \u0026 X!a) | F(!b \u0026 Xa)))"
},
......@@ -1931,6 +1948,9 @@
{
"formula": "((FGa | XFb | GF(a \u0026 c)) \u0026 (FGd | XXe | GF(d \u0026 f)))"
},
{
"formula": "(FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))"
},
{
"formula": "(G(a | XGb) \u0026 G(c | XG!b))"
},
......@@ -2023,6 +2043,9 @@
{
"formula": "(GFa | F(a \u0026 XFa))"
},
{
"formula": "(GFa | FG(a | Xa))"
},
{
"formula": "((((a \u0026 b)) U (c)) | F(d \u0026 (((a \u0026 b)) U (c))))",
"properties": {
......@@ -2092,6 +2115,9 @@
{
"formula": "(FG(a | Xb) | FG(c | Xd))"
},
{
"formula": "(GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))"
},
{
"formula": "(Fa | (FGb \u0026 FGc) | F(!d \u0026 ((d) R ((b \u0026 c)))))"
},
......@@ -2217,6 +2243,9 @@
{
"formula": "FG(a | XXb)"
},
{
"formula": "FG(Xa | ((a) W (Xa)))"
},
{
"formula": "FG(a | Xb | XXc)"
},
......@@ -2277,6 +2306,9 @@
{
"formula": "GF(a \u0026 XXb)"
},
{
"formula": "GF(Xa \u0026 ((a) M (Xa)))"
},
{
"formula": "GF(a \u0026 Xb \u0026 XXc)"
},
......@@ -2591,6 +2623,9 @@
{
"formula": "((FGa | GFb | GFc) \u0026 G(b | d | G(a | XFc)))"
},
{
"formula": "((!a | GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a)))) \u0026 (a | (FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))))"
},
{
"formula": "((FGa | GF(b \u0026 XXa)) \u0026 FG(c | X(b \u0026 Xa)))"
},
......@@ -2612,6 +2647,9 @@
{
"formula": "((FGa \u0026 FGb \u0026 GFc) | F(a \u0026 d \u0026 F(c \u0026 XGb)))"
},
{
"formula": "((a \u0026 FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a)))) | (!a \u0026 (GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))))"
},
{
"formula": "((GFa \u0026 FG(b | XXa)) | GF(c \u0026 X(b | Xa)))"
},
......@@ -2799,6 +2837,12 @@
{
"formula": "G(a | b | c | X!c | X(Xb | ((c) U (((!c) U (((c) U ((b | d)))))))))"
},
{
"formula": "((!a | GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a))))))) \u0026 (a | (FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a)))))))))"
},
{
"formula": "((a \u0026 FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a))))))) | (!a \u0026 (GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a)))))))))"
},
{
"formula": "F(a \u0026 (((b \u0026 ((c) R ((c | d | X((c) R (e))))))) R ((!c \u0026 F(b \u0026 (d | XGe))))))"
},
......
......@@ -501,6 +501,9 @@
{
"formula": "(Ga \u0026 GFb)"
},
{
"formula": "(G!a \u0026 ((a \u0026 b) | (!a \u0026 !b)))"
},
{
"formula": "((Fa | Gb) \u0026 (Fb | Gc))"
},
......@@ -611,6 +614,17 @@
"deterministic": true
}
},
{
"formula": "(Fa | ((a | b) \u0026 (!a | !b)))",
"properties": {
"size": 4,
"initialStatesSize": 2,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "(Fa | F(b \u0026 c))",
"properties": {
......@@ -1883,6 +1897,9 @@
{
"formula": "(FGa \u0026 G(a | XGa))"
},
{
"formula": "(FGa \u0026 GF(a \u0026 Xa))"
},
{
"formula": "(FG!a \u0026 (F(b \u0026 X!a) | F(!b \u0026 Xa)))"
},
......@@ -1931,6 +1948,9 @@
{
"formula": "((FGa | XFb | GF(a \u0026 c)) \u0026 (FGd | XXe | GF(d \u0026 f)))"
},
{
"formula": "(FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))"
},
{
"formula": "(G(a | XGb) \u0026 G(c | XG!b))"
},
......@@ -2023,6 +2043,9 @@
{
"formula": "(GFa | F(a \u0026 XFa))"
},
{
"formula": "(GFa | FG(a | Xa))"
},
{
"formula": "((((a \u0026 b)) U (c)) | F(d \u0026 (((a \u0026 b)) U (c))))",
"properties": {
......@@ -2092,6 +2115,9 @@
{
"formula": "(FG(a | Xb) | FG(c | Xd))"
},
{
"formula": "(GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))"
},
{
"formula": "(Fa | (FGb \u0026 FGc) | F(!d \u0026 ((d) R ((b \u0026 c)))))"
},
......@@ -2217,6 +2243,9 @@
{
"formula": "FG(a | XXb)"
},
{
"formula": "FG(Xa | ((a) W (Xa)))"
},
{
"formula": "FG(a | Xb | XXc)"
},
......@@ -2277,6 +2306,9 @@
{
"formula": "GF(a \u0026 XXb)"
},
{
"formula": "GF(Xa \u0026 ((a) M (Xa)))"
},
{
"formula": "GF(a \u0026 Xb \u0026 XXc)"
},
......@@ -2591,6 +2623,9 @@
{
"formula": "((FGa | GFb | GFc) \u0026 G(b | d | G(a | XFc)))"
},
{
"formula": "((!a | GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a)))) \u0026 (a | (FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))))"
},
{
"formula": "((FGa | GF(b \u0026 XXa)) \u0026 FG(c | X(b \u0026 Xa)))"
},
......@@ -2612,6 +2647,9 @@
{
"formula": "((FGa \u0026 FGb \u0026 GFc) | F(a \u0026 d \u0026 F(c \u0026 XGb)))"
},
{
"formula": "((a \u0026 FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a)))) | (!a \u0026 (GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))))"
},
{
"formula": "((GFa \u0026 FG(b | XXa)) | GF(c \u0026 X(b | Xa)))"
},
......@@ -2799,6 +2837,12 @@
{
"formula": "G(a | b | c | X!c | X(Xb | ((c) U (((!c) U (((c) U ((b | d)))))))))"
},
{
"formula": "((!a | GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a))))))) \u0026 (a | (FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a)))))))))"
},
{
"formula": "((a \u0026 FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a))))))) | (!a \u0026 (GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a)))))))))"
},
{
"formula": "F(a \u0026 (((b \u0026 ((c) R ((c | d | X((c) R (e))))))) R ((!c \u0026 F(b \u0026 (d | XGe))))))"
},
......
......@@ -325,6 +325,9 @@
{
"formula": "(Ga \u0026 GFb)"
},
{
"formula": "(G!a \u0026 ((a \u0026 b) | (!a \u0026 !b)))"
},
{
"formula": "((Fa | Gb) \u0026 (Fb | Gc))",
"properties": {
......@@ -499,6 +502,9 @@
{
"formula": "(!a | XFa)"
},
{
"formula": "(Fa | ((a | b) \u0026 (!a | !b)))"
},
{
"formula": "(Fa | F(b \u0026 c))"
},
......@@ -2131,6 +2137,9 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 GF(a \u0026 Xa))"
},
{
"formula": "(FG!a \u0026 (F(b \u0026 X!a) | F(!b \u0026 Xa)))",
"properties": {
......@@ -2195,6 +2204,9 @@
{
"formula": "((FGa | XFb | GF(a \u0026 c)) \u0026 (FGd | XXe | GF(d \u0026 f)))"
},
{
"formula": "(FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))"
},
{
"formula": "(G(a | XGb) \u0026 G(c | XG!b))"
},
......@@ -2351,6 +2363,9 @@
{
"formula": "(GFa | F(a \u0026 XFa))"
},
{
"formula": "(GFa | FG(a | Xa))"
},
{
"formula": "((((a \u0026 b)) U (c)) | F(d \u0026 (((a \u0026 b)) U (c))))"
},
......@@ -2412,6 +2427,9 @@
{
"formula": "(FG(a | Xb) | FG(c | Xd))"
},
{
"formula": "(GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))"
},
{
"formula": "(Fa | (FGb \u0026 FGc) | F(!d \u0026 ((d) R ((b \u0026 c)))))",
"properties": {
......@@ -2641,6 +2659,17 @@
"deterministic": true
}
},
{
"formula": "FG(Xa | ((a) W (Xa)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "FG(a | Xb | XXc)",
"properties": {
......@@ -2709,6 +2738,9 @@
{
"formula": "GF(a \u0026 XXb)"
},
{
"formula": "GF(Xa \u0026 ((a) M (Xa)))"
},
{
"formula": "GF(a \u0026 Xb \u0026 XXc)"
},
......@@ -3127,6 +3159,9 @@
{
"formula": "((FGa | GFb | GFc) \u0026 G(b | d | G(a | XFc)))"
},
{
"formula": "((!a | GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a)))) \u0026 (a | (FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))))"
},
{
"formula": "((FGa | GF(b \u0026 XXa)) \u0026 FG(c | X(b \u0026 Xa)))"
},
......@@ -3172,6 +3207,9 @@
{
"formula": "((FGa \u0026 FGb \u0026 GFc) | F(a \u0026 d \u0026 F(c \u0026 XGb)))"
},
{
"formula": "((a \u0026 FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a)))) | (!a \u0026 (GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))))"
},
{
"formula": "((GFa \u0026 FG(b | XXa)) | GF(c \u0026 X(b | Xa)))"
},
......@@ -3487,6 +3525,12 @@
{
"formula": "G(a | b | c | X!c | X(Xb | ((c) U (((!c) U (((c) U ((b | d)))))))))"
},
{
"formula": "((!a | GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a))))))) \u0026 (a | (FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a)))))))))"
},
{
"formula": "((a \u0026 FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a))))))) | (!a \u0026 (GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a)))))))))"
},
{
"formula": "F(a \u0026 (((b \u0026 ((c) R ((c | d | X((c) R (e))))))) R ((!c \u0026 F(b \u0026 (d | XGe))))))"
},
......
......@@ -813,6 +813,17 @@
"deterministic": true
}
},
{
"formula": "(G!a \u0026 ((a \u0026 b) | (!a \u0026 !b)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "((Fa | Gb) \u0026 (Fb | Gc))",
"properties": {
......@@ -1187,6 +1198,17 @@
"deterministic": true
}
},
{
"formula": "(Fa | ((a | b) \u0026 (!a | !b)))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
},
{
"formula": "(Fa | F(b \u0026 c))",
"properties": {
......@@ -4531,6 +4553,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 GF(a \u0026 Xa))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 6,
"complete": true,
"deterministic": true
}
},
{
"formula": "(FG!a \u0026 (F(b \u0026 X!a) | F(!b \u0026 Xa)))",
"properties": {
......@@ -4707,6 +4740,17 @@
"deterministic": true
}
},
{
"formula": "(FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 6,
"complete": true,
"deterministic": true
}
},
{
"formula": "(G(a | XGb) \u0026 G(c | XG!b))",
"properties": {
......@@ -5015,6 +5059,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | FG(a | Xa))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 10,
"complete": true,
"deterministic": true
}
},
{
"formula": "((((a \u0026 b)) U (c)) | F(d \u0026 (((a \u0026 b)) U (c))))",
"properties": {
......@@ -5180,6 +5235,17 @@
"deterministic": true
}
},
{
"formula": "(GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 18,
"complete": true,
"deterministic": true
}
},
{
"formula": "(Fa | (FGb \u0026 FGc) | F(!d \u0026 ((d) R ((b \u0026 c)))))",
"properties": {
......@@ -5521,6 +5587,17 @@
"deterministic": true
}
},
{
"formula": "FG(Xa | ((a) W (Xa)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
},
{
"formula": "FG(a | Xb | XXc)",
"properties": {
......@@ -5741,6 +5818,17 @@
"deterministic": true
}
},
{
"formula": "GF(Xa \u0026 ((a) M (Xa)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 6,
"complete": true,
"deterministic": true
}
},
{
"formula": "GF(a \u0026 Xb \u0026 XXc)",
"properties": {
......@@ -6687,6 +6775,17 @@
"deterministic": true
}
},
{
"formula": "((!a | GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a)))) \u0026 (a | (FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 30,
"complete": true,
"deterministic": true
}
},
{
"formula": "((FGa | GF(b \u0026 XXa)) \u0026 FG(c | X(b \u0026 Xa)))",
"properties": {
......@@ -6764,6 +6863,17 @@
"deterministic": true
}
},
{
"formula": "((a \u0026 FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a)))) | (!a \u0026 (GF(a \u0026 ((!b) M (!a))) | GF(!a \u0026 ((b) W (a))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 26,
"complete": true,
"deterministic": true
}
},
{
"formula": "((GFa \u0026 FG(b | XXa)) | GF(c \u0026 X(b | Xa)))",
"properties": {
......@@ -7391,6 +7501,28 @@
"deterministic": true
}
},
{
"formula": "((!a | GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a))))))) \u0026 (a | (FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a)))))))))",
"properties": {
"size": 14,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 57,
"complete": false,
"deterministic": true
}
},
{
"formula": "((a \u0026 FG(!a | b | ((c) W (a))) \u0026 FG(a | (!b \u0026 ((!c) M (!a)))) \u0026 (Gc | (G(!a | b | ((c) W (a))) \u0026 G(a | (!b \u0026 ((!c) M (!a))))))) | (!a \u0026 (GF(a \u0026 !b \u0026 ((!c) M (!a))) | GF(!a \u0026 (b | ((c) W (a)))) | (F!c \u0026 (F(a \u0026 !b \u0026 ((!c) M (!a))) | F(!a \u0026 (b | ((c) W (a)))))))))",
"properties": {
"size": 14,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 38,
"complete": false,
"deterministic": true
}
},
{
"formula": "F(a \u0026 (((b \u0026 ((c) R ((c | d | X((c) R (e))))))) R ((!c \u0026 F(b \u0026 (d | XGe))))))",
"properties": {
......
......@@ -813,6 +813,17 @@
"deterministic": true
}
},
{
"formula": "(G!a \u0026 ((a \u0026 b) | (!a \u0026 !b)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": true
}
},
{
"formula": "((Fa | Gb) \u0026 (Fb | Gc))",
"properties": {
......@@ -1187,6 +1198,17 @@
"deterministic": true
}
},
{
"formula": "(Fa | ((a | b) \u0026 (!a | !b)))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "(Fa | F(b \u0026 c))",
"properties": {
......@@ -4531,6 +4553,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 GF(a \u0026 Xa))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "(FG!a \u0026 (F(b \u0026 X!a) | F(!b \u0026 Xa)))",
"properties": {
......@@ -4707,6 +4740,17 @@
"deterministic": true
}
},
{
"formula": "(FG(a | ((!b) M (!a))) \u0026 FG(!a | ((b) W (a))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
},
{
"formula": "(G(a | XGb) \u0026 G(c | XG!b))",
"properties": {
......@@ -5015,6 +5059,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | FG(a | Xa))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
},
{