{ "actions": [ { "name": "reply" }, { "name": "time" } ], "automata": [ { "edges": [ { "destinations": [ { "assignments": [ { "comment": "receiver <- 1", "ref": "receiver", "value": 1 }, { "comment": "freq1 <- f1", "ref": "freq1", "value": "f1" }, { "comment": "train1 <- t1", "ref": "train1", "value": "t1" } ], "location": "l" } ], "guard": { "comment": "(((receiver = 0) & (y1 = 0)) & success)", "exp": { "left": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 0 } }, "op": "∧", "right": { "args": [], "function": "success", "op": "call" } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "y1 <- 1", "ref": "y1", "value": 1 }, { "comment": "receiver <- 0", "ref": "receiver", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(((receiver = 0) & (y1 = 0)) & !(success))", "exp": { "left": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 0 } }, "op": "∧", "right": { "exp": { "args": [], "function": "success", "op": "call" }, "op": "¬" } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "y1 <- 2", "ref": "y1", "value": 2 }, { "comment": "receiver <- 2", "ref": "receiver", "value": 2 }, { "comment": "freq1 <- 0", "ref": "freq1", "value": 0 }, { "comment": "train1 <- 0", "ref": "train1", "value": 0 } ], "location": "l" } ], "guard": { "comment": "((receiver = 1) & hear)", "exp": { "left": { "left": "receiver", "op": "=", "right": 1 }, "op": "∧", "right": { "args": [], "function": "hear", "op": "call" } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "receiver <- 1", "ref": "receiver", "value": 1 }, { "comment": "freq1 <- f1", "ref": "freq1", "value": "f1" }, { "comment": "train1 <- t1", "ref": "train1", "value": "t1" } ], "location": "l" } ], "guard": { "comment": "(((receiver = 3) & (y1 = 0)) & success)", "exp": { "left": { "left": { "left": "receiver", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 0 } }, "op": "∧", "right": { "args": [], "function": "success", "op": "call" } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "y1 <- 1", "ref": "y1", "value": 1 }, { "comment": "receiver <- 0", "ref": "receiver", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(((receiver = 3) & (y1 = 0)) & !(success))", "exp": { "left": { "left": { "left": "receiver", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 0 } }, "op": "∧", "right": { "exp": { "args": [], "function": "success", "op": "call" }, "op": "¬" } } }, "location": "l" }, { "action": "reply", "destinations": [ { "assignments": [ { "comment": "y1 <- 0", "ref": "y1", "value": 0 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 2", "ref": "y1", "value": 2 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 4", "ref": "y1", "value": 4 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 6", "ref": "y1", "value": 6 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 8", "ref": "y1", "value": 8 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 10", "ref": "y1", "value": 10 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 12", "ref": "y1", "value": 12 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 14", "ref": "y1", "value": 14 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 16", "ref": "y1", "value": 16 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 18", "ref": "y1", "value": 18 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 20", "ref": "y1", "value": 20 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 22", "ref": "y1", "value": 22 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 24", "ref": "y1", "value": 24 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 26", "ref": "y1", "value": 26 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 28", "ref": "y1", "value": 28 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 30", "ref": "y1", "value": 30 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 32", "ref": "y1", "value": 32 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 34", "ref": "y1", "value": 34 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 36", "ref": "y1", "value": 36 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 38", "ref": "y1", "value": 38 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 40", "ref": "y1", "value": 40 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 42", "ref": "y1", "value": 42 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 44", "ref": "y1", "value": 44 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 46", "ref": "y1", "value": 46 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 48", "ref": "y1", "value": 48 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 50", "ref": "y1", "value": 50 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 52", "ref": "y1", "value": 52 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 54", "ref": "y1", "value": 54 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 56", "ref": "y1", "value": 56 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 58", "ref": "y1", "value": 58 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 60", "ref": "y1", "value": 60 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 62", "ref": "y1", "value": 62 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 64", "ref": "y1", "value": 64 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 66", "ref": "y1", "value": 66 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 68", "ref": "y1", "value": 68 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 70", "ref": "y1", "value": 70 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 72", "ref": "y1", "value": 72 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 74", "ref": "y1", "value": 74 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 76", "ref": "y1", "value": 76 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 78", "ref": "y1", "value": 78 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 80", "ref": "y1", "value": 80 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 82", "ref": "y1", "value": 82 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 84", "ref": "y1", "value": 84 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 86", "ref": "y1", "value": 86 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 88", "ref": "y1", "value": 88 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 90", "ref": "y1", "value": 90 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 92", "ref": "y1", "value": 92 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 94", "ref": "y1", "value": 94 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 96", "ref": "y1", "value": 96 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 98", "ref": "y1", "value": 98 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 100", "ref": "y1", "value": 100 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 102", "ref": "y1", "value": 102 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 104", "ref": "y1", "value": 104 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 106", "ref": "y1", "value": 106 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 108", "ref": "y1", "value": 108 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 110", "ref": "y1", "value": 110 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 112", "ref": "y1", "value": 112 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 114", "ref": "y1", "value": 114 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 116", "ref": "y1", "value": 116 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 118", "ref": "y1", "value": 118 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 120", "ref": "y1", "value": 120 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 122", "ref": "y1", "value": 122 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 124", "ref": "y1", "value": 124 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 126", "ref": "y1", "value": 126 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 128", "ref": "y1", "value": 128 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 130", "ref": "y1", "value": 130 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 132", "ref": "y1", "value": 132 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 134", "ref": "y1", "value": 134 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 136", "ref": "y1", "value": 136 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 138", "ref": "y1", "value": 138 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 140", "ref": "y1", "value": 140 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 142", "ref": "y1", "value": 142 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 144", "ref": "y1", "value": 144 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 146", "ref": "y1", "value": 146 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 148", "ref": "y1", "value": 148 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 150", "ref": "y1", "value": 150 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 152", "ref": "y1", "value": 152 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 154", "ref": "y1", "value": 154 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 156", "ref": "y1", "value": 156 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 158", "ref": "y1", "value": 158 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 160", "ref": "y1", "value": 160 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 162", "ref": "y1", "value": 162 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 164", "ref": "y1", "value": 164 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 166", "ref": "y1", "value": 166 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 168", "ref": "y1", "value": 168 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 170", "ref": "y1", "value": 170 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 172", "ref": "y1", "value": 172 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 174", "ref": "y1", "value": 174 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 176", "ref": "y1", "value": 176 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 178", "ref": "y1", "value": 178 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 180", "ref": "y1", "value": 180 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 182", "ref": "y1", "value": 182 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 184", "ref": "y1", "value": 184 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 186", "ref": "y1", "value": 186 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 188", "ref": "y1", "value": 188 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 190", "ref": "y1", "value": 190 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 192", "ref": "y1", "value": 192 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 194", "ref": "y1", "value": 194 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 196", "ref": "y1", "value": 196 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 198", "ref": "y1", "value": 198 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 200", "ref": "y1", "value": 200 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 202", "ref": "y1", "value": 202 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 204", "ref": "y1", "value": 204 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 206", "ref": "y1", "value": 206 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 208", "ref": "y1", "value": 208 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 210", "ref": "y1", "value": 210 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 212", "ref": "y1", "value": 212 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 214", "ref": "y1", "value": 214 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 216", "ref": "y1", "value": 216 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 218", "ref": "y1", "value": 218 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 220", "ref": "y1", "value": 220 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 222", "ref": "y1", "value": 222 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 224", "ref": "y1", "value": 224 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 226", "ref": "y1", "value": 226 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 228", "ref": "y1", "value": 228 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 230", "ref": "y1", "value": 230 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 232", "ref": "y1", "value": 232 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 234", "ref": "y1", "value": 234 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 236", "ref": "y1", "value": 236 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 238", "ref": "y1", "value": 238 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 240", "ref": "y1", "value": 240 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 242", "ref": "y1", "value": 242 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 244", "ref": "y1", "value": 244 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 246", "ref": "y1", "value": 246 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 248", "ref": "y1", "value": 248 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 250", "ref": "y1", "value": 250 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 252", "ref": "y1", "value": 252 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } }, { "assignments": [ { "comment": "y1 <- 254", "ref": "y1", "value": 254 }, { "comment": "receiver <- 3", "ref": "receiver", "value": 3 } ], "location": "l", "probability": { "comment": "(1 / (127 + 1))", "exp": { "left": 1, "op": "/", "right": 128 } } } ], "guard": { "comment": "((receiver = 2) & (y1 = 0))", "exp": { "left": { "left": "receiver", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 0 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "y1 <- (y1 - 1)", "ref": "y1", "value": { "left": "y1", "op": "-", "right": 1 } }, { "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))", "ref": "time", "value": { "left": { "else": 0.0, "if": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 1 } }, "op": "ite", "then": 2048 }, "op": "+", "right": { "else": 0.0, "if": { "left": "receiver", "op": ">", "right": 0 }, "op": "ite", "then": 1 } } } ], "location": "l" } ], "guard": { "comment": "((receiver = 0) & (y1 = 1))", "exp": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 1 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "y1 <- y1", "ref": "y1", "value": "y1" }, { "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))", "ref": "time", "value": { "left": { "else": 0.0, "if": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 1 } }, "op": "ite", "then": 2048 }, "op": "+", "right": { "else": 0.0, "if": { "left": "receiver", "op": ">", "right": 0 }, "op": "ite", "then": 1 } } } ], "location": "l" } ], "guard": { "comment": "((receiver = 1) & !(hear))", "exp": { "left": { "left": "receiver", "op": "=", "right": 1 }, "op": "∧", "right": { "exp": { "args": [], "function": "hear", "op": "call" }, "op": "¬" } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "y1 <- (y1 - 1)", "ref": "y1", "value": { "left": "y1", "op": "-", "right": 1 } }, { "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))", "ref": "time", "value": { "left": { "else": 0.0, "if": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 1 } }, "op": "ite", "then": 2048 }, "op": "+", "right": { "else": 0.0, "if": { "left": "receiver", "op": ">", "right": 0 }, "op": "ite", "then": 1 } } } ], "location": "l" } ], "guard": { "comment": "((receiver = 2) & (y1 > 0))", "exp": { "left": { "left": "receiver", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "y1", "op": ">", "right": 0 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "y1 <- (y1 - 1)", "ref": "y1", "value": { "left": "y1", "op": "-", "right": 1 } }, { "comment": "time <- ((((receiver = 0) & (y1 = 1)) ? 2048 : 0) + ((receiver > 0) ? 1 : 0))", "ref": "time", "value": { "left": { "else": 0.0, "if": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 1 } }, "op": "ite", "then": 2048 }, "op": "+", "right": { "else": 0.0, "if": { "left": "receiver", "op": ">", "right": 0 }, "op": "ite", "then": 1 } } } ], "location": "l" } ], "guard": { "comment": "((receiver = 3) & (y1 > 0))", "exp": { "left": { "left": "receiver", "op": "=", "right": 3 }, "op": "∧", "right": { "left": "y1", "op": ">", "right": 0 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l", "transient-values": [ { "comment": "target <- (rec = 1)", "ref": "target", "value": { "left": "rec", "op": "=", "right": 1 } } ] } ], "name": "receiver1", "variables": [] }, { "edges": [ { "action": "reply", "destinations": [ { "assignments": [ { "comment": "f1 <- ((f1 < 16) ? (f1 + 1) : 1)", "ref": "f1", "value": { "else": 1, "if": { "left": "f1", "op": "<", "right": 16 }, "op": "ite", "then": { "left": "f1", "op": "+", "right": 1 } } }, { "comment": "t1 <- ((f1 < 16) ? t1 : (1 - t1))", "ref": "t1", "value": { "else": { "left": 1, "op": "-", "right": "t1" }, "if": { "left": "f1", "op": "<", "right": 16 }, "op": "ite", "then": "t1" } } ], "location": "l" } ], "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "z1 <- (z1 + 1)", "ref": "z1", "value": { "left": "z1", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "(!(sleep) & (z1 < 4096))", "exp": { "left": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" }, "op": "∧", "right": { "left": "z1", "op": "<", "right": 4096 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "z1 <- 1", "ref": "z1", "value": 1 }, { "comment": "f1 <- (f1 + 1)", "ref": "f1", "value": { "left": "f1", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "((!(sleep) & (z1 = 4096)) & (f1 < 16))", "exp": { "left": { "left": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" }, "op": "∧", "right": { "left": "z1", "op": "=", "right": 4096 } }, "op": "∧", "right": { "left": "f1", "op": "<", "right": 16 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "z1 <- 1", "ref": "z1", "value": 1 }, { "comment": "f1 <- 1", "ref": "f1", "value": 1 }, { "comment": "t1 <- (1 - t1)", "ref": "t1", "value": { "left": 1, "op": "-", "right": "t1" } } ], "location": "l" } ], "guard": { "comment": "((!(sleep) & (z1 = 4096)) & (f1 = 16))", "exp": { "left": { "left": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" }, "op": "∧", "right": { "left": "z1", "op": "=", "right": 4096 } }, "op": "∧", "right": { "left": "f1", "op": "=", "right": 16 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "z1 <- (z1 + 2048)", "ref": "z1", "value": { "left": "z1", "op": "+", "right": 2048 } } ], "location": "l" } ], "guard": { "comment": "(sleep & (z1 <= 2048))", "exp": { "left": { "args": [], "function": "sleep", "op": "call" }, "op": "∧", "right": { "left": "z1", "op": "≤", "right": 2048 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "z1 <- (z1 - 2048)", "ref": "z1", "value": { "left": "z1", "op": "-", "right": 2048 } }, { "comment": "f1 <- (f1 + 1)", "ref": "f1", "value": { "left": "f1", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "((sleep & (z1 > 2048)) & (f1 < 16))", "exp": { "left": { "left": { "args": [], "function": "sleep", "op": "call" }, "op": "∧", "right": { "left": "z1", "op": ">", "right": 2048 } }, "op": "∧", "right": { "left": "f1", "op": "<", "right": 16 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "z1 <- (z1 - 2048)", "ref": "z1", "value": { "left": "z1", "op": "-", "right": 2048 } }, { "comment": "f1 <- 1", "ref": "f1", "value": 1 }, { "comment": "t1 <- (1 - t1)", "ref": "t1", "value": { "left": 1, "op": "-", "right": "t1" } } ], "location": "l" } ], "guard": { "comment": "((sleep & (z1 > 2048)) & (f1 = 16))", "exp": { "left": { "left": { "args": [], "function": "sleep", "op": "call" }, "op": "∧", "right": { "left": "z1", "op": ">", "right": 2048 } }, "op": "∧", "right": { "left": "f1", "op": "=", "right": 16 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "frequency1", "variables": [ { "name": "z1", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 4096 } } ] }, { "edges": [ { "action": "time", "destinations": [ { "assignments": [ { "comment": "freq <- (freq + 1)", "ref": "freq", "value": { "left": "freq", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "(((!(sleep) & (send = 1)) & ((((((((freq = 1) | (freq = 3)) | (freq = 5)) | (freq = 7)) | (freq = 9)) | (freq = 11)) | (freq = 13)) | (freq = 15))) & (freq != c))", "exp": { "left": { "left": { "left": "freq", "op": "≠", "right": "c" }, "op": "∧", "right": { "left": "send", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": { "left": { "left": { "left": { "left": "freq", "op": "=", "right": 15 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 3 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 9 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 7 } } }, "op": "∨", "right": { "left": { "left": { "left": "freq", "op": "=", "right": 13 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 1 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 11 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 5 } } } }, "op": "∧", "right": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "freq <- (freq + 1)", "ref": "freq", "value": { "left": "freq", "op": "+", "right": 1 } }, { "comment": "train <- (1 - train)", "ref": "train", "value": { "left": 1, "op": "-", "right": "train" } } ], "location": "l" } ], "guard": { "comment": "(((!(sleep) & (send = 1)) & ((((((((freq = 1) | (freq = 3)) | (freq = 5)) | (freq = 7)) | (freq = 9)) | (freq = 11)) | (freq = 13)) | (freq = 15))) & (freq = c))", "exp": { "left": { "left": { "left": "freq", "op": "=", "right": "c" }, "op": "∧", "right": { "left": "send", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": { "left": { "left": { "left": { "left": "freq", "op": "=", "right": 15 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 3 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 9 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 7 } } }, "op": "∨", "right": { "left": { "left": { "left": "freq", "op": "=", "right": 13 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 1 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 11 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 5 } } } }, "op": "∧", "right": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "send <- 2", "ref": "send", "value": 2 } ], "location": "l" } ], "guard": { "comment": "((!(sleep) & (send = 1)) & ((((((((freq = 2) | (freq = 4)) | (freq = 6)) | (freq = 8)) | (freq = 10)) | (freq = 12)) | (freq = 14)) | (freq = 16)))", "exp": { "left": { "left": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" }, "op": "∧", "right": { "left": "send", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": { "left": { "left": { "left": "freq", "op": "=", "right": 16 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 4 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 10 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "freq", "op": "=", "right": 14 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 2 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 12 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 6 } } } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "send <- 3", "ref": "send", "value": 3 } ], "location": "l" } ], "guard": { "comment": "(!(sleep) & (send = 2))", "exp": { "left": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" }, "op": "∧", "right": { "left": "send", "op": "=", "right": 2 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "send <- 1", "ref": "send", "value": 1 }, { "comment": "freq <- (freq + 1)", "ref": "freq", "value": { "left": "freq", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "(((!(sleep) & (send = 3)) & (freq < 16)) & (freq != c))", "exp": { "left": { "left": { "left": "freq", "op": "≠", "right": "c" }, "op": "∧", "right": { "left": "send", "op": "=", "right": 3 } }, "op": "∧", "right": { "left": { "left": "freq", "op": "<", "right": 16 }, "op": "∧", "right": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "send <- 1", "ref": "send", "value": 1 }, { "comment": "freq <- (freq + 1)", "ref": "freq", "value": { "left": "freq", "op": "+", "right": 1 } }, { "comment": "train <- (1 - train)", "ref": "train", "value": { "left": 1, "op": "-", "right": "train" } } ], "location": "l" } ], "guard": { "comment": "(((!(sleep) & (send = 3)) & (freq < 16)) & (freq = c))", "exp": { "left": { "left": { "left": "freq", "op": "=", "right": "c" }, "op": "∧", "right": { "left": "send", "op": "=", "right": 3 } }, "op": "∧", "right": { "left": { "left": "freq", "op": "<", "right": 16 }, "op": "∧", "right": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "send <- 1", "ref": "send", "value": 1 }, { "comment": "freq <- 1", "ref": "freq", "value": 1 }, { "comment": "train <- (1 - train)", "ref": "train", "value": { "left": 1, "op": "-", "right": "train" } }, { "comment": "rep <- (rep + 1)", "ref": "rep", "value": { "left": "rep", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "((((!(sleep) & (send = 3)) & (freq = 16)) & (rep < 128)) & (c != 16))", "exp": { "left": { "left": { "left": { "left": "c", "op": "≠", "right": 16 }, "op": "∧", "right": { "left": "send", "op": "=", "right": 3 } }, "op": "∧", "right": { "left": "freq", "op": "=", "right": 16 } }, "op": "∧", "right": { "left": { "left": "rep", "op": "<", "right": 128 }, "op": "∧", "right": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "send <- 1", "ref": "send", "value": 1 }, { "comment": "freq <- 1", "ref": "freq", "value": 1 }, { "comment": "rep <- (rep + 1)", "ref": "rep", "value": { "left": "rep", "op": "+", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "((((!(sleep) & (send = 3)) & (freq = 16)) & (rep < 128)) & (c = 16))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 16 }, "op": "∧", "right": { "left": "send", "op": "=", "right": 3 } }, "op": "∧", "right": { "left": "freq", "op": "=", "right": 16 } }, "op": "∧", "right": { "left": { "left": "rep", "op": "<", "right": 128 }, "op": "∧", "right": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "send <- 1", "ref": "send", "value": 1 }, { "comment": "freq <- 1", "ref": "freq", "value": 1 }, { "comment": "train <- (swap ? (1 - train) : train)", "ref": "train", "value": { "else": "train", "if": { "args": [], "function": "swap", "op": "call" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, { "comment": "c <- ((c = 16) ? 1 : (c + 1))", "ref": "c", "value": { "else": { "left": "c", "op": "+", "right": 1 }, "if": { "left": "c", "op": "=", "right": 16 }, "op": "ite", "then": 1 } }, { "comment": "rep <- 1", "ref": "rep", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(((!(sleep) & (send = 3)) & (freq = 16)) & (rep = 128))", "exp": { "left": { "left": { "left": "rep", "op": "=", "right": 128 }, "op": "∧", "right": { "left": "send", "op": "=", "right": 3 } }, "op": "∧", "right": { "left": { "left": "freq", "op": "=", "right": 16 }, "op": "∧", "right": { "exp": { "args": [], "function": "sleep", "op": "call" }, "op": "¬" } } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "rep <- (rep + 64)", "ref": "rep", "value": { "left": "rep", "op": "+", "right": 64 } } ], "location": "l" } ], "guard": { "comment": "(sleep & (rep <= 64))", "exp": { "left": { "args": [], "function": "sleep", "op": "call" }, "op": "∧", "right": { "left": "rep", "op": "≤", "right": 64 } } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "train <- (swap2 ? (1 - train) : train)", "ref": "train", "value": { "else": "train", "if": { "args": [], "function": "swap2", "op": "call" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, { "comment": "c <- ((c = 16) ? 1 : (c + 1))", "ref": "c", "value": { "else": { "left": "c", "op": "+", "right": 1 }, "if": { "left": "c", "op": "=", "right": 16 }, "op": "ite", "then": 1 } }, { "comment": "rep <- (rep - 64)", "ref": "rep", "value": { "left": "rep", "op": "-", "right": 64 } } ], "location": "l" } ], "guard": { "comment": "(sleep & (rep > 64))", "exp": { "left": { "args": [], "function": "sleep", "op": "call" }, "op": "∧", "right": { "left": "rep", "op": ">", "right": 64 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "sender_frequency", "variables": [] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "rec <- rec", "ref": "rec", "value": "rec" } ], "location": "l" } ], "guard": { "comment": "(rec = 1)", "exp": { "left": "rec", "op": "=", "right": 1 } }, "location": "l" }, { "action": "reply", "destinations": [ { "assignments": [ { "comment": "rec <- (min((rec + 1), 1))", "ref": "rec", "value": { "left": { "left": "rec", "op": "+", "right": 1 }, "op": "min", "right": 1 } } ], "location": "l" } ], "guard": { "comment": "(rec < 1)", "exp": { "left": "rec", "op": "<", "right": 1 } }, "location": "l" }, { "action": "time", "destinations": [ { "assignments": [ { "comment": "rec <- rec", "ref": "rec", "value": "rec" } ], "location": "l" } ], "guard": { "comment": "(rec < 1)", "exp": { "left": "rec", "op": "<", "right": 1 } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "replies", "variables": [] } ], "constants": [ { "name": "phase", "type": "int", "value": 4096 }, { "name": "maxr", "type": "int", "value": 127 }, { "name": "mrep", "type": "int", "value": 128 }, { "name": "mrec", "type": "int", "value": 1 }, { "name": "k", "type": "int", "value": 1 }, { "name": "T", "type": "int", "value": 0 } ], "features": [ "derived-operators", "functions" ], "functions": [ { "body": { "left": { "left": "receiver", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 1 } }, "name": "sleep", "parameters": [], "type": "bool" }, { "body": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 16 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 4 } }, "op": "∨", "right": { "left": { "left": "c", "op": "=", "right": 10 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 8 } } }, "op": "∨", "right": { "left": { "left": { "left": "c", "op": "=", "right": 14 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 2 } }, "op": "∨", "right": { "left": { "left": "c", "op": "=", "right": 12 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 6 } } } }, "name": "swap", "parameters": [], "type": "bool" }, { "body": { "left": { "left": { "left": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 16 }, "op": "∧", "right": { "left": "c", "op": "=", "right": 16 } }, "op": "∧", "right": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "f1", "op": "=", "right": 1 }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } } }, "op": "∧", "right": { "left": { "left": "f1", "op": "≤", "right": { "left": "freq", "op": "+", "right": 2 } }, "op": "∧", "right": { "left": "rep", "op": "=", "right": 128 } } }, "op": "∨", "right": { "left": { "left": { "left": "rep", "op": "=", "right": 128 }, "op": "∧", "right": { "left": { "left": { "left": "send", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "freq", "op": "≤", "right": "f1" } }, "op": "∨", "right": { "left": { "left": "send", "op": ">", "right": 1 }, "op": "∧", "right": { "left": "freq", "op": "<", "right": "f1" } } } }, "op": "∧", "right": { "left": { "left": { "left": "t1", "op": "=", "right": { "else": { "left": 1, "op": "-", "right": "train" }, "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": "train" } }, "op": "∧", "right": { "left": "f1", "op": "≤", "right": "c" } }, "op": "∨", "right": { "left": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, "op": "∧", "right": { "left": "f1", "op": ">", "right": "c" } } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": { "left": "f1", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "freq", "op": "≥", "right": 15 } }, "op": "∨", "right": { "left": { "left": "f1", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "freq", "op": "=", "right": 16 } } }, "op": "∧", "right": { "left": "c", "op": "=", "right": 16 } }, "op": "∧", "right": { "left": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "f1", "op": "=", "right": 1 }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, "op": "∧", "right": { "left": "rep", "op": "=", "right": 127 } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": { "left": "f1", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "freq", "op": "≥", "right": 15 } }, "op": "∨", "right": { "left": { "left": "f1", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "freq", "op": "=", "right": 16 } } }, "op": "∧", "right": { "left": "c", "op": "<", "right": 16 } }, "op": "∧", "right": { "exp": { "args": [], "function": "swap", "op": "call" }, "op": "¬" } }, "op": "∧", "right": { "left": { "left": { "left": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, "op": "∧", "right": { "left": "f1", "op": "≤", "right": { "left": "c", "op": "+", "right": 1 } } }, "op": "∨", "right": { "left": { "left": "t1", "op": "=", "right": { "else": { "left": 1, "op": "-", "right": "train" }, "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": "train" } }, "op": "∧", "right": { "left": "f1", "op": ">", "right": { "left": "c", "op": "+", "right": 1 } } } }, "op": "∧", "right": { "left": "rep", "op": "=", "right": 127 } } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": { "left": "f1", "op": "≤", "right": { "left": "freq", "op": "+", "right": 2 } }, "op": "∧", "right": { "left": "c", "op": "<", "right": 16 } }, "op": "∧", "right": { "exp": { "args": [], "function": "swap", "op": "call" }, "op": "¬" } }, "op": "∧", "right": { "left": { "left": { "left": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, "op": "∧", "right": { "left": "f1", "op": "≤", "right": { "left": "c", "op": "+", "right": 1 } } }, "op": "∨", "right": { "left": { "left": "t1", "op": "=", "right": { "else": { "left": 1, "op": "-", "right": "train" }, "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": "train" } }, "op": "∧", "right": { "left": "f1", "op": ">", "right": { "left": "c", "op": "+", "right": 1 } } } }, "op": "∧", "right": { "left": "rep", "op": "=", "right": 128 } } }, "op": "∨", "right": { "left": { "left": "rep", "op": "<", "right": 128 }, "op": "∧", "right": { "left": { "left": { "left": "t1", "op": "=", "right": { "else": { "left": 1, "op": "-", "right": "train" }, "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": "train" } }, "op": "∧", "right": { "left": "f1", "op": "≤", "right": "c" } }, "op": "∨", "right": { "left": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, "op": "∧", "right": { "left": "f1", "op": ">", "right": "c" } } } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": "f1", "op": "≤", "right": { "left": "freq", "op": "+", "right": 2 } }, "op": "∧", "right": { "left": "c", "op": "<", "right": 16 } }, "op": "∧", "right": { "args": [], "function": "swap", "op": "call" } }, "op": "∧", "right": { "left": { "left": { "left": { "left": "t1", "op": "=", "right": { "else": { "left": 1, "op": "-", "right": "train" }, "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": "train" } }, "op": "∧", "right": { "left": "f1", "op": "≤", "right": { "left": "c", "op": "+", "right": 1 } } }, "op": "∨", "right": { "left": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, "op": "∧", "right": { "left": "f1", "op": ">", "right": { "left": "c", "op": "+", "right": 1 } } } }, "op": "∧", "right": { "left": "rep", "op": "=", "right": 128 } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": { "left": "f1", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "freq", "op": "≥", "right": 15 } }, "op": "∨", "right": { "left": { "left": "f1", "op": "=", "right": 2 }, "op": "∧", "right": { "left": "freq", "op": "=", "right": 16 } } }, "op": "∧", "right": { "left": "c", "op": "<", "right": 16 } }, "op": "∧", "right": { "args": [], "function": "swap", "op": "call" } }, "op": "∧", "right": { "left": { "left": { "left": { "left": "t1", "op": "=", "right": { "else": { "left": 1, "op": "-", "right": "train" }, "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": "train" } }, "op": "∧", "right": { "left": "f1", "op": "≤", "right": { "left": "c", "op": "+", "right": 1 } } }, "op": "∨", "right": { "left": { "left": "t1", "op": "=", "right": { "else": "train", "if": { "left": "freq", "op": "≤", "right": "c" }, "op": "ite", "then": { "left": 1, "op": "-", "right": "train" } } }, "op": "∧", "right": { "left": "f1", "op": ">", "right": { "left": "c", "op": "+", "right": 1 } } } }, "op": "∧", "right": { "left": "rep", "op": "=", "right": 127 } } } } } }, "name": "success", "parameters": [], "type": "bool" }, { "body": { "left": { "left": { "left": "freq1", "op": "=", "right": "freq" }, "op": "∧", "right": { "left": "train1", "op": "=", "right": "train" } }, "op": "∧", "right": { "left": "send", "op": "=", "right": 1 } }, "name": "hear", "parameters": [], "type": "bool" }, { "body": { "left": { "left": { "left": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 14 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 4 } }, "op": "∨", "right": { "left": "c", "op": "=", "right": 8 } }, "op": "∨", "right": { "left": { "left": { "left": "c", "op": "=", "right": 12 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 2 } }, "op": "∨", "right": { "left": { "left": "c", "op": "=", "right": 10 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 6 } } } }, "op": "∧", "right": { "left": "freq", "op": "=", "right": { "left": "c", "op": "+", "right": 1 } } }, "op": "∨", "right": { "left": { "left": "c", "op": "=", "right": 16 }, "op": "∧", "right": { "left": "freq", "op": "=", "right": 1 } } }, "op": "∨", "right": { "left": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 15 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 3 } }, "op": "∨", "right": { "left": { "left": "c", "op": "=", "right": 9 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 7 } } }, "op": "∨", "right": { "left": { "left": { "left": "c", "op": "=", "right": 13 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 1 } }, "op": "∨", "right": { "left": { "left": "c", "op": "=", "right": 11 }, "op": "∨", "right": { "left": "c", "op": "=", "right": 5 } } } }, "op": "∧", "right": { "left": "freq", "op": "≠", "right": { "left": "c", "op": "+", "right": 1 } } } }, "name": "swap2", "parameters": [], "type": "bool" } ], "jani-version": 1, "name": "model", "properties": [ { "expression": { "fun": "max", "op": "filter", "states": { "op": "initial" }, "values": { "accumulate": [ "steps" ], "exp": "time", "op": "Emin", "reach": "target" } }, "name": "time" } ], "restrict-initial": { "exp": { "left": { "left": { "left": { "left": { "left": { "left": { "left": { "left": "send", "op": "=", "right": 1 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 4 } }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 10 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 14 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 6 } } }, "op": "∨", "right": { "left": { "left": { "left": "freq", "op": "=", "right": 16 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 2 } }, "op": "∨", "right": { "left": { "left": "freq", "op": "=", "right": 12 }, "op": "∨", "right": { "left": "freq", "op": "=", "right": 8 } } } }, "op": "∧", "right": { "left": "y1", "op": "=", "right": 0 } }, "op": "∧", "right": { "left": { "left": "rec", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "train1", "op": "=", "right": 0 } } }, "op": "∧", "right": { "left": { "left": { "left": "t1", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "receiver", "op": "=", "right": 0 } }, "op": "∧", "right": { "left": { "left": "f1", "op": "=", "right": 1 }, "op": "∧", "right": { "left": "freq1", "op": "=", "right": 0 } } } } }, "system": { "elements": [ { "automaton": "receiver1" }, { "automaton": "frequency1" }, { "automaton": "sender_frequency" }, { "automaton": "replies" } ], "syncs": [ { "result": "reply", "synchronise": [ "reply", "reply", null, "reply" ] }, { "result": "time", "synchronise": [ "time", "time", "time", "time" ] } ] }, "type": "dtmc", "variables": [ { "initial-value": false, "name": "target", "transient": true, "type": "bool" }, { "initial-value": 0.0, "name": "time", "transient": true, "type": "real" }, { "name": "y1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 255 } }, { "name": "receiver", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 3 } }, { "name": "freq1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 16 } }, { "name": "train1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "name": "f1", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 16 } }, { "name": "t1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "name": "send", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 3 } }, { "name": "freq", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 16 } }, { "name": "train", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "name": "c", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 16 } }, { "name": "rep", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 128 } }, { "name": "rec", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } } ] }