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

...
 
Commits (9)
# 2019.06 (unreleased)
Translations:
Modules:
* Implemented all LICS'18 translations for LTL fragments. Including a symbolic
successor / edge computation. The translations can be found in the canonical
package and are exposed via `ltl2da` and `ltl2na`.
* Removed TLSF support. Ensuring the correct implementation of the TLSF
specification posed a too large maintenance burden. Users of the TLSF format
can use Syfco (https://github.com/reactive-systems/syfco) to translate it to
a basic LTL formula.
API:
* Overhaul of the symbolic successor computation
......@@ -36,6 +41,15 @@ API:
2. x R (!x | y) and y is pure universal -> G (!x | y)
3. x U (!x & y) and y is pure eventual -> F (!x & y)
4. x W (!x & y) and y is pure eventual -> G x | F (!x & y)
5. F a & a R b -> a M b
6. F a & b W a -> b U a
7. G a | a U b -> a W b
8. G a | b M a -> b R a
* Overhaul of the C++-API. Most notably there is an API for approximative realisability checks for a
state in the decomposed DPA.
* Add basic support for ultimately periodic words and add language membership tests.
Bugfixes:
......
......@@ -226,6 +226,18 @@ shadowJar {
minimize()
}
task sourcesJar(type: Jar, dependsOn: classes) {
classifier = 'sources'
from sourceSets.main.allSource
}
task javadocJar(type: Jar, dependsOn: javadoc) {
classifier = 'javadoc'
from javadoc.destinationDir
}
task mavenJars(dependsOn: [jar, sourcesJar, javadocJar])
// ---------------- Script Jobs ----------------
def allStartScripts = createStartScriptTasks("", jar.outputs.files + project.getConfigurations().getByName(JavaPlugin.RUNTIME_CLASSPATH_CONFIGURATION_NAME), scripts)
......
......@@ -8,7 +8,10 @@
<!-- Suppress everything for generated files -->
<suppress files="owl[\\/]grammar[\\/]" checks=".*"/>
<suppress files="FG.*|.+2.+" checks="AbbreviationAsWordInName"/>
<!-- Suppress broken file -->
<suppress files="owl[\\/]cinterface[\\/]DeterministicAutomaton" checks=".*"/>
<suppress files="FG.*|.+2.+|.*DPA.*" checks="AbbreviationAsWordInName"/>
<!-- Soon we will doc everything ... -->
<suppress checks="JavadocMethod" files=".*"/>
......
......@@ -5,7 +5,7 @@
"http://www.puppycrawl.com/dtds/suppressions_1_0.dtd">
<suppressions>
<suppress files="Size.*|LTL2.*|NBA2.*|LD.*" checks="AbbreviationAsWordInName"/>
<suppress files="Size.*|LTL2.*|NBA2.*|LD.*|.*DPA.*" checks="AbbreviationAsWordInName"/>
<!-- We avoid final modifier -->
<suppress checks="VariableDeclarationUsageDistanceCheck" files=".*" />
......
......@@ -168,9 +168,6 @@
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R (b)))"
},
{
"formula": "(Fa \u0026 ((b) R (!a)))"
},
......@@ -181,7 +178,15 @@
"formula": "(Ga \u0026 Xb)"
},
{
"formula": "(Fa \u0026 ((a) R (b)) \u0026 ((c) U (d)))"
"formula": "(((a) M (b)) \u0026 ((c) U (d)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": true
}
},
{
"formula": "(a | ((b) U (a)))",
......@@ -250,14 +255,11 @@
{
"formula": "(Ga | Xb)"
},
{
"formula": "(Ga | ((a) U (b)))"
},
{
"formula": "(G!a | ((b) U (a)))"
},
{
"formula": "(Ga | ((b) R (c)) | ((a) U (d)))"
"formula": "(((a) R (b)) | ((c) W (d)))"
},
{
"formula": "F(a \u0026 b)",
......@@ -1520,6 +1522,17 @@
{
"formula": "F(a \u0026 Gb \u0026 XGc)"
},
{
"formula": "F(!a \u0026 Xa \u0026 X((!a) M (b)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "F((a | Fb) \u0026 (c | Fd) \u0026 (e | Ff))",
"properties": {
......@@ -1623,6 +1636,9 @@
{
"formula": "G(a | Fb | XFc)"
},
{
"formula": "G(a | X!a | X((a) W (b)))"
},
{
"formula": "G(!a | b | ((b) R ((a | b))))"
},
......@@ -1657,19 +1673,38 @@
"formula": "XF(a \u0026 Gb)"
},
{
"formula": "XF(a \u0026 b \u0026 F!b \u0026 ((!b) R (c)))"
"formula": "XF(a \u0026 b \u0026 ((!b) M (c)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "XF(a \u0026 !b \u0026 Fb \u0026 ((b) R (c)))"
"formula": "XF(a \u0026 !b \u0026 ((b) M (c)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "XG(a | Fb)"
},
{
"formula": "XG(a | b | G!b | ((!b) U (c)))"
"formula": "XG(a | b | ((!b) W (c)))"
},
{
"formula": "XG(a | !b | ((b) W (c)))"
},
{
"formula": "XG(a | !b | Gb | ((b) U (c)))"
"formula": "((a) M ((a | b | X((a) R (c)))))"
},
{
"formula": "((a) R ((b | X((c) R (d)))))"
......@@ -1745,6 +1780,9 @@
"deterministic": true
}
},
{
"formula": "((a) W ((a \u0026 b \u0026 X((a) U (c)))))"
},
{
"formula": "(a \u0026 F(b \u0026 (a | Gb)))"
},
......@@ -1759,9 +1797,6 @@
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R ((a | b | X((a) R (c))))))"
},
{
"formula": "(Fa \u0026 (((b \u0026 ((a) R ((a | c))))) R (!a)))"
},
......@@ -1873,9 +1908,6 @@
{
"formula": "(Ga | XG(b | Xc))"
},
{
"formula": "(Ga | ((a) U ((a \u0026 b \u0026 X((a) U (c))))))"
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c))))) U (a)))"
},
......@@ -2096,9 +2128,6 @@
{
"formula": "F((a | Xb) \u0026 (b | XGc))"
},
{
"formula": "F(!a \u0026 Xa \u0026 X(F!a \u0026 ((!a) R (b))))"
},
{
"formula": "F((a | XXb) \u0026 (b | XXc) \u0026 (c | XGd))"
},
......@@ -2159,9 +2188,6 @@
{
"formula": "G((!a \u0026 Xa) | ((b | X!b) \u0026 (!b | Xb)))"
},
{
"formula": "G(a | X!a | X(Ga | ((a) U (b))))"
},
{
"formula": "G((a \u0026 XXb) | (b \u0026 XXc) | (c \u0026 XFd))"
},
......@@ -2423,6 +2449,9 @@
"deterministic": true
}
},
{
"formula": "((a) M ((a \u0026 ((b) M ((b | c | X((b) R (d))))))))"
},
{
"formula": "((((!a) M (((b | XGa) \u0026 (!b | XF!a))))) M (!a))"
},
......@@ -2441,10 +2470,10 @@
}
},
{
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))"
"formula": "((a) W ((a | ((b) W ((b \u0026 c \u0026 X((b) U (d))))))))"
},
{
"formula": "(Fa \u0026 ((a) R ((a \u0026 Fb \u0026 ((b) R ((b | c | X((b) R (d)))))))))"
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))"
},
{
"formula": "(Fa \u0026 (((b \u0026 ((a) R ((a | c | X((a) R (d))))))) R (!a)))"
......@@ -2470,9 +2499,6 @@
{
"formula": "(Ga \u0026 G!b \u0026 Gc \u0026 XGb \u0026 X(Xa \u0026 ((!b) R (((b) R (((!b) R ((a \u0026 d)))))))))"
},
{
"formula": "(Ga | ((a) U ((a | Gb | ((b) U ((b \u0026 c \u0026 X((b) U (d)))))))))"
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 X((!a) U (d))))))) U (a)))"
},
......@@ -2515,13 +2541,13 @@
"formula": "F(a \u0026 F(b \u0026 (c | d | X((d) R (e)))))"
},
{
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))"
"formula": "F(a \u0026 ((b) M ((c \u0026 (b | d | X((b) R (e)))))))"
},
{
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))"
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))"
},
{
"formula": "F(a \u0026 Fb \u0026 ((b) R ((c \u0026 (b | d | X((b) R (e)))))))"
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))"
},
{
"formula": "F(a \u0026 Fb \u0026 ((c) R ((!b \u0026 (c | d | X((c) R (e)))))))"
......@@ -2551,13 +2577,13 @@
"formula": "G(a | ((!b) U (((b) U (((!b) U (((b) U ((b \u0026 c))))))))))"
},
{
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))"
"formula": "G(a | ((b) W ((c | (b \u0026 d \u0026 X((b) U (e)))))))"
},
{
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))"
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))"
},
{
"formula": "G(a | Gb | ((b) U ((c | (b \u0026 d \u0026 X((b) U (e)))))))"
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))"
},
{
"formula": "G(a | Gb | ((!b) U ((c | (!b \u0026 d \u0026 X((!b) U (e)))))))"
......@@ -2577,6 +2603,20 @@
{
"formula": "G(a | G(b | XGc) | (((b | Fd | XG(c | d))) U ((d | e))))"
},
{
"formula": "((a) M ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd)))))"
},
{
"formula": "((a) M ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb)))))))))))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "((a) R ((!b | !c | ((Gb) M (((c | d) \u0026 (!d | ((!c) R ((a | !c))))))))))"
},
......@@ -2584,10 +2624,10 @@
"formula": "((a) U ((b \u0026 c \u0026 ((F!b) W (((!c \u0026 !d) | (d \u0026 ((c) U ((a \u0026 c))))))))))"
},
{
"formula": "(Fa \u0026 ((a) R ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd))))))"
"formula": "((!a) W ((a \u0026 (((b) U (c)) | G(b | XGd)))))"
},
{
"formula": "(Fa \u0026 ((a) R ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb))))))))))))"
"formula": "((!a) W ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b)))))))))))"
},
{
"formula": "(Fa \u0026 (((b \u0026 ((a) R ((a | c | d | X(((a | d)) R (e))))))) R (!a)))"
......@@ -2598,12 +2638,6 @@
{
"formula": "(FG(a | XXXXa) \u0026 FG(!a | XXXX!a))"
},
{
"formula": "(G!a | ((!a) U ((a \u0026 (((b) U (c)) | G(b | XGd))))))"
},
{
"formula": "(G!a | ((!a) U ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b))))))))))))"
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 d \u0026 X(((!a \u0026 d)) U (e))))))) U (a)))"
},
......
......@@ -168,9 +168,6 @@
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R (b)))"
},
{
"formula": "(Fa \u0026 ((b) R (!a)))"
},
......@@ -181,7 +178,15 @@
"formula": "(Ga \u0026 Xb)"
},
{
"formula": "(Fa \u0026 ((a) R (b)) \u0026 ((c) U (d)))"
"formula": "(((a) M (b)) \u0026 ((c) U (d)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": true
}
},
{
"formula": "(a | ((b) U (a)))",
......@@ -250,14 +255,11 @@
{
"formula": "(Ga | Xb)"
},
{
"formula": "(Ga | ((a) U (b)))"
},
{
"formula": "(G!a | ((b) U (a)))"
},
{
"formula": "(Ga | ((b) R (c)) | ((a) U (d)))"
"formula": "(((a) R (b)) | ((c) W (d)))"
},
{
"formula": "F(a \u0026 b)",
......@@ -1520,6 +1522,17 @@
{
"formula": "F(a \u0026 Gb \u0026 XGc)"
},
{
"formula": "F(!a \u0026 Xa \u0026 X((!a) M (b)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "F((a | Fb) \u0026 (c | Fd) \u0026 (e | Ff))",
"properties": {
......@@ -1623,6 +1636,9 @@
{
"formula": "G(a | Fb | XFc)"
},
{
"formula": "G(a | X!a | X((a) W (b)))"
},
{
"formula": "G(!a | b | ((b) R ((a | b))))"
},
......@@ -1657,19 +1673,38 @@
"formula": "XF(a \u0026 Gb)"
},
{
"formula": "XF(a \u0026 b \u0026 F!b \u0026 ((!b) R (c)))"
"formula": "XF(a \u0026 b \u0026 ((!b) M (c)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "XF(a \u0026 !b \u0026 Fb \u0026 ((b) R (c)))"
"formula": "XF(a \u0026 !b \u0026 ((b) M (c)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": false,
"deterministic": false
}
},
{
"formula": "XG(a | Fb)"
},
{
"formula": "XG(a | b | G!b | ((!b) U (c)))"
"formula": "XG(a | b | ((!b) W (c)))"
},
{
"formula": "XG(a | !b | ((b) W (c)))"
},
{
"formula": "XG(a | !b | Gb | ((b) U (c)))"
"formula": "((a) M ((a | b | X((a) R (c)))))"
},
{
"formula": "((a) R ((b | X((c) R (d)))))"
......@@ -1745,6 +1780,9 @@
"deterministic": true
}
},
{
"formula": "((a) W ((a \u0026 b \u0026 X((a) U (c)))))"
},
{
"formula": "(a \u0026 F(b \u0026 (a | Gb)))"
},
......@@ -1759,9 +1797,6 @@
"deterministic": false
}
},
{
"formula": "(Fa \u0026 ((a) R ((a | b | X((a) R (c))))))"
},
{
"formula": "(Fa \u0026 (((b \u0026 ((a) R ((a | c))))) R (!a)))"
},
......@@ -1873,9 +1908,6 @@
{
"formula": "(Ga | XG(b | Xc))"
},
{
"formula": "(Ga | ((a) U ((a \u0026 b \u0026 X((a) U (c))))))"
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c))))) U (a)))"
},
......@@ -2096,9 +2128,6 @@
{
"formula": "F((a | Xb) \u0026 (b | XGc))"
},
{
"formula": "F(!a \u0026 Xa \u0026 X(F!a \u0026 ((!a) R (b))))"
},
{
"formula": "F((a | XXb) \u0026 (b | XXc) \u0026 (c | XGd))"
},
......@@ -2159,9 +2188,6 @@
{
"formula": "G((!a \u0026 Xa) | ((b | X!b) \u0026 (!b | Xb)))"
},
{
"formula": "G(a | X!a | X(Ga | ((a) U (b))))"
},
{
"formula": "G((a \u0026 XXb) | (b \u0026 XXc) | (c \u0026 XFd))"
},
......@@ -2423,6 +2449,9 @@
"deterministic": true
}
},
{
"formula": "((a) M ((a \u0026 ((b) M ((b | c | X((b) R (d))))))))"
},
{
"formula": "((((!a) M (((b | XGa) \u0026 (!b | XF!a))))) M (!a))"
},
......@@ -2441,10 +2470,10 @@
}
},
{
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))"
"formula": "((a) W ((a | ((b) W ((b \u0026 c \u0026 X((b) U (d))))))))"
},
{
"formula": "(Fa \u0026 ((a) R ((a \u0026 Fb \u0026 ((b) R ((b | c | X((b) R (d)))))))))"
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))"
},
{
"formula": "(Fa \u0026 (((b \u0026 ((a) R ((a | c | X((a) R (d))))))) R (!a)))"
......@@ -2470,9 +2499,6 @@
{
"formula": "(Ga \u0026 G!b \u0026 Gc \u0026 XGb \u0026 X(Xa \u0026 ((!b) R (((b) R (((!b) R ((a \u0026 d)))))))))"
},
{
"formula": "(Ga | ((a) U ((a | Gb | ((b) U ((b \u0026 c \u0026 X((b) U (d)))))))))"
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 X((!a) U (d))))))) U (a)))"
},
......@@ -2515,13 +2541,13 @@
"formula": "F(a \u0026 F(b \u0026 (c | d | X((d) R (e)))))"
},
{
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))"
"formula": "F(a \u0026 ((b) M ((c \u0026 (b | d | X((b) R (e)))))))"
},
{
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))"
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))"
},
{
"formula": "F(a \u0026 Fb \u0026 ((b) R ((c \u0026 (b | d | X((b) R (e)))))))"
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))"
},
{
"formula": "F(a \u0026 Fb \u0026 ((c) R ((!b \u0026 (c | d | X((c) R (e)))))))"
......@@ -2551,13 +2577,13 @@
"formula": "G(a | ((!b) U (((b) U (((!b) U (((b) U ((b \u0026 c))))))))))"
},
{
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))"
"formula": "G(a | ((b) W ((c | (b \u0026 d \u0026 X((b) U (e)))))))"
},
{
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))"
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))"
},
{
"formula": "G(a | Gb | ((b) U ((c | (b \u0026 d \u0026 X((b) U (e)))))))"
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))"
},
{
"formula": "G(a | Gb | ((!b) U ((c | (!b \u0026 d \u0026 X((!b) U (e)))))))"
......@@ -2577,6 +2603,20 @@
{
"formula": "G(a | G(b | XGc) | (((b | Fd | XG(c | d))) U ((d | e))))"
},
{
"formula": "((a) M ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd)))))"
},
{
"formula": "((a) M ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb)))))))))))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "BuchiAcceptance",
"acceptanceSets": 1,
"complete": true,
"deterministic": true
}
},
{
"formula": "((a) R ((!b | !c | ((Gb) M (((c | d) \u0026 (!d | ((!c) R ((a | !c))))))))))"
},
......@@ -2584,10 +2624,10 @@
"formula": "((a) U ((b \u0026 c \u0026 ((F!b) W (((!c \u0026 !d) | (d \u0026 ((c) U ((a \u0026 c))))))))))"
},
{
"formula": "(Fa \u0026 ((a) R ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd))))))"
"formula": "((!a) W ((a \u0026 (((b) U (c)) | G(b | XGd)))))"
},
{
"formula": "(Fa \u0026 ((a) R ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb))))))))))))"
"formula": "((!a) W ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b)))))))))))"
},
{
"formula": "(Fa \u0026 (((b \u0026 ((a) R ((a | c | d | X(((a | d)) R (e))))))) R (!a)))"
......@@ -2598,12 +2638,6 @@
{
"formula": "(FG(a | XXXXa) \u0026 FG(!a | XXXX!a))"
},
{
"formula": "(G!a | ((!a) U ((a \u0026 (((b) U (c)) | G(b | XGd))))))"
},
{
"formula": "(G!a | ((!a) U ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b))))))))))))"
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 d \u0026 X(((!a \u0026 d)) U (e))))))) U (a)))"
},
......
......@@ -208,17 +208,6 @@
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R (b)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((b) R (!a)))",
"properties": {
......@@ -253,7 +242,7 @@
}
},
{
"formula": "(Fa \u0026 ((a) R (b)) \u0026 ((c) U (d)))",
"formula": "(((a) M (b)) \u0026 ((c) U (d)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -362,17 +351,6 @@
"deterministic": true
}
},
{
"formula": "(Ga | ((a) U (b)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | ((b) U (a)))",
"properties": {
......@@ -385,7 +363,7 @@
}
},
{
"formula": "(Ga | ((b) R (c)) | ((a) U (d)))",
"formula": "(((a) R (b)) | ((c) W (d)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -3431,6 +3409,17 @@
"deterministic": true
}
},
{
"formula": "((a) M ((a | b | X((a) R (c)))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((a) R ((b | X((c) R (d)))))",
"properties": {
......@@ -3564,7 +3553,7 @@
}
},
{
"formula": "(a \u0026 F(b \u0026 (a | Gb)))",
"formula": "((a) W ((a \u0026 b \u0026 X((a) U (c)))))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -3575,24 +3564,24 @@
}
},
{
"formula": "(Fa \u0026 XF(b \u0026 Xc))",
"formula": "(a \u0026 F(b \u0026 (a | Gb)))",
"properties": {
"size": 7,
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"complete": false,
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R ((a | b | X((a) R (c))))))",
"formula": "(Fa \u0026 XF(b \u0026 Xc))",
"properties": {
"size": 3,
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"complete": true,
"deterministic": true
}
},
......@@ -3959,17 +3948,6 @@
"deterministic": true
}
},
{
"formula": "(Ga | ((a) U ((a \u0026 b \u0026 X((a) U (c))))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c))))) U (a)))",
"properties": {
......@@ -5323,6 +5301,17 @@
"deterministic": true
}
},
{
"formula": "((a) M ((a \u0026 ((b) M ((b | c | X((b) R (d))))))))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((!a) M (((b | XGa) \u0026 (!b | XF!a))))) M (!a))",
"properties": {
......@@ -5357,20 +5346,20 @@
}
},
{
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))",
"formula": "((a) W ((a | ((b) W ((b \u0026 c \u0026 X((b) U (d))))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R ((a \u0026 Fb \u0026 ((b) R ((b | c | X((b) R (d)))))))))",
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))",
"properties": {
"size": 4,
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 4,
......@@ -5455,17 +5444,6 @@
"deterministic": true
}
},
{
"formula": "(Ga | ((a) U ((a | Gb | ((b) U ((b \u0026 c \u0026 X((b) U (d)))))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 X((!a) U (d))))))) U (a)))",
"properties": {
......@@ -5577,9 +5555,9 @@
}
},
{
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))",
"formula": "F(a \u0026 ((b) M ((c \u0026 (b | d | X((b) R (e)))))))",
"properties": {
"size": 13,
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
......@@ -5588,9 +5566,9 @@
}
},
{
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))",
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))",
"properties": {
"size": 6,
"size": 13,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
......@@ -5599,9 +5577,9 @@
}
},
{
"formula": "F(a \u0026 Fb \u0026 ((b) R ((c \u0026 (b | d | X((b) R (e)))))))",
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))",
"properties": {
"size": 4,
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
......@@ -5698,34 +5676,34 @@
}
},
{
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))",
"formula": "G(a | ((b) W ((c | (b \u0026 d \u0026 X((b) U (e)))))))",
"properties": {
"size": 6,
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 36,
"complete": true,
"acceptanceSets": 4,
"complete": false,
"deterministic": true
}
},
{
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))",
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))",
"properties": {
"size": 137,
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 24,
"complete": false,
"acceptanceSets": 36,
"complete": true,
"deterministic": true
}
},
{
"formula": "G(a | Gb | ((b) U ((c | (b \u0026 d \u0026 X((b) U (e)))))))",
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))",
"properties": {
"size": 11,
"size": 137,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 12,
"acceptanceSets": 24,
"complete": false,
"deterministic": true
}
......@@ -5785,6 +5763,28 @@
"deterministic": true
}
},
{
"formula": "((a) M ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd)))))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((a) M ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb)))))))))))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((a) R ((!b | !c | ((Gb) M (((c | d) \u0026 (!d | ((!c) R ((a | !c))))))))))",
"properties": {
......@@ -5808,24 +5808,24 @@
}
},
{
"formula": "(Fa \u0026 ((a) R ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd))))))",
"formula": "((!a) W ((a \u0026 (((b) U (c)) | G(b | XGd)))))",
"properties": {
"size": 4,
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 6,
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb))))))))))))",
"formula": "((!a) W ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b)))))))))))",
"properties": {
"size": 7,
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 12,
"complete": true,
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
......@@ -5862,28 +5862,6 @@
"deterministic": true
}
},
{
"formula": "(G!a | ((!a) U ((a \u0026 (((b) U (c)) | G(b | XGd))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | ((!a) U ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b))))))))))))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "GeneralizedRabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 d \u0026 X(((!a \u0026 d)) U (e))))))) U (a)))",
"properties": {
......
This diff is collapsed.
......@@ -208,17 +208,6 @@
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R (b)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((b) R (!a)))",
"properties": {
......@@ -253,7 +242,7 @@
}
},
{
"formula": "(Fa \u0026 ((a) R (b)) \u0026 ((c) U (d)))",
"formula": "(((a) M (b)) \u0026 ((c) U (d)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -362,17 +351,6 @@
"deterministic": true
}
},
{
"formula": "(Ga | ((a) U (b)))",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | ((b) U (a)))",
"properties": {
......@@ -385,7 +363,7 @@
}
},
{
"formula": "(Ga | ((b) R (c)) | ((a) U (d)))",
"formula": "(((a) R (b)) | ((c) W (d)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -3431,6 +3409,17 @@
"deterministic": true
}
},
{
"formula": "((a) M ((a | b | X((a) R (c)))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((a) R ((b | X((c) R (d)))))",
"properties": {
......@@ -3564,7 +3553,7 @@
}
},
{
"formula": "(a \u0026 F(b \u0026 (a | Gb)))",
"formula": "((a) W ((a \u0026 b \u0026 X((a) U (c)))))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -3575,24 +3564,24 @@
}
},
{
"formula": "(Fa \u0026 XF(b \u0026 Xc))",
"formula": "(a \u0026 F(b \u0026 (a | Gb)))",
"properties": {
"size": 7,
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": true,
"complete": false,
"deterministic": true
}
},
{
"formula": "(Fa \u0026 ((a) R ((a | b | X((a) R (c))))))",
"formula": "(Fa \u0026 XF(b \u0026 Xc))",
"properties": {
"size": 3,
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"complete": true,
"deterministic": true
}
},
......@@ -3959,17 +3948,6 @@
"deterministic": true
}
},
{
"formula": "(Ga | ((a) U ((a \u0026 b \u0026 X((a) U (c))))))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c))))) U (a)))",
"properties": {
......@@ -5323,6 +5301,17 @@
"deterministic": true
}
},
{
"formula": "((a) M ((a \u0026 ((b) M ((b | c | X((b) R (d))))))))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((((!a) M (((b | XGa) \u0026 (!b | XF!a))))) M (!a))",
"properties": {
......@@ -5357,7 +5346,7 @@
}
},
{
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))",
"formula": "((a) W ((a | ((b) W ((b \u0026 c \u0026 X((b) U (d))))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
......@@ -5368,9 +5357,9 @@
}
},
{
"formula": "(Fa \u0026 ((a) R ((a \u0026 Fb \u0026 ((b) R ((b | c | X((b) R (d)))))))))",
"formula": "((((a) W (((b \u0026 XGa) | (!b \u0026 XF!a))))) W (a))",
"properties": {
"size": 4,
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
......@@ -5455,17 +5444,6 @@
"deterministic": true
}
},
{
"formula": "(Ga | ((a) U ((a | Gb | ((b) U ((b \u0026 c \u0026 X((b) U (d)))))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 X((!a) U (d))))))) U (a)))",
"properties": {
......@@ -5577,9 +5555,9 @@
}
},
{
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))",
"formula": "F(a \u0026 ((b) M ((c \u0026 (b | d | X((b) R (e)))))))",
"properties": {
"size": 13,
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
......@@ -5588,9 +5566,9 @@
}
},
{
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))",
"formula": "F(a \u0026 ((!a) R ((b | ((b) R ((c | ((c) R (d)))))))))",
"properties": {
"size": 6,
"size": 13,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
......@@ -5599,9 +5577,9 @@
}
},
{
"formula": "F(a \u0026 Fb \u0026 ((b) R ((c \u0026 (b | d | X((b) R (e)))))))",
"formula": "F(a \u0026 ((b) R (((!b) R (((b) R (((!b) R ((!b | c))))))))))",
"properties": {
"size": 4,
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
......@@ -5698,34 +5676,34 @@
}
},
{
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))",
"formula": "G(a | ((b) W ((c | (b \u0026 d \u0026 X((b) U (e)))))))",
"properties": {
"size": 12,
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 4,
"complete": true,
"complete": false,
"deterministic": true
}
},
{
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))",
"formula": "G(!a | ((!a | F(!b \u0026 !c) | FG!c) \u0026 (a | (G(b | c) \u0026 GFc))))",
"properties": {
"size": 499,
"size": 12,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 9,
"complete": false,
"acceptanceSets": 4,
"complete": true,
"deterministic": true
}
},
{
"formula": "G(a | Gb | ((b) U ((c | (b \u0026 d \u0026 X((b) U (e)))))))",
"formula": "G(!a | ((a) U ((b \u0026 ((b) U ((c \u0026 ((c) U (d)))))))))",
"properties": {
"size": 16,
"size": 499,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 6,
"acceptanceSets": 9,
"complete": false,
"deterministic": true
}
......@@ -5785,6 +5763,28 @@
"deterministic": true
}
},
{
"formula": "((a) M ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd)))))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "((a) M ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb)))))))))))",
"properties": {
"size": 7,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "((a) R ((!b | !c | ((Gb) M (((c | d) \u0026 (!d | ((!c) R ((a | !c))))))))))",
"properties": {
......@@ -5808,9 +5808,9 @@
}
},
{
"formula": "(Fa \u0026 ((a) R ((!a | (((b) R (c)) \u0026 F(b \u0026 XFd))))))",
"formula": "((!a) W ((a \u0026 (((b) U (c)) | G(b | XGd)))))",
"properties": {
"size": 4,
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
......@@ -5819,13 +5819,13 @@
}
},
{
"formula": "(Fa \u0026 ((a) R ((!a | ((b) M (((!b) M (((b) M (((!b) M (Fb))))))))))))",
"formula": "((!a) W ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b)))))))))))",
"properties": {
"size": 7,
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": true,
"complete": false,
"deterministic": true
}
},
......@@ -5862,28 +5862,6 @@
"deterministic": true
}
},
{
"formula": "(G!a | ((!a) U ((a \u0026 (((b) U (c)) | G(b | XGd))))))",
"properties": {
"size": 5,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | ((!a) U ((a \u0026 ((!b) W (((b) W (((!b) W (((b) W (G!b))))))))))))",
"properties": {
"size": 6,
"initialStatesSize": 1,
"acceptanceName": "ParityAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "(G!a | (((b | ((!a) U ((!a \u0026 c \u0026 d \u0026 X(((!a \u0026 d)) U (e))))))) U (a)))",
"properties": {
......
......@@ -44,7 +44,7 @@
}
},
{
"formula": "((a) R (b))",
"formula": "((a) M (b))",
"properties": {
"size": 2,
"initialStatesSize": 1,
......@@ -55,7 +55,7 @@
}
},
{
"formula": "((a) U (b))",
"formula": "((a) R (b))",
"properties": {
"size": 2,
"initialStatesSize": 1,
......@@ -66,7 +66,7 @@
}
},
{
"formula": "(Fa \u0026 ((a) R (b)))",
"formula": "((a) U (b))",
"properties": {
"size": 2,
"initialStatesSize": 1,
......@@ -77,9 +77,9 @@
}
},
{
"formula": "(Ga \u0026 Gb)",
"formula": "((a) W (b))",
"properties": {
"size": 1,
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 2,
......@@ -88,24 +88,24 @@
}
},
{
"formula": "(Fa | Fb)",
"formula": "(Ga \u0026 Gb)",
"properties": {
"size": 2,
"size": 1,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"complete": false,
"deterministic": true
}
},
{
"formula": "(Ga | ((a) U (b)))",
"formula": "(Fa | Fb)",
"properties": {
"size": 2,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"complete": true,
"deterministic": true
}
},
......@@ -494,6 +494,17 @@
"deterministic": true
}
},
{
"formula": "F(!a \u0026 Xa \u0026 X((!a) M (b)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 2,
"complete": true,
"deterministic": true
}
},
{
"formula": "F((a | X!a) \u0026 (b | Xb) \u0026 (!b | X!b))",
"properties": {
......@@ -549,6 +560,17 @@
"deterministic": true
}
},
{
"formula": "G(a | X!a | X((a) W (b)))",
"properties": {
"size": 3,
"initialStatesSize": 1,
"acceptanceName": "RabinAcceptance",
"acceptanceSets": 2,
"complete": false,
"deterministic": true
}
},
{
"formula": "G((!a \u0026 Xa) | (b \u0026 Xb) | (!b \u0026 X!b))",
"properties": {
......@@ -572,7 +594,7 @@
}
},
{
"formula": "XF(a \u0026 b \u0026 F!b \u0026 ((!b) R (c)))",
"formula": "XF(a \u0026 b \u0026 ((!b) M (c)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -583,7 +605,7 @@
}
},
{
"formula": "XF(a \u0026 !b \u0026 Fb \u0026 ((b) R (c)))",
"formula": "XF(a \u0026 !b \u0026 ((b) M (c)))",
"properties": {
"size": 4,
"initialStatesSize": 1,
......@@ -594,23 +616,23 @@
}
},
{
"formula": "XG(a | b | G!b | ((!b) U (c)))",
"formula": "XG(a | b | ((!b) W (c)))",