{ "actions": [ { "name": "receiveA" }, { "name": "receiveB" } ], "automata": [ { "edges": [ { "destinations": [ { "assignments": [ { "comment": "phase <- 4", "ref": "phase", "value": 4 } ], "location": "l" } ], "guard": { "comment": "(phase = 4)", "exp": { "left": "phase", "op": "=", "right": 4 } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "n <- (n + 1)", "ref": "n", "value": { "left": "n", "op": "+", "right": 1 } }, { "comment": "party <- 1", "ref": "party", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(((phase = 1) & (party = 2)) & (n < (10 - 1)))", "exp": { "left": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "party", "op": "=", "right": 2 } }, "op": "∧", "right": { "left": "n", "op": "<", "right": 9 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "n <- 0", "ref": "n", "value": 0 }, { "comment": "phase <- 2", "ref": "phase", "value": 2 }, { "comment": "party <- 1", "ref": "party", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(((phase = 1) & (party = 2)) & (n = (10 - 1)))", "exp": { "left": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "party", "op": "=", "right": 2 } }, "op": "∧", "right": { "left": "n", "op": "=", "right": 9 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "n <- (n + 1)", "ref": "n", "value": { "left": "n", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "((((phase >= 2) & (phase <= 3)) & (party = 2)) & (n < (10 - 1)))", "exp": { "left": { "left": { "left": "n", "op": "<", "right": 9 }, "op": "∧", "right": { "left": "phase", "op": "≤", "right": 3 } }, "op": "∧", "right": { "left": { "left": "party", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "phase", "op": "≥", "right": 2 } } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "n <- 1", "ref": "n", "value": 1 }, { "comment": "party <- 1", "ref": "party", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((((phase >= 2) & (phase <= 3)) & (party = 2)) & (n = (10 - 1)))", "exp": { "left": { "left": { "left": "n", "op": "=", "right": 9 }, "op": "∧", "right": { "left": "phase", "op": "≤", "right": 3 } }, "op": "∧", "right": { "left": { "left": "party", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "phase", "op": "≥", "right": 2 } } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "party <- 2", "ref": "party", "value": 2 } ], "location": "l" } ], "guard": { "comment": "((phase = 1) & (party = 1))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "party", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "party <- 2", "ref": "party", "value": 2 } ], "location": "l" } ], "guard": { "comment": "((((phase >= 2) & (phase <= 3)) & (party = 1)) & (n = 0))", "exp": { "left": { "left": { "left": "n", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "phase", "op": "≤", "right": 3 } }, "op": "∧", "right": { "left": { "left": "party", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "phase", "op": "≥", "right": 2 } } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "n <- (n + 1)", "ref": "n", "value": { "left": "n", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "(((((phase >= 2) & (phase <= 3)) & (party = 1)) & (n < (10 - 1))) & (n > 0))", "exp": { "left": { "left": { "left": { "left": "n", "op": ">", "right": 0 }, "op": "∧", "right": { "left": "phase", "op": "≤", "right": 3 } }, "op": "∧", "right": { "left": "party", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": { "left": "n", "op": "<", "right": 9 }, "op": "∧", "right": { "left": "phase", "op": "≥", "right": 2 } } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "b <- (b + 1)", "ref": "b", "value": { "left": "b", "op": "+", "right": 1 } }, { "comment": "n <- 0", "ref": "n", "value": 0 }, { "comment": "party <- 1", "ref": "party", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(((((phase >= 2) & (phase <= 3)) & (party = 1)) & (n = (10 - 1))) & (b < 8))", "exp": { "left": { "left": { "left": { "left": "b", "op": "<", "right": 8 }, "op": "∧", "right": { "left": "phase", "op": "≤", "right": 3 } }, "op": "∧", "right": { "left": "party", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": { "left": "n", "op": "=", "right": 9 }, "op": "∧", "right": { "left": "phase", "op": "≥", "right": 2 } } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "b <- 1", "ref": "b", "value": 1 }, { "comment": "n <- 0", "ref": "n", "value": 0 }, { "comment": "phase <- 3", "ref": "phase", "value": 3 }, { "comment": "party <- 1", "ref": "party", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((((phase = 2) & (party = 1)) & (n = (10 - 1))) & (b = 8))", "exp": { "left": { "left": { "left": "b", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "party", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": { "left": "n", "op": "=", "right": 9 }, "op": "∧", "right": { "left": "phase", "op": "=", "right": 2 } } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "phase <- 4", "ref": "phase", "value": 4 } ], "location": "l" } ], "guard": { "comment": "((((phase = 3) & (party = 1)) & (n = (10 - 1))) & (b = 8))", "exp": { "left": { "left": { "left": "b", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "party", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": { "left": "n", "op": "=", "right": 9 }, "op": "∧", "right": { "left": "phase", "op": "=", "right": 3 } } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l", "transient-values": [ { "comment": "knowB <- kB(a0, a20, a1, a21, a2, a22, a3, a23, a4, a24, a5, a25, a6, a26, a7, a27, a8, a28, a9, a29, a10, a30, a11, a31, a12, a32, a13, a33, a14, a34, a15, a35, a16, a36, a17, a37, a18, a38, a19, a39)", "ref": "knowB", "value": { "args": [ "a0", "a20", "a1", "a21", "a2", "a22", "a3", "a23", "a4", "a24", "a5", "a25", "a6", "a26", "a7", "a27", "a8", "a28", "a9", "a29", "a10", "a30", "a11", "a31", "a12", "a32", "a13", "a33", "a14", "a34", "a15", "a35", "a16", "a36", "a17", "a37", "a18", "a38", "a19", "a39" ], "function": "kB", "op": "call" } }, { "comment": "knowA <- kA(b0, b20, b1, b21, b2, b22, b3, b23, b4, b24, b5, b25, b6, b26, b7, b27, b8, b28, b9, b29, b10, b30, b11, b31, b12, b32, b13, b33, b14, b34, b15, b35, b16, b36, b17, b37, b18, b38, b19, b39)", "ref": "knowA", "value": { "args": [ "b0", "b20", "b1", "b21", "b2", "b22", "b3", "b23", "b4", "b24", "b5", "b25", "b6", "b26", "b7", "b27", "b8", "b28", "b9", "b29", "b10", "b30", "b11", "b31", "b12", "b32", "b13", "b33", "b14", "b34", "b15", "b35", "b16", "b36", "b17", "b37", "b18", "b38", "b19", "b39" ], "function": "kA", "op": "call" } } ] } ], "name": "counter", "variables": [ { "initial-value": 1, "name": "b", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 8 } }, { "initial-value": 1, "name": "party", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 2 } } ] }, { "edges": [ { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b0 <- 8", "ref": "b0", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b20 <- 8", "ref": "b20", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 0))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 0 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b1 <- 8", "ref": "b1", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b21 <- 8", "ref": "b21", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 1))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b2 <- 8", "ref": "b2", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b22 <- 8", "ref": "b22", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 2))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 2 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b3 <- 8", "ref": "b3", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b23 <- 8", "ref": "b23", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 3))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 3 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b4 <- 8", "ref": "b4", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b24 <- 8", "ref": "b24", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 4))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 4 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b5 <- 8", "ref": "b5", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b25 <- 8", "ref": "b25", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 5))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 5 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b6 <- 8", "ref": "b6", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b26 <- 8", "ref": "b26", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 6))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 6 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b7 <- 8", "ref": "b7", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b27 <- 8", "ref": "b27", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 7))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 7 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b8 <- 8", "ref": "b8", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b28 <- 8", "ref": "b28", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 8))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 8 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b9 <- 8", "ref": "b9", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b29 <- 8", "ref": "b29", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 9))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 9 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b10 <- 8", "ref": "b10", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b30 <- 8", "ref": "b30", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 10))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 10 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b11 <- 8", "ref": "b11", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b31 <- 8", "ref": "b31", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 11))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 11 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b12 <- 8", "ref": "b12", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b32 <- 8", "ref": "b32", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 12))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 12 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b13 <- 8", "ref": "b13", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b33 <- 8", "ref": "b33", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 13))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 13 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b14 <- 8", "ref": "b14", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b34 <- 8", "ref": "b34", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 14))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 14 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b15 <- 8", "ref": "b15", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b35 <- 8", "ref": "b35", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 15))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 15 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b16 <- 8", "ref": "b16", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b36 <- 8", "ref": "b36", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 16))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 16 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b17 <- 8", "ref": "b17", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b37 <- 8", "ref": "b37", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 17))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 17 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b18 <- 8", "ref": "b18", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b38 <- 8", "ref": "b38", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 18))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 18 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b19 <- 8", "ref": "b19", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b39 <- 8", "ref": "b39", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 19))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 19 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b0 <- (min((b0 + 1), 8))", "ref": "b0", "value": { "left": { "left": "b0", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 0))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 0 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b1 <- (min((b1 + 1), 8))", "ref": "b1", "value": { "left": { "left": "b1", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 1))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b2 <- (min((b2 + 1), 8))", "ref": "b2", "value": { "left": { "left": "b2", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 2))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 2 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b3 <- (min((b3 + 1), 8))", "ref": "b3", "value": { "left": { "left": "b3", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 3))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 3 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b4 <- (min((b4 + 1), 8))", "ref": "b4", "value": { "left": { "left": "b4", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 4))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 4 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b5 <- (min((b5 + 1), 8))", "ref": "b5", "value": { "left": { "left": "b5", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 5))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 5 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b6 <- (min((b6 + 1), 8))", "ref": "b6", "value": { "left": { "left": "b6", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 6))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 6 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b7 <- (min((b7 + 1), 8))", "ref": "b7", "value": { "left": { "left": "b7", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 7))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 7 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b8 <- (min((b8 + 1), 8))", "ref": "b8", "value": { "left": { "left": "b8", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 8))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 8 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b9 <- (min((b9 + 1), 8))", "ref": "b9", "value": { "left": { "left": "b9", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 9))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 9 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b10 <- (min((b10 + 1), 8))", "ref": "b10", "value": { "left": { "left": "b10", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 10))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 10 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b11 <- (min((b11 + 1), 8))", "ref": "b11", "value": { "left": { "left": "b11", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 11))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 11 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b12 <- (min((b12 + 1), 8))", "ref": "b12", "value": { "left": { "left": "b12", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 12))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 12 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b13 <- (min((b13 + 1), 8))", "ref": "b13", "value": { "left": { "left": "b13", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 13))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 13 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b14 <- (min((b14 + 1), 8))", "ref": "b14", "value": { "left": { "left": "b14", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 14))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 14 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b15 <- (min((b15 + 1), 8))", "ref": "b15", "value": { "left": { "left": "b15", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 15))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 15 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b16 <- (min((b16 + 1), 8))", "ref": "b16", "value": { "left": { "left": "b16", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 16))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 16 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b17 <- (min((b17 + 1), 8))", "ref": "b17", "value": { "left": { "left": "b17", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 17))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 17 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b18 <- (min((b18 + 1), 8))", "ref": "b18", "value": { "left": { "left": "b18", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 18))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 18 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b19 <- (min((b19 + 1), 8))", "ref": "b19", "value": { "left": { "left": "b19", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 19))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 19 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b20 <- (min((b20 + 1), 8))", "ref": "b20", "value": { "left": { "left": "b20", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 0))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 0 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b21 <- (min((b21 + 1), 8))", "ref": "b21", "value": { "left": { "left": "b21", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 1))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b22 <- (min((b22 + 1), 8))", "ref": "b22", "value": { "left": { "left": "b22", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 2))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 2 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b23 <- (min((b23 + 1), 8))", "ref": "b23", "value": { "left": { "left": "b23", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 3))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 3 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b24 <- (min((b24 + 1), 8))", "ref": "b24", "value": { "left": { "left": "b24", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 4))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 4 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b25 <- (min((b25 + 1), 8))", "ref": "b25", "value": { "left": { "left": "b25", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 5))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 5 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b26 <- (min((b26 + 1), 8))", "ref": "b26", "value": { "left": { "left": "b26", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 6))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 6 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b27 <- (min((b27 + 1), 8))", "ref": "b27", "value": { "left": { "left": "b27", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 7))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 7 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b28 <- (min((b28 + 1), 8))", "ref": "b28", "value": { "left": { "left": "b28", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 8))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 8 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b29 <- (min((b29 + 1), 8))", "ref": "b29", "value": { "left": { "left": "b29", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 9))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 9 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b30 <- (min((b30 + 1), 8))", "ref": "b30", "value": { "left": { "left": "b30", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 10))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 10 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b31 <- (min((b31 + 1), 8))", "ref": "b31", "value": { "left": { "left": "b31", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 11))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 11 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b32 <- (min((b32 + 1), 8))", "ref": "b32", "value": { "left": { "left": "b32", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 12))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 12 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b33 <- (min((b33 + 1), 8))", "ref": "b33", "value": { "left": { "left": "b33", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 13))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 13 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b34 <- (min((b34 + 1), 8))", "ref": "b34", "value": { "left": { "left": "b34", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 14))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 14 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b35 <- (min((b35 + 1), 8))", "ref": "b35", "value": { "left": { "left": "b35", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 15))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 15 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b36 <- (min((b36 + 1), 8))", "ref": "b36", "value": { "left": { "left": "b36", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 16))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 16 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b37 <- (min((b37 + 1), 8))", "ref": "b37", "value": { "left": { "left": "b37", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 17))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 17 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b38 <- (min((b38 + 1), 8))", "ref": "b38", "value": { "left": { "left": "b38", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 18))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 18 } } }, "location": "l" }, { "action": "receiveA", "destinations": [ { "assignments": [ { "comment": "b39 <- (min((b39 + 1), 8))", "ref": "b39", "value": { "left": { "left": "b39", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 19))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 19 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "partyA", "variables": [] }, { "edges": [ { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a0 <- 8", "ref": "a0", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a20 <- 8", "ref": "a20", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 0))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 0 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a1 <- 8", "ref": "a1", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a21 <- 8", "ref": "a21", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 1))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a2 <- 8", "ref": "a2", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a22 <- 8", "ref": "a22", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 2))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 2 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a3 <- 8", "ref": "a3", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a23 <- 8", "ref": "a23", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 3))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 3 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a4 <- 8", "ref": "a4", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a24 <- 8", "ref": "a24", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 4))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 4 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a5 <- 8", "ref": "a5", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a25 <- 8", "ref": "a25", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 5))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 5 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a6 <- 8", "ref": "a6", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a26 <- 8", "ref": "a26", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 6))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 6 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a7 <- 8", "ref": "a7", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a27 <- 8", "ref": "a27", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 7))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 7 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a8 <- 8", "ref": "a8", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a28 <- 8", "ref": "a28", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 8))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 8 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a9 <- 8", "ref": "a9", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a29 <- 8", "ref": "a29", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 9))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 9 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a10 <- 8", "ref": "a10", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a30 <- 8", "ref": "a30", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 10))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 10 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a11 <- 8", "ref": "a11", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a31 <- 8", "ref": "a31", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 11))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 11 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a12 <- 8", "ref": "a12", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a32 <- 8", "ref": "a32", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 12))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 12 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a13 <- 8", "ref": "a13", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a33 <- 8", "ref": "a33", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 13))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 13 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a14 <- 8", "ref": "a14", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a34 <- 8", "ref": "a34", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 14))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 14 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a15 <- 8", "ref": "a15", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a35 <- 8", "ref": "a35", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 15))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 15 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a16 <- 8", "ref": "a16", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a36 <- 8", "ref": "a36", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 16))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 16 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a17 <- 8", "ref": "a17", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a37 <- 8", "ref": "a37", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 17))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 17 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a18 <- 8", "ref": "a18", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a38 <- 8", "ref": "a38", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 18))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 18 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a19 <- 8", "ref": "a19", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "a39 <- 8", "ref": "a39", "value": 8 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((phase = 1) & (n = 19))", "exp": { "left": { "left": "phase", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 19 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a0 <- (min((a0 + 1), 8))", "ref": "a0", "value": { "left": { "left": "a0", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 0))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 0 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a1 <- (min((a1 + 1), 8))", "ref": "a1", "value": { "left": { "left": "a1", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 1))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a2 <- (min((a2 + 1), 8))", "ref": "a2", "value": { "left": { "left": "a2", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 2))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 2 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a3 <- (min((a3 + 1), 8))", "ref": "a3", "value": { "left": { "left": "a3", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 3))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 3 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a4 <- (min((a4 + 1), 8))", "ref": "a4", "value": { "left": { "left": "a4", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 4))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 4 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a5 <- (min((a5 + 1), 8))", "ref": "a5", "value": { "left": { "left": "a5", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 5))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 5 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a6 <- (min((a6 + 1), 8))", "ref": "a6", "value": { "left": { "left": "a6", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 6))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 6 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a7 <- (min((a7 + 1), 8))", "ref": "a7", "value": { "left": { "left": "a7", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 7))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 7 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a8 <- (min((a8 + 1), 8))", "ref": "a8", "value": { "left": { "left": "a8", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 8))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 8 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a9 <- (min((a9 + 1), 8))", "ref": "a9", "value": { "left": { "left": "a9", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 9))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 9 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a10 <- (min((a10 + 1), 8))", "ref": "a10", "value": { "left": { "left": "a10", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 10))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 10 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a11 <- (min((a11 + 1), 8))", "ref": "a11", "value": { "left": { "left": "a11", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 11))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 11 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a12 <- (min((a12 + 1), 8))", "ref": "a12", "value": { "left": { "left": "a12", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 12))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 12 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a13 <- (min((a13 + 1), 8))", "ref": "a13", "value": { "left": { "left": "a13", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 13))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 13 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a14 <- (min((a14 + 1), 8))", "ref": "a14", "value": { "left": { "left": "a14", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 14))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 14 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a15 <- (min((a15 + 1), 8))", "ref": "a15", "value": { "left": { "left": "a15", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 15))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 15 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a16 <- (min((a16 + 1), 8))", "ref": "a16", "value": { "left": { "left": "a16", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 16))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 16 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a17 <- (min((a17 + 1), 8))", "ref": "a17", "value": { "left": { "left": "a17", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 17))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 17 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a18 <- (min((a18 + 1), 8))", "ref": "a18", "value": { "left": { "left": "a18", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 18))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 18 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a19 <- (min((a19 + 1), 8))", "ref": "a19", "value": { "left": { "left": "a19", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 2) & (n = 19))", "exp": { "left": { "left": "phase", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 19 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a20 <- (min((a20 + 1), 8))", "ref": "a20", "value": { "left": { "left": "a20", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 0))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 0 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a21 <- (min((a21 + 1), 8))", "ref": "a21", "value": { "left": { "left": "a21", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 1))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a22 <- (min((a22 + 1), 8))", "ref": "a22", "value": { "left": { "left": "a22", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 2))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 2 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a23 <- (min((a23 + 1), 8))", "ref": "a23", "value": { "left": { "left": "a23", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 3))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 3 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a24 <- (min((a24 + 1), 8))", "ref": "a24", "value": { "left": { "left": "a24", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 4))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 4 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a25 <- (min((a25 + 1), 8))", "ref": "a25", "value": { "left": { "left": "a25", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 5))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 5 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a26 <- (min((a26 + 1), 8))", "ref": "a26", "value": { "left": { "left": "a26", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 6))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 6 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a27 <- (min((a27 + 1), 8))", "ref": "a27", "value": { "left": { "left": "a27", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 7))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 7 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a28 <- (min((a28 + 1), 8))", "ref": "a28", "value": { "left": { "left": "a28", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 8))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 8 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a29 <- (min((a29 + 1), 8))", "ref": "a29", "value": { "left": { "left": "a29", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 9))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 9 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a30 <- (min((a30 + 1), 8))", "ref": "a30", "value": { "left": { "left": "a30", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 10))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 10 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a31 <- (min((a31 + 1), 8))", "ref": "a31", "value": { "left": { "left": "a31", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 11))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 11 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a32 <- (min((a32 + 1), 8))", "ref": "a32", "value": { "left": { "left": "a32", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 12))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 12 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a33 <- (min((a33 + 1), 8))", "ref": "a33", "value": { "left": { "left": "a33", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 13))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 13 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a34 <- (min((a34 + 1), 8))", "ref": "a34", "value": { "left": { "left": "a34", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 14))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 14 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a35 <- (min((a35 + 1), 8))", "ref": "a35", "value": { "left": { "left": "a35", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 15))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 15 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a36 <- (min((a36 + 1), 8))", "ref": "a36", "value": { "left": { "left": "a36", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 16))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 16 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a37 <- (min((a37 + 1), 8))", "ref": "a37", "value": { "left": { "left": "a37", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 17))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 17 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a38 <- (min((a38 + 1), 8))", "ref": "a38", "value": { "left": { "left": "a38", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 18))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 18 } } }, "location": "l" }, { "action": "receiveB", "destinations": [ { "assignments": [ { "comment": "a39 <- (min((a39 + 1), 8))", "ref": "a39", "value": { "left": { "left": "a39", "op": "+", "right": 1 }, "op": "min", "right": 8 } } ], "location": "l" } ], "guard": { "comment": "((phase = 3) & (n = 19))", "exp": { "left": { "left": "phase", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "n", "op": "=", "right": 19 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "partyB", "variables": [] } ], "constants": [ { "name": "N", "type": "int", "value": 10 }, { "name": "L", "type": "int", "value": 8 } ], "features": [ "derived-operators", "functions" ], "functions": [ { "body": { "left": { "left": { "left": { "left": { "left": { "left": { "left": "kA__param__b19", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b39", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b1", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b21", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kA__param__b10", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b30", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b9", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b29", "op": "=", "right": 8 } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": "kA__param__b15", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b35", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b4", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b24", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kA__param__b14", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b34", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b5", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b25", "op": "=", "right": 8 } } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": "kA__param__b17", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b37", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b2", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b22", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kA__param__b12", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b32", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b7", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b27", "op": "=", "right": 8 } } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": "kA__param__b18", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b38", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b0", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b20", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kA__param__b11", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b31", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b8", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b28", "op": "=", "right": 8 } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": "kA__param__b16", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b36", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b3", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b23", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kA__param__b13", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b33", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kA__param__b6", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kA__param__b26", "op": "=", "right": 8 } } } } } }, "name": "kA", "parameters": [ { "name": "kA__param__b0", "type": "int" }, { "name": "kA__param__b20", "type": "int" }, { "name": "kA__param__b1", "type": "int" }, { "name": "kA__param__b21", "type": "int" }, { "name": "kA__param__b2", "type": "int" }, { "name": "kA__param__b22", "type": "int" }, { "name": "kA__param__b3", "type": "int" }, { "name": "kA__param__b23", "type": "int" }, { "name": "kA__param__b4", "type": "int" }, { "name": "kA__param__b24", "type": "int" }, { "name": "kA__param__b5", "type": "int" }, { "name": "kA__param__b25", "type": "int" }, { "name": "kA__param__b6", "type": "int" }, { "name": "kA__param__b26", "type": "int" }, { "name": "kA__param__b7", "type": "int" }, { "name": "kA__param__b27", "type": "int" }, { "name": "kA__param__b8", "type": "int" }, { "name": "kA__param__b28", "type": "int" }, { "name": "kA__param__b9", "type": "int" }, { "name": "kA__param__b29", "type": "int" }, { "name": "kA__param__b10", "type": "int" }, { "name": "kA__param__b30", "type": "int" }, { "name": "kA__param__b11", "type": "int" }, { "name": "kA__param__b31", "type": "int" }, { "name": "kA__param__b12", "type": "int" }, { "name": "kA__param__b32", "type": "int" }, { "name": "kA__param__b13", "type": "int" }, { "name": "kA__param__b33", "type": "int" }, { "name": "kA__param__b14", "type": "int" }, { "name": "kA__param__b34", "type": "int" }, { "name": "kA__param__b15", "type": "int" }, { "name": "kA__param__b35", "type": "int" }, { "name": "kA__param__b16", "type": "int" }, { "name": "kA__param__b36", "type": "int" }, { "name": "kA__param__b17", "type": "int" }, { "name": "kA__param__b37", "type": "int" }, { "name": "kA__param__b18", "type": "int" }, { "name": "kA__param__b38", "type": "int" }, { "name": "kA__param__b19", "type": "int" }, { "name": "kA__param__b39", "type": "int" } ], "type": "bool" }, { "body": { "left": { "left": { "left": { "left": { "left": { "left": { "left": "kB__param__a19", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a39", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a1", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a21", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kB__param__a10", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a30", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a9", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a29", "op": "=", "right": 8 } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": "kB__param__a15", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a35", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a4", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a24", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kB__param__a14", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a34", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a5", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a25", "op": "=", "right": 8 } } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": "kB__param__a17", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a37", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a2", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a22", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kB__param__a12", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a32", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a7", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a27", "op": "=", "right": 8 } } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": "kB__param__a18", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a38", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a0", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a20", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kB__param__a11", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a31", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a8", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a28", "op": "=", "right": 8 } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": "kB__param__a16", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a36", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a3", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a23", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "kB__param__a13", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a33", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": "kB__param__a6", "op": "=", "right": 8 }, "op": "∧", "right": { "left": "kB__param__a26", "op": "=", "right": 8 } } } } } }, "name": "kB", "parameters": [ { "name": "kB__param__a0", "type": "int" }, { "name": "kB__param__a20", "type": "int" }, { "name": "kB__param__a1", "type": "int" }, { "name": "kB__param__a21", "type": "int" }, { "name": "kB__param__a2", "type": "int" }, { "name": "kB__param__a22", "type": "int" }, { "name": "kB__param__a3", "type": "int" }, { "name": "kB__param__a23", "type": "int" }, { "name": "kB__param__a4", "type": "int" }, { "name": "kB__param__a24", "type": "int" }, { "name": "kB__param__a5", "type": "int" }, { "name": "kB__param__a25", "type": "int" }, { "name": "kB__param__a6", "type": "int" }, { "name": "kB__param__a26", "type": "int" }, { "name": "kB__param__a7", "type": "int" }, { "name": "kB__param__a27", "type": "int" }, { "name": "kB__param__a8", "type": "int" }, { "name": "kB__param__a28", "type": "int" }, { "name": "kB__param__a9", "type": "int" }, { "name": "kB__param__a29", "type": "int" }, { "name": "kB__param__a10", "type": "int" }, { "name": "kB__param__a30", "type": "int" }, { "name": "kB__param__a11", "type": "int" }, { "name": "kB__param__a31", "type": "int" }, { "name": "kB__param__a12", "type": "int" }, { "name": "kB__param__a32", "type": "int" }, { "name": "kB__param__a13", "type": "int" }, { "name": "kB__param__a33", "type": "int" }, { "name": "kB__param__a14", "type": "int" }, { "name": "kB__param__a34", "type": "int" }, { "name": "kB__param__a15", "type": "int" }, { "name": "kB__param__a35", "type": "int" }, { "name": "kB__param__a16", "type": "int" }, { "name": "kB__param__a36", "type": "int" }, { "name": "kB__param__a17", "type": "int" }, { "name": "kB__param__a37", "type": "int" }, { "name": "kB__param__a18", "type": "int" }, { "name": "kB__param__a38", "type": "int" }, { "name": "kB__param__a19", "type": "int" }, { "name": "kB__param__a39", "type": "int" } ], "type": "bool" } ], "jani-version": 1, "name": "model", "properties": [ { "expression": { "fun": "values", "op": "filter", "states": { "op": "initial" }, "values": { "exp": { "left": true, "op": "U", "right": { "left": { "exp": "knowA", "op": "¬" }, "op": "∧", "right": "knowB" } }, "op": "Pmin" } }, "name": "unfairA" } ], "restrict-initial": { "exp": true }, "system": { "elements": [ { "automaton": "counter" }, { "automaton": "partyA" }, { "automaton": "partyB" } ], "syncs": [ { "result": "receiveA", "synchronise": [ "receiveA", "receiveA", null ] }, { "result": "receiveB", "synchronise": [ "receiveB", null, "receiveB" ] } ] }, "type": "dtmc", "variables": [ { "initial-value": false, "name": "knowB", "transient": true, "type": "bool" }, { "initial-value": false, "name": "knowA", "transient": true, "type": "bool" }, { "initial-value": 0, "name": "n", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 9 } }, { "initial-value": 1, "name": "phase", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 5 } }, { "initial-value": 0, "name": "b0", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b20", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b21", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b2", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b22", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b3", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b23", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b4", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b24", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b5", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b25", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b6", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b26", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b7", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b27", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b8", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b28", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b9", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b29", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b10", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b30", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b11", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b31", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b12", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b32", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b13", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b33", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b14", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b34", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b15", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b35", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b16", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b36", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b17", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b37", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b18", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b38", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b19", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "b39", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a0", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a20", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a21", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a2", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a22", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a3", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a23", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a4", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a24", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a5", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a25", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a6", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a26", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a7", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a27", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a8", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a28", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a9", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a29", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a10", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a30", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a11", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a31", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a12", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a32", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a13", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a33", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a14", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a34", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a15", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a35", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a16", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a36", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a17", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a37", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a18", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a38", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a19", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "a39", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } } ] }