Commit 01321303 authored by Salomon Sickert-Zehnter's avatar Salomon Sickert-Zehnter

Merge branch 'portfolio-extensions' into 'master'

Portfolio Translation

See merge request i7/owl!332
parents c44d952f fdd782c6
......@@ -15,12 +15,25 @@ Modules:
(on the test sets) smaller automata compared to `fgx2dpa`.
* `ltl2da` uses for the "safety-cosafety" and "cosafety-safety" fragment a
optimised construction without invoking a fallback solution.
optimised construction without invoking a fallback solution.
* `ltl2nba`, `ltl2ngba`, `ltl2ldba`, `ltl2ldgba`, `ltl2dra`, `ltl2dgra`,
and `ltl2dpa` use a portfolio translator selecting simpler translations
based on syntactic criteria, before applying the general purpose
translation. This feature can be deactivated using `--disable-portfolio`.
* `ltl2dpa` by default uses also a complement translation to obtain a small
DPA. This feature can be deactivated using `--disable-complement`.
API:
* Removed unused and unmaintained `FrequencyG` class and forbid subclassing
of `GOperator`.
* Addition of `Negation` as a syntactic element for LTL formulas.
* OmegaAcceptanceCast enables casting and conversion of different types of
omega-acceptance.
Bugfixes:
......
......@@ -13,7 +13,8 @@ G (F (a & (G a)))
F (a & GF (b W a))
G (F (a & (a U b)))
G (F (a & X (F b)))
(G b) U (a & G F a)
(G a) U (b U (G a))
(G a) U (b & G F b)
F (a & (!a | G F b))
G (G a | (F b & G b))
G (a | (a U (a U b)))
......
......@@ -1170,6 +1170,9 @@
{
"formula": "(((a) R (b)) \u0026 F(c \u0026 Xa))"
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))"
},
{
"formula": "(GFa \u0026 (F!a | FGb))"
},
......@@ -1335,6 +1338,9 @@
{
"formula": "(FG!a | (Ga \u0026 GFb))"
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))"
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))"
},
......
......@@ -1170,6 +1170,9 @@
{
"formula": "(((a) R (b)) \u0026 F(c \u0026 Xa))"
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))"
},
{
"formula": "(GFa \u0026 (F!a | FGb))"
},
......@@ -1335,6 +1338,9 @@
{
"formula": "(FG!a | (Ga \u0026 GFb))"
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))"
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))"
},
......
......@@ -984,7 +984,7 @@
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 1,
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -1006,7 +1006,7 @@
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 1,
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
......@@ -1028,7 +1028,7 @@
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 1,
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
......@@ -1050,7 +1050,7 @@
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 1,
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -1061,7 +1061,7 @@
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 1,
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -1072,7 +1072,7 @@
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 1,
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -1083,7 +1083,7 @@
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "EmersonLeiAcceptance",
"acceptanceSets": 1,
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......
......@@ -2562,6 +2562,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "(GFa \u0026 (F!a | FGb))",
"properties": {
......@@ -3167,6 +3178,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 10,
"complete": true,
"deterministic": true
}
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))",
"properties": {
......
......@@ -2562,6 +2562,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": true
}
},
{
"formula": "(GFa \u0026 (F!a | FGb))",
"properties": {
......@@ -3167,6 +3178,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))",
"properties": {
......
This diff is collapsed.
......@@ -2298,6 +2298,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(GFa \u0026 (F!a | FGb))",
"properties": {
......@@ -2837,6 +2848,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))",
"properties": {
......
This diff is collapsed.
......@@ -2298,6 +2298,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(GFa \u0026 (F!a | FGb))",
"properties": {
......@@ -2837,6 +2848,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))",
"properties": {
......@@ -6250,7 +6272,7 @@
{
"formula": "((GFa \u0026 FG(b | XXc)) | (FGc \u0026 GF(d \u0026 X(b | Xa))))",
"properties": {
"size": 24,
"size": 12,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 5,
......
This diff is collapsed.
......@@ -2562,6 +2562,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "(GFa \u0026 (F!a | FGb))",
"properties": {
......@@ -3167,6 +3178,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 10,
"complete": true,
"deterministic": true
}
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))",
"properties": {
......
......@@ -2562,6 +2562,17 @@
"deterministic": true
}
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(GFa \u0026 (F!a | FGb))",
"properties": {
......@@ -3167,6 +3178,17 @@
"deterministic": true
}
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))",
"properties": {
......
This diff is collapsed.
......@@ -394,10 +394,10 @@
{
"formula": "(FGa | FG!a)",
"properties": {
"size": 2,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -405,10 +405,10 @@
{
"formula": "(FGa | FGb)",
"properties": {
"size": 2,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -443,10 +443,10 @@
{
"formula": "(FGa | FGb | FGc)",
"properties": {
"size": 3,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
......@@ -475,10 +475,10 @@
{
"formula": "(FGa | FGb | FGc | FGd)",
"properties": {
"size": 4,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
......@@ -492,10 +492,10 @@
{
"formula": "(FGa | FGb | FGc | FGd | FGe)",
"properties": {
"size": 5,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 5,
"complete": true,
"deterministic": true
}
......@@ -515,10 +515,10 @@
{
"formula": "(FGa | FGb | FGc | FGd | FGe | FGf | FGg | FGh | FGi)",
"properties": {
"size": 9,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 9,
"complete": true,
"deterministic": true
}
......@@ -762,6 +762,9 @@
{
"formula": "(((a) R (b)) \u0026 F(c \u0026 Xa))"
},
{
"formula": "(FGa \u0026 (Ga | ((b) U (Ga))))"
},
{
"formula": "(GFa \u0026 (F!a | FGb))"
},
......@@ -927,6 +930,9 @@
{
"formula": "(FG!a | (Ga \u0026 GFb))"
},
{
"formula": "(GFa | (Fa \u0026 ((b) R (Fa))))"
},
{
"formula": "(((Xa) U (b)) | X((!a) R ((!a | !b))))"
},
......@@ -978,10 +984,10 @@
{
"formula": "(FGa | FGb | FG(c | d))",
"properties": {
"size": 3,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
......@@ -1007,10 +1013,10 @@
{
"formula": "(FG(a | b) | FG(c | d) | FG(e | f))",
"properties": {
"size": 3,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
......@@ -1498,10 +1504,10 @@
{
"formula": "(FG(a | b) | FG(!a | Xb))",
"properties": {
"size": 3,
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -1544,10 +1550,10 @@
{
"formula": "(FGa | FGb | FG(c | Xd))",
"properties": {
"size": 4,
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 3,
"complete": true,
"deterministic": true
}
......@@ -1859,10 +1865,10 @@
{
"formula": "(FG(a | b) | FG(!a | Xb) | FG(a | XXb))",
"properties": {
"size": 7,
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......@@ -2048,10 +2054,10 @@
{
"formula": "(FG(a | b) | FG(!a | Xb) | FG(a | XXb) | FG(!a | XXXb))",
"properties": {
"size": 15,
"size": 14,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"acceptanceName": "GeneralizedCoBuchiAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
......
......@@ -392,10 +392,26 @@
"formula": "(F(a \u0026 b) | FGc)"
},
{
"formula": "(FGa | FG!a)"
"formula": "(FGa | FG!a)",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "(FGa | FGb)"
"formula": "(FGa | FGb)",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "CoBuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "(FGa | GFb)"
......@@ -425,7 +441,15 @@
"formula": "(F(a \u0026 b) | FGb | FGc)"
},
{
<