Commit 93934ffe authored by Tobias MEGGENDORFER's avatar Tobias MEGGENDORFER
Browse files

Gossip

parent 7c4ffe37
......@@ -7,6 +7,7 @@ if __name__ == "__main__":
"name": f"gossip{n}",
"ap": [f"g{i}" for i in range(1, n + 1)],
"type": "module",
"goal": f"F G ({' & '.join(f'g{i}' for i in range(1, n + 1))})",
"modules": {
f"A{i}": {
"goal": f"G F g{i}",
......@@ -41,7 +42,7 @@ if __name__ == "__main__":
{
"action": "g",
"guard": " | ".join(f"g{j}" for j in range(1, n+1) if j != i),
"to": "s2"
"to": "s1"
}
]
}
......
{
"name": "gossip2",
"type": "module",
"ap": [
"g1",
"g2"
],
"type": "module",
"goal": "F G (g1 & g2)",
"modules": {
"A1": {
"goal": "G F g1",
"payoff": "?",
"actions": ["a", "g", "w"],
"labels": ["g1"],
"initial": "s11",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g1"
],
"initial": "s1",
"states": {
"s11": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s11"
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s12"
"to": "s2"
}
]
},
"s12": {
"labels": ["g1"],
"s2": {
"labels": [
"g1"
],
"transitions": [
{
"action": "w",
"guard": "!g2",
"to": "s12"
"to": "s2"
},
{
"action": "a",
"action": "g",
"guard": "g2",
"to": "s11"
"to": "s1"
}
]
}
......@@ -48,37 +57,45 @@
"A2": {
"goal": "G F g2",
"payoff": "?",
"actions": ["a", "g", "w"],
"labels": ["g2"],
"initial": "s21",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g2"
],
"initial": "s1",
"states": {
"s21": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s21"
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s22"
"to": "s2"
}
]
},
"s22": {
"labels": ["g2"],
"s2": {
"labels": [
"g2"
],
"transitions": [
{
"action": "w",
"guard": "!g1",
"to": "s22"
"to": "s2"
},
{
"action": "a",
"action": "g",
"guard": "g1",
"to": "s21"
"to": "s1"
}
]
}
......
{
"name": "gossip3",
"type": "module",
"ap": [
"g1",
"g2",
"g3"
],
"type": "module",
"goal": "F G (g1 & g2 & g3)",
"modules": {
"A1": {
"goal": "G F g1",
......@@ -46,7 +47,7 @@
"to": "s2"
},
{
"action": "a",
"action": "g",
"guard": "g2 | g3",
"to": "s1"
}
......@@ -93,7 +94,7 @@
"to": "s2"
},
{
"action": "a",
"action": "g",
"guard": "g1 | g3",
"to": "s1"
}
......@@ -140,7 +141,7 @@
"to": "s2"
},
{
"action": "a",
"action": "g",
"guard": "g1 | g2",
"to": "s1"
}
......
{
"name": "gossip4",
"type": "module",
"ap": [
"g1",
"g2",
"g3",
"g4"
],
"type": "module",
"goal": "F G (g1 & g2 & g3 & g4)",
"modules": {
"A1": {
"goal": "G F g1",
......@@ -49,7 +50,7 @@
{
"action": "g",
"guard": "g2 | g3 | g4",
"to": "s2"
"to": "s1"
}
]
}
......@@ -96,7 +97,7 @@
{
"action": "g",
"guard": "g1 | g3 | g4",
"to": "s2"
"to": "s1"
}
]
}
......@@ -143,7 +144,7 @@
{
"action": "g",
"guard": "g1 | g2 | g4",
"to": "s2"
"to": "s1"
}
]
}
......@@ -190,11 +191,11 @@
{
"action": "g",
"guard": "g1 | g2 | g3",
"to": "s2"
"to": "s1"
}
]
}
}
}
}
}
}
\ No newline at end of file
{
"name": "gossip5",
"ap": [
"g1",
"g2",
"g3",
"g4",
"g5"
],
"type": "module",
"goal": "F G (g1 & g2 & g3 & g4 & g5)",
"modules": {
"A1": {
"goal": "G F g1",
"payoff": "?",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g1"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g1"
],
"transitions": [
{
"action": "w",
"guard": "!g2 & !g3 & !g4 & !g5",
"to": "s2"
},
{
"action": "g",
"guard": "g2 | g3 | g4 | g5",
"to": "s1"
}
]
}
}
},
"A2": {
"goal": "G F g2",
"payoff": "?",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g2"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g2"
],
"transitions": [
{
"action": "w",
"guard": "!g1 & !g3 & !g4 & !g5",
"to": "s2"
},
{
"action": "g",
"guard": "g1 | g3 | g4 | g5",
"to": "s1"
}
]
}
}
},
"A3": {
"goal": "G F g3",
"payoff": "?",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g3"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g3"
],
"transitions": [
{
"action": "w",
"guard": "!g1 & !g2 & !g4 & !g5",
"to": "s2"
},
{
"action": "g",
"guard": "g1 | g2 | g4 | g5",
"to": "s1"
}
]
}
}
},
"A4": {
"goal": "G F g4",
"payoff": "?",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g4"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g4"
],
"transitions": [
{
"action": "w",
"guard": "!g1 & !g2 & !g3 & !g5",
"to": "s2"
},
{
"action": "g",
"guard": "g1 | g2 | g3 | g5",
"to": "s1"
}
]
}
}
},
"A5": {
"goal": "G F g5",
"payoff": "?",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g5"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g5"
],
"transitions": [
{
"action": "w",
"guard": "!g1 & !g2 & !g3 & !g4",
"to": "s2"
},
{
"action": "g",
"guard": "g1 | g2 | g3 | g4",
"to": "s1"
}
]
}
}
}
}
}
\ No newline at end of file
{
"name": "gossip6",
"type": "module",
"ap": [
"g1",
"g2",
......@@ -9,6 +8,8 @@
"g5",
"g6"
],
"type": "module",
"goal": "F G (g1 & g2 & g3 & g4 & g5 & g6)",
"modules": {
"A1": {
"goal": "G F g1",
......@@ -51,7 +52,7 @@
{
"action": "g",
"guard": "g2 | g3 | g4 | g5 | g6",
"to": "s2"
"to": "s1"
}
]
}
......@@ -98,7 +99,7 @@
{
"action": "g",
"guard": "g1 | g3 | g4 | g5 | g6",
"to": "s2"
"to": "s1"
}
]
}
......@@ -145,7 +146,7 @@
{
"action": "g",
"guard": "g1 | g2 | g4 | g5 | g6",
"to": "s2"
"to": "s1"
}
]
}
......@@ -192,7 +193,7 @@
{
"action": "g",
"guard": "g1 | g2 | g3 | g5 | g6",
"to": "s2"
"to": "s1"
}
]
}
......@@ -239,7 +240,7 @@
{
"action": "g",
"guard": "g1 | g2 | g3 | g4 | g6",
"to": "s2"
"to": "s1"
}
]
}
......@@ -286,11 +287,11 @@
{
"action": "g",
"guard": "g1 | g2 | g3 | g4 | g5",
"to": "s2"
"to": "s1"
}
]
}
}
}
}
}
}
\ No newline at end of file
{
"name": "gossip7",
"ap": [
"g1",
"g2",
"g3",
"g4",
"g5",
"g6",
"g7"
],
"type": "module",
"goal": "F G (g1 & g2 & g3 & g4 & g5 & g6 & g7)",
"modules": {
"A1": {
"goal": "G F g1",
"payoff": "?",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g1"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{
"action": "a",
"guard": "true",
"to": "s1"
},
{
"action": "g",
"guard": "true",
"to": "s2"
}
]
},
"s2": {
"labels": [
"g1"
],
"transitions": [
{
"action": "w",
"guard": "!g2 & !g3 & !g4 & !g5 & !g6 & !g7",
"to": "s2"
},
{
"action": "g",
"guard": "g2 | g3 | g4 | g5 | g6 | g7",
"to": "s1"
}
]
}
}
},
"A2": {
"goal": "G F g2",
"payoff": "?",
"actions": [
"a",
"g",
"w"
],
"labels": [
"g2"
],
"initial": "s1",
"states": {
"s1": {
"labels": [],
"transitions": [
{