{ "actions": [], "automata": [ { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p1 <- 1", "ref": "p1", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p1 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p1", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw1 <- 1", "ref": "draw1", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & draw(p1, b1, r1)) & (draw1 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p1", "b1", "r1" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw1", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b1 <- 1", "ref": "b1", "value": 1 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b1 <- 2", "ref": "b1", "value": 2 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b1 <- 3", "ref": "b1", "value": 3 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b1 <- 4", "ref": "b1", "value": 4 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b1 <- 5", "ref": "b1", "value": 5 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b1 <- 6", "ref": "b1", "value": 6 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b1 <- 7", "ref": "b1", "value": 7 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b1 <- 8", "ref": "b1", "value": 8 }, { "comment": "r1 <- r", "ref": "r1", "value": "r" }, { "comment": "draw1 <- 0", "ref": "draw1", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw1 = 1)", "exp": { "left": "draw1", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p1 <- 2", "ref": "p1", "value": 2 }, { "comment": "b1 <- 0", "ref": "b1", "value": 0 }, { "comment": "r1 <- 0", "ref": "r1", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p1 <- 2", "ref": "p1", "value": 2 }, { "comment": "b1 <- 0", "ref": "b1", "value": 0 }, { "comment": "r1 <- 0", "ref": "r1", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p1 = 1)) & (b = b1)) & (r = r1)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p1", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b1" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r1" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p1 <- 0", "ref": "p1", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p1 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p1", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l", "transient-values": [ { "comment": "target <- ((((((((((p1 = 2) | (p2 = 2)) | (p3 = 2)) | (p4 = 2)) | (p5 = 2)) | (p6 = 2)) | (p7 = 2)) | (p8 = 2)) | (p9 = 2)) | (p10 = 2))", "ref": "target", "value": { "left": { "left": { "left": { "left": { "left": "p10", "op": "=", "right": 2 }, "op": "∨", "right": { "left": "p2", "op": "=", "right": 2 } }, "op": "∨", "right": { "left": { "left": "p6", "op": "=", "right": 2 }, "op": "∨", "right": { "left": "p5", "op": "=", "right": 2 } } }, "op": "∨", "right": { "left": { "left": "p8", "op": "=", "right": 2 }, "op": "∨", "right": { "left": "p3", "op": "=", "right": 2 } } }, "op": "∨", "right": { "left": { "left": { "left": "p9", "op": "=", "right": 2 }, "op": "∨", "right": { "left": "p1", "op": "=", "right": 2 } }, "op": "∨", "right": { "left": { "left": "p7", "op": "=", "right": 2 }, "op": "∨", "right": { "left": "p4", "op": "=", "right": 2 } } } } } ] } ], "name": "process1", "variables": [ { "initial-value": 0, "name": "b1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p2 <- 1", "ref": "p2", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw1, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p2 = 0))", "exp": { "left": { "args": [ "draw1", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p2", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw2 <- 1", "ref": "draw2", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw1, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & draw(p2, b2, r2)) & (draw2 = 0))", "exp": { "left": { "left": { "args": [ "draw1", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p2", "b2", "r2" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw2", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b2 <- 1", "ref": "b2", "value": 1 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b2 <- 2", "ref": "b2", "value": 2 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b2 <- 3", "ref": "b2", "value": 3 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b2 <- 4", "ref": "b2", "value": 4 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b2 <- 5", "ref": "b2", "value": 5 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b2 <- 6", "ref": "b2", "value": 6 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b2 <- 7", "ref": "b2", "value": 7 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b2 <- 8", "ref": "b2", "value": 8 }, { "comment": "r2 <- r", "ref": "r2", "value": "r" }, { "comment": "draw2 <- 0", "ref": "draw2", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw2 = 1)", "exp": { "left": "draw2", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p2 <- 2", "ref": "p2", "value": 2 }, { "comment": "b2 <- 0", "ref": "b2", "value": 0 }, { "comment": "r2 <- 0", "ref": "r2", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p2 <- 2", "ref": "p2", "value": 2 }, { "comment": "b2 <- 0", "ref": "b2", "value": 0 }, { "comment": "r2 <- 0", "ref": "r2", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw1, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p2 = 1)) & (b = b2)) & (r = r2)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p2", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b2" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r2" }, "op": "∧", "right": { "args": [ "draw1", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p2 <- 0", "ref": "p2", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw1, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p2 = 2))", "exp": { "left": { "args": [ "draw1", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p2", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process2", "variables": [ { "initial-value": 0, "name": "b2", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r2", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p3 <- 1", "ref": "p3", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw1, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p3 = 0))", "exp": { "left": { "args": [ "draw2", "draw1", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p3", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw3 <- 1", "ref": "draw3", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw1, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & draw(p3, b3, r3)) & (draw3 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw1", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p3", "b3", "r3" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw3", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b3 <- 1", "ref": "b3", "value": 1 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b3 <- 2", "ref": "b3", "value": 2 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b3 <- 3", "ref": "b3", "value": 3 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b3 <- 4", "ref": "b3", "value": 4 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b3 <- 5", "ref": "b3", "value": 5 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b3 <- 6", "ref": "b3", "value": 6 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b3 <- 7", "ref": "b3", "value": 7 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b3 <- 8", "ref": "b3", "value": 8 }, { "comment": "r3 <- r", "ref": "r3", "value": "r" }, { "comment": "draw3 <- 0", "ref": "draw3", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw3 = 1)", "exp": { "left": "draw3", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p3 <- 2", "ref": "p3", "value": 2 }, { "comment": "b3 <- 0", "ref": "b3", "value": 0 }, { "comment": "r3 <- 0", "ref": "r3", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p3 <- 2", "ref": "p3", "value": 2 }, { "comment": "b3 <- 0", "ref": "b3", "value": 0 }, { "comment": "r3 <- 0", "ref": "r3", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw1, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p3 = 1)) & (b = b3)) & (r = r3)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p3", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b3" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r3" }, "op": "∧", "right": { "args": [ "draw2", "draw1", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p3 <- 0", "ref": "p3", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw1, draw4, draw5, draw6, draw7, draw8, draw9, draw10) & (p3 = 2))", "exp": { "left": { "args": [ "draw2", "draw1", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p3", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process3", "variables": [ { "initial-value": 0, "name": "b3", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r3", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p4 <- 1", "ref": "p4", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw1, draw5, draw6, draw7, draw8, draw9, draw10) & (p4 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw1", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p4", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw4 <- 1", "ref": "draw4", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw1, draw5, draw6, draw7, draw8, draw9, draw10) & draw(p4, b4, r4)) & (draw4 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw1", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p4", "b4", "r4" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw4", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b4 <- 1", "ref": "b4", "value": 1 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b4 <- 2", "ref": "b4", "value": 2 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b4 <- 3", "ref": "b4", "value": 3 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b4 <- 4", "ref": "b4", "value": 4 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b4 <- 5", "ref": "b4", "value": 5 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b4 <- 6", "ref": "b4", "value": 6 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b4 <- 7", "ref": "b4", "value": 7 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b4 <- 8", "ref": "b4", "value": 8 }, { "comment": "r4 <- r", "ref": "r4", "value": "r" }, { "comment": "draw4 <- 0", "ref": "draw4", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw4 = 1)", "exp": { "left": "draw4", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p4 <- 2", "ref": "p4", "value": 2 }, { "comment": "b4 <- 0", "ref": "b4", "value": 0 }, { "comment": "r4 <- 0", "ref": "r4", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p4 <- 2", "ref": "p4", "value": 2 }, { "comment": "b4 <- 0", "ref": "b4", "value": 0 }, { "comment": "r4 <- 0", "ref": "r4", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw1, draw5, draw6, draw7, draw8, draw9, draw10) & (p4 = 1)) & (b = b4)) & (r = r4)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p4", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b4" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r4" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw1", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p4 <- 0", "ref": "p4", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw1, draw5, draw6, draw7, draw8, draw9, draw10) & (p4 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw1", "draw5", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p4", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process4", "variables": [ { "initial-value": 0, "name": "b4", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r4", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p5 <- 1", "ref": "p5", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw1, draw6, draw7, draw8, draw9, draw10) & (p5 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw1", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p5", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw5 <- 1", "ref": "draw5", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw4, draw1, draw6, draw7, draw8, draw9, draw10) & draw(p5, b5, r5)) & (draw5 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw4", "draw1", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p5", "b5", "r5" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw5", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b5 <- 1", "ref": "b5", "value": 1 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b5 <- 2", "ref": "b5", "value": 2 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b5 <- 3", "ref": "b5", "value": 3 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b5 <- 4", "ref": "b5", "value": 4 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b5 <- 5", "ref": "b5", "value": 5 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b5 <- 6", "ref": "b5", "value": 6 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b5 <- 7", "ref": "b5", "value": 7 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b5 <- 8", "ref": "b5", "value": 8 }, { "comment": "r5 <- r", "ref": "r5", "value": "r" }, { "comment": "draw5 <- 0", "ref": "draw5", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw5 = 1)", "exp": { "left": "draw5", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p5 <- 2", "ref": "p5", "value": 2 }, { "comment": "b5 <- 0", "ref": "b5", "value": 0 }, { "comment": "r5 <- 0", "ref": "r5", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p5 <- 2", "ref": "p5", "value": 2 }, { "comment": "b5 <- 0", "ref": "b5", "value": 0 }, { "comment": "r5 <- 0", "ref": "r5", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw4, draw1, draw6, draw7, draw8, draw9, draw10) & (p5 = 1)) & (b = b5)) & (r = r5)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p5", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b5" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r5" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw4", "draw1", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p5 <- 0", "ref": "p5", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw1, draw6, draw7, draw8, draw9, draw10) & (p5 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw1", "draw6", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p5", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process5", "variables": [ { "initial-value": 0, "name": "b5", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r5", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p6 <- 1", "ref": "p6", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw1, draw7, draw8, draw9, draw10) & (p6 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw1", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p6", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw6 <- 1", "ref": "draw6", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw4, draw5, draw1, draw7, draw8, draw9, draw10) & draw(p6, b6, r6)) & (draw6 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw1", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p6", "b6", "r6" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw6", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b6 <- 1", "ref": "b6", "value": 1 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b6 <- 2", "ref": "b6", "value": 2 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b6 <- 3", "ref": "b6", "value": 3 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b6 <- 4", "ref": "b6", "value": 4 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b6 <- 5", "ref": "b6", "value": 5 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b6 <- 6", "ref": "b6", "value": 6 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b6 <- 7", "ref": "b6", "value": 7 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b6 <- 8", "ref": "b6", "value": 8 }, { "comment": "r6 <- r", "ref": "r6", "value": "r" }, { "comment": "draw6 <- 0", "ref": "draw6", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw6 = 1)", "exp": { "left": "draw6", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p6 <- 2", "ref": "p6", "value": 2 }, { "comment": "b6 <- 0", "ref": "b6", "value": 0 }, { "comment": "r6 <- 0", "ref": "r6", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p6 <- 2", "ref": "p6", "value": 2 }, { "comment": "b6 <- 0", "ref": "b6", "value": 0 }, { "comment": "r6 <- 0", "ref": "r6", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw4, draw5, draw1, draw7, draw8, draw9, draw10) & (p6 = 1)) & (b = b6)) & (r = r6)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p6", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b6" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r6" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw1", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p6 <- 0", "ref": "p6", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw1, draw7, draw8, draw9, draw10) & (p6 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw1", "draw7", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p6", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process6", "variables": [ { "initial-value": 0, "name": "b6", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r6", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p7 <- 1", "ref": "p7", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw1, draw8, draw9, draw10) & (p7 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw1", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p7", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw7 <- 1", "ref": "draw7", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw4, draw5, draw6, draw1, draw8, draw9, draw10) & draw(p7, b7, r7)) & (draw7 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw1", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p7", "b7", "r7" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw7", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b7 <- 1", "ref": "b7", "value": 1 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b7 <- 2", "ref": "b7", "value": 2 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b7 <- 3", "ref": "b7", "value": 3 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b7 <- 4", "ref": "b7", "value": 4 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b7 <- 5", "ref": "b7", "value": 5 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b7 <- 6", "ref": "b7", "value": 6 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b7 <- 7", "ref": "b7", "value": 7 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b7 <- 8", "ref": "b7", "value": 8 }, { "comment": "r7 <- r", "ref": "r7", "value": "r" }, { "comment": "draw7 <- 0", "ref": "draw7", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw7 = 1)", "exp": { "left": "draw7", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p7 <- 2", "ref": "p7", "value": 2 }, { "comment": "b7 <- 0", "ref": "b7", "value": 0 }, { "comment": "r7 <- 0", "ref": "r7", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p7 <- 2", "ref": "p7", "value": 2 }, { "comment": "b7 <- 0", "ref": "b7", "value": 0 }, { "comment": "r7 <- 0", "ref": "r7", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw4, draw5, draw6, draw1, draw8, draw9, draw10) & (p7 = 1)) & (b = b7)) & (r = r7)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p7", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b7" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r7" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw1", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p7 <- 0", "ref": "p7", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw1, draw8, draw9, draw10) & (p7 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw1", "draw8", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p7", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process7", "variables": [ { "initial-value": 0, "name": "b7", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r7", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p8 <- 1", "ref": "p8", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw1, draw9, draw10) & (p8 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw1", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p8", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw8 <- 1", "ref": "draw8", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw4, draw5, draw6, draw7, draw1, draw9, draw10) & draw(p8, b8, r8)) & (draw8 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw1", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p8", "b8", "r8" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw8", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b8 <- 1", "ref": "b8", "value": 1 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b8 <- 2", "ref": "b8", "value": 2 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b8 <- 3", "ref": "b8", "value": 3 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b8 <- 4", "ref": "b8", "value": 4 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b8 <- 5", "ref": "b8", "value": 5 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b8 <- 6", "ref": "b8", "value": 6 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b8 <- 7", "ref": "b8", "value": 7 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b8 <- 8", "ref": "b8", "value": 8 }, { "comment": "r8 <- r", "ref": "r8", "value": "r" }, { "comment": "draw8 <- 0", "ref": "draw8", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw8 = 1)", "exp": { "left": "draw8", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p8 <- 2", "ref": "p8", "value": 2 }, { "comment": "b8 <- 0", "ref": "b8", "value": 0 }, { "comment": "r8 <- 0", "ref": "r8", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p8 <- 2", "ref": "p8", "value": 2 }, { "comment": "b8 <- 0", "ref": "b8", "value": 0 }, { "comment": "r8 <- 0", "ref": "r8", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw4, draw5, draw6, draw7, draw1, draw9, draw10) & (p8 = 1)) & (b = b8)) & (r = r8)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p8", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b8" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r8" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw1", "draw9", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p8 <- 0", "ref": "p8", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw1, draw9, draw10) & (p8 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw1", "draw9", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p8", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process8", "variables": [ { "initial-value": 0, "name": "b8", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r8", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p9 <- 1", "ref": "p9", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw1, draw10) & (p9 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw1", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p9", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw9 <- 1", "ref": "draw9", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw1, draw10) & draw(p9, b9, r9)) & (draw9 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw1", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p9", "b9", "r9" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw9", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b9 <- 1", "ref": "b9", "value": 1 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b9 <- 2", "ref": "b9", "value": 2 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b9 <- 3", "ref": "b9", "value": 3 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b9 <- 4", "ref": "b9", "value": 4 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b9 <- 5", "ref": "b9", "value": 5 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b9 <- 6", "ref": "b9", "value": 6 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b9 <- 7", "ref": "b9", "value": 7 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b9 <- 8", "ref": "b9", "value": 8 }, { "comment": "r9 <- r", "ref": "r9", "value": "r" }, { "comment": "draw9 <- 0", "ref": "draw9", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw9 = 1)", "exp": { "left": "draw9", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p9 <- 2", "ref": "p9", "value": 2 }, { "comment": "b9 <- 0", "ref": "b9", "value": 0 }, { "comment": "r9 <- 0", "ref": "r9", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p9 <- 2", "ref": "p9", "value": 2 }, { "comment": "b9 <- 0", "ref": "b9", "value": 0 }, { "comment": "r9 <- 0", "ref": "r9", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw1, draw10) & (p9 = 1)) & (b = b9)) & (r = r9)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p9", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b9" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r9" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw1", "draw10" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p9 <- 0", "ref": "p9", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw1, draw10) & (p9 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw1", "draw10" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p9", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process9", "variables": [ { "initial-value": 0, "name": "b9", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r9", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "p10 <- 1", "ref": "p10", "value": 1 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw1) & (p10 = 0))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw1" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p10", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "draw10 <- 1", "ref": "draw10", "value": 1 } ], "location": "l" } ], "guard": { "comment": "((go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw1) & draw(p10, b10, r10)) & (draw10 = 0))", "exp": { "left": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw1" ], "function": "go", "op": "call" }, "op": "∧", "right": { "args": [ "p10", "b10", "r10" ], "function": "draw", "op": "call" } }, "op": "∧", "right": { "left": "draw10", "op": "=", "right": 0 } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "b <- (max(b, 1))", "ref": "b", "value": { "left": "b", "op": "max", "right": 1 } }, { "comment": "b10 <- 1", "ref": "b10", "value": 1 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "b <- (max(b, 2))", "ref": "b", "value": { "left": "b", "op": "max", "right": 2 } }, { "comment": "b10 <- 2", "ref": "b10", "value": 2 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/4", "exp": 0.25 } }, { "assignments": [ { "comment": "b <- (max(b, 3))", "ref": "b", "value": { "left": "b", "op": "max", "right": 3 } }, { "comment": "b10 <- 3", "ref": "b10", "value": 3 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/8", "exp": 0.125 } }, { "assignments": [ { "comment": "b <- (max(b, 4))", "ref": "b", "value": { "left": "b", "op": "max", "right": 4 } }, { "comment": "b10 <- 4", "ref": "b10", "value": 4 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/16", "exp": 0.0625 } }, { "assignments": [ { "comment": "b <- (max(b, 5))", "ref": "b", "value": { "left": "b", "op": "max", "right": 5 } }, { "comment": "b10 <- 5", "ref": "b10", "value": 5 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/32", "exp": 0.03125 } }, { "assignments": [ { "comment": "b <- (max(b, 6))", "ref": "b", "value": { "left": "b", "op": "max", "right": 6 } }, { "comment": "b10 <- 6", "ref": "b10", "value": 6 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/64", "exp": 0.015625 } }, { "assignments": [ { "comment": "b <- (max(b, 7))", "ref": "b", "value": { "left": "b", "op": "max", "right": 7 } }, { "comment": "b10 <- 7", "ref": "b10", "value": 7 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } }, { "assignments": [ { "comment": "b <- (max(b, 8))", "ref": "b", "value": { "left": "b", "op": "max", "right": 8 } }, { "comment": "b10 <- 8", "ref": "b10", "value": 8 }, { "comment": "r10 <- r", "ref": "r10", "value": "r" }, { "comment": "draw10 <- 0", "ref": "draw10", "value": 0 } ], "location": "l", "probability": { "comment": "1/128", "exp": 0.0078125 } } ], "guard": { "comment": "(draw10 = 1)", "exp": { "left": "draw10", "op": "=", "right": 1 } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 1", "ref": "r", "value": 1 }, { "comment": "p10 <- 2", "ref": "p10", "value": 2 }, { "comment": "b10 <- 0", "ref": "b10", "value": 0 }, { "comment": "r10 <- 0", "ref": "r10", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } }, { "assignments": [ { "comment": "c <- 1", "ref": "c", "value": 1 }, { "comment": "b <- 0", "ref": "b", "value": 0 }, { "comment": "r <- 2", "ref": "r", "value": 2 }, { "comment": "p10 <- 2", "ref": "p10", "value": 2 }, { "comment": "b10 <- 0", "ref": "b10", "value": 0 }, { "comment": "r10 <- 0", "ref": "r10", "value": 0 } ], "location": "l", "probability": { "comment": "1/2", "exp": 0.5 } } ], "guard": { "comment": "((((go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw1) & (p10 = 1)) & (b = b10)) & (r = r10)) & (c = 0))", "exp": { "left": { "left": { "left": { "left": "c", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "p10", "op": "=", "right": 1 } }, "op": "∧", "right": { "left": "b", "op": "=", "right": "b10" } }, "op": "∧", "right": { "left": { "left": "r", "op": "=", "right": "r10" }, "op": "∧", "right": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw1" ], "function": "go", "op": "call" } } } }, "location": "l" }, { "destinations": [ { "assignments": [ { "comment": "c <- 0", "ref": "c", "value": 0 }, { "comment": "p10 <- 0", "ref": "p10", "value": 0 } ], "location": "l" } ], "guard": { "comment": "(go(draw2, draw3, draw4, draw5, draw6, draw7, draw8, draw9, draw1) & (p10 = 2))", "exp": { "left": { "args": [ "draw2", "draw3", "draw4", "draw5", "draw6", "draw7", "draw8", "draw9", "draw1" ], "function": "go", "op": "call" }, "op": "∧", "right": { "left": "p10", "op": "=", "right": 2 } } }, "location": "l" } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "process10", "variables": [ { "initial-value": 0, "name": "b10", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 0, "name": "r10", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } } ] } ], "constants": [ { "name": "K", "type": "int", "value": 8 } ], "features": [ "derived-operators", "functions" ], "functions": [ { "body": { "left": { "left": { "left": { "left": { "left": "go__param__draw10", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "go__param__draw3", "op": "=", "right": 0 } }, "op": "∧", "right": { "left": "go__param__draw6", "op": "=", "right": 0 } }, "op": "∧", "right": { "left": { "left": "go__param__draw8", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "go__param__draw4", "op": "=", "right": 0 } } }, "op": "∧", "right": { "left": { "left": { "left": "go__param__draw9", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "go__param__draw2", "op": "=", "right": 0 } }, "op": "∧", "right": { "left": { "left": "go__param__draw7", "op": "=", "right": 0 }, "op": "∧", "right": { "left": "go__param__draw5", "op": "=", "right": 0 } } } }, "name": "go", "parameters": [ { "name": "go__param__draw2", "type": "int" }, { "name": "go__param__draw3", "type": "int" }, { "name": "go__param__draw4", "type": "int" }, { "name": "go__param__draw5", "type": "int" }, { "name": "go__param__draw6", "type": "int" }, { "name": "go__param__draw7", "type": "int" }, { "name": "go__param__draw8", "type": "int" }, { "name": "go__param__draw9", "type": "int" }, { "name": "go__param__draw10", "type": "int" } ], "type": "bool" }, { "body": { "left": { "left": "draw__param__p1", "op": "=", "right": 1 }, "op": "∧", "right": { "left": { "left": "b", "op": "<", "right": "draw__param__b1" }, "op": "∨", "right": { "left": "r", "op": "≠", "right": "draw__param__r1" } } }, "name": "draw", "parameters": [ { "name": "draw__param__p1", "type": "int" }, { "name": "draw__param__b1", "type": "int" }, { "name": "draw__param__r1", "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": "target" }, "op": "Pmax" } }, "name": "live" } ], "restrict-initial": { "exp": true }, "system": { "elements": [ { "automaton": "process1" }, { "automaton": "process2" }, { "automaton": "process3" }, { "automaton": "process4" }, { "automaton": "process5" }, { "automaton": "process6" }, { "automaton": "process7" }, { "automaton": "process8" }, { "automaton": "process9" }, { "automaton": "process10" } ] }, "type": "mdp", "variables": [ { "initial-value": 0, "name": "c", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "b", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 8 } }, { "initial-value": 1, "name": "r", "type": { "base": "int", "kind": "bounded", "lower-bound": 1, "upper-bound": 2 } }, { "initial-value": false, "name": "target", "transient": true, "type": "bool" }, { "initial-value": 0, "name": "p1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p2", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw2", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p3", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw3", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p4", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw4", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p5", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw5", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p6", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw6", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p7", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw7", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p8", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw8", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p9", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw9", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } }, { "initial-value": 0, "name": "p10", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 2 } }, { "initial-value": 0, "name": "draw10", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 1 } } ] }