model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.25 MB)
Taken from QVBS (January 2026). The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020. Original Prism model and property files have been adapted for compatibility and simplicity: - Constants: All open constants are now explicitly set within model.prism (no need to set them via command line) - Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property. - Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.
// N-processor mutual exclusion [Rab82] // gxn/dxp 03/12/08 // to remove the need for fairness constraints for this model it is sufficent // to remove the self loops from the model // the step corresponding to a process making a draw has been split into two steps // to allow us to identify states where a process will draw without knowing the value // randomly drawn // to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic // (i.e. no other process can move one the first step has been made) // as for example otherwise an adversary can prevent the process from actually drawing // in the current round by not scheduling it after it has performed the first step mdp // size of shared counter const int K = 8; // 4+ceil(log_2 N) // global variables (all modules can read and write) global c : [0..1]; // 0/1 critical section free/taken global b : [0..K]; // current highest draw global r : [1..2]; // current round // formula for process 1 drawing formula draw = p1=1 & (b(p1'=0); // enter trying [] go & p1=0 -> (p1'=1); // make a draw [] go & draw & draw1=0 -> (draw1'=1); [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0) + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule module process7 = process1 [p1=p7, b1=b7, r1=r7, draw1=draw7, draw7=draw1 ] endmodule module process8 = process1 [p1=p8, b1=b8, r1=r8, draw1=draw8, draw8=draw1 ] endmodule module process9 = process1 [p1=p9, b1=b9, r1=r9, draw1=draw9, draw9=draw1 ] endmodule module process10 = process1 [p1=p10, b1=b10, r1=r10, draw1=draw10, draw10=draw1 ] endmodule label "target" = (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2);
"live": Pmax=? [ F "target" ] ;
{
"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
}
}
]
}