model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.28 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.
// randomized protocol for signing contracts Even, Goldreich and Lempel dtmc // we now let B to makes his/her choices based on what he/she knows // to do this I have added non-determinism to the previous version // and changed the modules so that only "B's view" is visible // then reveal the values when B thinks he has an advantage // to model the non-deterministic behaviour of corrupt party (party B) // we have a set of possible initial states corresponding to what messages // he/she tries to over hear when sending - we could do this with nondeterminism // but it will just make the model less structured and B has to make the choices // at the start anyway since B's view at this point should tell him nothing // (we use the new construct init...endinit to specify the set of initial states) // note that certain variables that belong to a party appear in the other party's module // as this leads to a more structured model - without this PRISM runs out of memory // note we have included the case when B stops if he/she thinks that the protocol has reached // a state where he/she has an advantage // currently, this model only works for N up to 20 const int N=10; // number of pairs of secrets the party sends const int L=2; // number of bits in each secret module counter b : [1..L]; // counter for current bit to be send (used in phases 2 and 3) n : [0..max(N-1,1)]; // counter as parties send N messages in a row phase : [1..5]; // phase of the protocol party : [1..2]; // which party moves // 1 first phase of the protocol (sending messages of the form OT(.,.,.,.) // 2 and 3 - second phase of the protocol (sending secretes 1..n and n+1..2n respectively) // 4 finished the protocol // FIRST PHASE [receiveB] phase=1 & party=1 -> (party'=2); // first A sends a message then B does [receiveA] phase=1 & party=2 & n(party'=1) & (n'=n+1); // after B sends a message we move onto the next message [receiveA] phase=1 & party=2 & n=N-1 -> (party'=1) & (phase'=2) & (n'=0); // B has sent his final message - move to next phase // SECOND AND THIRD PHASES // when A sends [receiveB] ((phase)>=(2)&(phase)<=(3))& party=1 & n=0-> (party'=2); // A transmits bth bit of secrets 1..N or N=1..2N [receiveA] ((phase)>=(2)&(phase)<=(3))& party=2 & n (n'=n+1); // A transmits bth bit of secrets 1..N or N=1..2N [receiveA] ((phase)>=(2)&(phase)<=(3))& party=2 & n=N-1 -> (party'=1) & (n'=1); // finished for party A now move to party B // when A sends [receiveB] ((phase)>=(2)&(phase)<=(3))& party=1 & n 0 -> (n'=n+1); // B transmits bth bit of secrets 1..N or N=1..2N [receiveB] ((phase)>=(2)&(phase)<=(3))& party=1 & n=N-1 & b (party'=1) & (n'=0) & (b'=b+1); // finished for party B move to next bit [receiveB] phase=2 & party=1 & n=N-1 & b=L -> (phase'=3) & (party'=1) & (n'=0) & (b'=1); // finished for party B move to next phase [receiveB] phase=3 & party=1 & n=N-1 & b=L -> (phase'=4); // finished protocol (reveal values) // FINISHED [] phase=4 -> (phase'=4); // loop endmodule // party A module partyA // bi the number of bits of B's ith secret A knows // (keep pairs of secrets together to give a more structured model) b0 : [0..L]; b20 : [0..L]; b1 : [0..L]; b21 : [0..L]; b2 : [0..L]; b22 : [0..L]; b3 : [0..L]; b23 : [0..L]; b4 : [0..L]; b24 : [0..L]; b5 : [0..L]; b25 : [0..L]; b6 : [0..L]; b26 : [0..L]; b7 : [0..L]; b27 : [0..L]; b8 : [0..L]; b28 : [0..L]; b9 : [0..L]; b29 : [0..L]; b10 : [0..L]; b30 : [0..L]; b11 : [0..L]; b31 : [0..L]; b12 : [0..L]; b32 : [0..L]; b13 : [0..L]; b33 : [0..L]; b14 : [0..L]; b34 : [0..L]; b15 : [0..L]; b35 : [0..L]; b16 : [0..L]; b36 : [0..L]; b17 : [0..L]; b37 : [0..L]; b18 : [0..L]; b38 : [0..L]; b19 : [0..L]; b39 : [0..L]; // first step (get either secret i or (N-1)+i with equal probability) [receiveA] phase=1 & n=0 -> 0.5 : (b0'=L) + 0.5 : (b20'=L); [receiveA] phase=1 & n=1 -> 0.5 : (b1'=L) + 0.5 : (b21'=L); [receiveA] phase=1 & n=2 -> 0.5 : (b2'=L) + 0.5 : (b22'=L); [receiveA] phase=1 & n=3 -> 0.5 : (b3'=L) + 0.5 : (b23'=L); [receiveA] phase=1 & n=4 -> 0.5 : (b4'=L) + 0.5 : (b24'=L); [receiveA] phase=1 & n=5 -> 0.5 : (b5'=L) + 0.5 : (b25'=L); [receiveA] phase=1 & n=6 -> 0.5 : (b6'=L) + 0.5 : (b26'=L); [receiveA] phase=1 & n=7 -> 0.5 : (b7'=L) + 0.5 : (b27'=L); [receiveA] phase=1 & n=8 -> 0.5 : (b8'=L) + 0.5 : (b28'=L); [receiveA] phase=1 & n=9 -> 0.5 : (b9'=L) + 0.5 : (b29'=L); [receiveA] phase=1 & n=10 -> 0.5 : (b10'=L) + 0.5 : (b30'=L); [receiveA] phase=1 & n=11 -> 0.5 : (b11'=L) + 0.5 : (b31'=L); [receiveA] phase=1 & n=12 -> 0.5 : (b12'=L) + 0.5 : (b32'=L); [receiveA] phase=1 & n=13 -> 0.5 : (b13'=L) + 0.5 : (b33'=L); [receiveA] phase=1 & n=14 -> 0.5 : (b14'=L) + 0.5 : (b34'=L); [receiveA] phase=1 & n=15 -> 0.5 : (b15'=L) + 0.5 : (b35'=L); [receiveA] phase=1 & n=16 -> 0.5 : (b16'=L) + 0.5 : (b36'=L); [receiveA] phase=1 & n=17 -> 0.5 : (b17'=L) + 0.5 : (b37'=L); [receiveA] phase=1 & n=18 -> 0.5 : (b18'=L) + 0.5 : (b38'=L); [receiveA] phase=1 & n=19 -> 0.5 : (b19'=L) + 0.5 : (b39'=L); // second step (secrets 0,...,N-1) [receiveA] phase=2 & n=0 -> (b0'=min(b0+1,L)); [receiveA] phase=2 & n=1 -> (b1'=min(b1+1,L)); [receiveA] phase=2 & n=2 -> (b2'=min(b2+1,L)); [receiveA] phase=2 & n=3 -> (b3'=min(b3+1,L)); [receiveA] phase=2 & n=4 -> (b4'=min(b4+1,L)); [receiveA] phase=2 & n=5 -> (b5'=min(b5+1,L)); [receiveA] phase=2 & n=6 -> (b6'=min(b6+1,L)); [receiveA] phase=2 & n=7 -> (b7'=min(b7+1,L)); [receiveA] phase=2 & n=8 -> (b8'=min(b8+1,L)); [receiveA] phase=2 & n=9 -> (b9'=min(b9+1,L)); [receiveA] phase=2 & n=10 -> (b10'=min(b10+1,L)); [receiveA] phase=2 & n=11 -> (b11'=min(b11+1,L)); [receiveA] phase=2 & n=12 -> (b12'=min(b12+1,L)); [receiveA] phase=2 & n=13 -> (b13'=min(b13+1,L)); [receiveA] phase=2 & n=14 -> (b14'=min(b14+1,L)); [receiveA] phase=2 & n=15 -> (b15'=min(b15+1,L)); [receiveA] phase=2 & n=16 -> (b16'=min(b16+1,L)); [receiveA] phase=2 & n=17 -> (b17'=min(b17+1,L)); [receiveA] phase=2 & n=18 -> (b18'=min(b18+1,L)); [receiveA] phase=2 & n=19 -> (b19'=min(b19+1,L)); // second step (secrets N,...,2N-1) [receiveA] phase=3 & n=0 -> (b20'=min(b20+1,L)); [receiveA] phase=3 & n=1 -> (b21'=min(b21+1,L)); [receiveA] phase=3 & n=2 -> (b22'=min(b22+1,L)); [receiveA] phase=3 & n=3 -> (b23'=min(b23+1,L)); [receiveA] phase=3 & n=4 -> (b24'=min(b24+1,L)); [receiveA] phase=3 & n=5 -> (b25'=min(b25+1,L)); [receiveA] phase=3 & n=6 -> (b26'=min(b26+1,L)); [receiveA] phase=3 & n=7 -> (b27'=min(b27+1,L)); [receiveA] phase=3 & n=8 -> (b28'=min(b28+1,L)); [receiveA] phase=3 & n=9 -> (b29'=min(b29+1,L)); [receiveA] phase=3 & n=10 -> (b30'=min(b30+1,L)); [receiveA] phase=3 & n=11 -> (b31'=min(b31+1,L)); [receiveA] phase=3 & n=12 -> (b32'=min(b32+1,L)); [receiveA] phase=3 & n=13 -> (b33'=min(b33+1,L)); [receiveA] phase=3 & n=14 -> (b34'=min(b34+1,L)); [receiveA] phase=3 & n=15 -> (b35'=min(b35+1,L)); [receiveA] phase=3 & n=16 -> (b36'=min(b36+1,L)); [receiveA] phase=3 & n=17 -> (b37'=min(b37+1,L)); [receiveA] phase=3 & n=18 -> (b38'=min(b38+1,L)); [receiveA] phase=3 & n=19 -> (b39'=min(b39+1,L)); endmodule // construct module for party B through renaming module partyB=partyA[b0 =a0 ,b1 =a1 ,b2 =a2 ,b3 =a3 ,b4 =a4 ,b5 =a5 ,b6 =a6 ,b7 =a7 ,b8 =a8 ,b9 =a9, b10=a10,b11=a11,b12=a12,b13=a13,b14=a14,b15=a15,b16=a16,b17=a17,b18=a18,b19=a19, b20=a20,b21=a21,b22=a22,b23=a23,b24=a24,b25=a25,b26=a26,b27=a27,b28=a28,b29=a29, b30=a30,b31=a31,b32=a32,b33=a33,b34=a34,b35=a35,b36=a36,b37=a37,b38=a38,b39=a39, receiveA=receiveB] endmodule // formulae formula kB = ( (a0=L & a20=L) | (a1=L & a21=L) | (a2=L & a22=L) | (a3=L & a23=L) | (a4=L & a24=L) | (a5=L & a25=L) | (a6=L & a26=L) | (a7=L & a27=L) | (a8=L & a28=L) | (a9=L & a29=L) | (a10=L & a30=L) | (a11=L & a31=L) | (a12=L & a32=L) | (a13=L & a33=L) | (a14=L & a34=L) | (a15=L & a35=L) | (a16=L & a36=L) | (a17=L & a37=L) | (a18=L & a38=L) | (a19=L & a39=L)); formula kA = ( (b0=L & b20=L) | (b1=L & b21=L) | (b2=L & b22=L) | (b3=L & b23=L) | (b4=L & b24=L) | (b5=L & b25=L) | (b6=L & b26=L) | (b7=L & b27=L) | (b8=L & b28=L) | (b9=L & b29=L) | (b10=L & b30=L) | (b11=L & b31=L) | (b12=L & b32=L) | (b13=L & b33=L) | (b14=L & b34=L) | (b15=L & b35=L) | (b16=L & b36=L) | (b17=L & b37=L) | (b18=L & b38=L) | (b19=L & b39=L)); // labels label "knowB" = kB; label "knowA" = kA;
"unfairA": P=? [ F !"knowA" & "knowB" ];
{
"actions": [
{
"name": "receiveA"
},
{
"name": "receiveB"
}
],
"automata": [
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "phase <- 4",
"ref": "phase",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(phase = 4)",
"exp": {
"left": "phase",
"op": "=",
"right": 4
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "n <- (n + 1)",
"ref": "n",
"value": {
"left": "n",
"op": "+",
"right": 1
}
},
{
"comment": "party <- 1",
"ref": "party",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((phase = 1) & (party = 2)) & (n < (10 - 1)))",
"exp": {
"left": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "party",
"op": "=",
"right": 2
}
},
"op": "∧",
"right": {
"left": "n",
"op": "<",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "n <- 0",
"ref": "n",
"value": 0
},
{
"comment": "phase <- 2",
"ref": "phase",
"value": 2
},
{
"comment": "party <- 1",
"ref": "party",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((phase = 1) & (party = 2)) & (n = (10 - 1)))",
"exp": {
"left": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "party",
"op": "=",
"right": 2
}
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "n <- (n + 1)",
"ref": "n",
"value": {
"left": "n",
"op": "+",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((((phase >= 2) & (phase <= 3)) & (party = 2)) & (n < (10 - 1)))",
"exp": {
"left": {
"left": {
"left": "n",
"op": "<",
"right": 9
},
"op": "∧",
"right": {
"left": "phase",
"op": "≤",
"right": 3
}
},
"op": "∧",
"right": {
"left": {
"left": "party",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "phase",
"op": "≥",
"right": 2
}
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "n <- 1",
"ref": "n",
"value": 1
},
{
"comment": "party <- 1",
"ref": "party",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((((phase >= 2) & (phase <= 3)) & (party = 2)) & (n = (10 - 1)))",
"exp": {
"left": {
"left": {
"left": "n",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "phase",
"op": "≤",
"right": 3
}
},
"op": "∧",
"right": {
"left": {
"left": "party",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "phase",
"op": "≥",
"right": 2
}
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "party <- 2",
"ref": "party",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 1) & (party = 1))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "party",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "party <- 2",
"ref": "party",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((((phase >= 2) & (phase <= 3)) & (party = 1)) & (n = 0))",
"exp": {
"left": {
"left": {
"left": "n",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "phase",
"op": "≤",
"right": 3
}
},
"op": "∧",
"right": {
"left": {
"left": "party",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "phase",
"op": "≥",
"right": 2
}
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "n <- (n + 1)",
"ref": "n",
"value": {
"left": "n",
"op": "+",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((((phase >= 2) & (phase <= 3)) & (party = 1)) & (n < (10 - 1))) & (n > 0))",
"exp": {
"left": {
"left": {
"left": {
"left": "n",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "phase",
"op": "≤",
"right": 3
}
},
"op": "∧",
"right": {
"left": "party",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "n",
"op": "<",
"right": 9
},
"op": "∧",
"right": {
"left": "phase",
"op": "≥",
"right": 2
}
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "b <- (b + 1)",
"ref": "b",
"value": {
"left": "b",
"op": "+",
"right": 1
}
},
{
"comment": "n <- 0",
"ref": "n",
"value": 0
},
{
"comment": "party <- 1",
"ref": "party",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((((phase >= 2) & (phase <= 3)) & (party = 1)) & (n = (10 - 1))) & (b < 2))",
"exp": {
"left": {
"left": {
"left": {
"left": "b",
"op": "<",
"right": 2
},
"op": "∧",
"right": {
"left": "phase",
"op": "≤",
"right": 3
}
},
"op": "∧",
"right": {
"left": "party",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "n",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "phase",
"op": "≥",
"right": 2
}
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "b <- 1",
"ref": "b",
"value": 1
},
{
"comment": "n <- 0",
"ref": "n",
"value": 0
},
{
"comment": "phase <- 3",
"ref": "phase",
"value": 3
},
{
"comment": "party <- 1",
"ref": "party",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((((phase = 2) & (party = 1)) & (n = (10 - 1))) & (b = 2))",
"exp": {
"left": {
"left": {
"left": "b",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "party",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "n",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "phase",
"op": "=",
"right": 2
}
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "phase <- 4",
"ref": "phase",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "((((phase = 3) & (party = 1)) & (n = (10 - 1))) & (b = 2))",
"exp": {
"left": {
"left": {
"left": "b",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "party",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "n",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "phase",
"op": "=",
"right": 3
}
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "knowB <- kB(a0, a20, a1, a21, a2, a22, a3, a23, a4, a24, a5, a25, a6, a26, a7, a27, a8, a28, a9, a29, a10, a30, a11, a31, a12, a32, a13, a33, a14, a34, a15, a35, a16, a36, a17, a37, a18, a38, a19, a39)",
"ref": "knowB",
"value": {
"args": [
"a0",
"a20",
"a1",
"a21",
"a2",
"a22",
"a3",
"a23",
"a4",
"a24",
"a5",
"a25",
"a6",
"a26",
"a7",
"a27",
"a8",
"a28",
"a9",
"a29",
"a10",
"a30",
"a11",
"a31",
"a12",
"a32",
"a13",
"a33",
"a14",
"a34",
"a15",
"a35",
"a16",
"a36",
"a17",
"a37",
"a18",
"a38",
"a19",
"a39"
],
"function": "kB",
"op": "call"
}
},
{
"comment": "knowA <- kA(b0, b20, b1, b21, b2, b22, b3, b23, b4, b24, b5, b25, b6, b26, b7, b27, b8, b28, b9, b29, b10, b30, b11, b31, b12, b32, b13, b33, b14, b34, b15, b35, b16, b36, b17, b37, b18, b38, b19, b39)",
"ref": "knowA",
"value": {
"args": [
"b0",
"b20",
"b1",
"b21",
"b2",
"b22",
"b3",
"b23",
"b4",
"b24",
"b5",
"b25",
"b6",
"b26",
"b7",
"b27",
"b8",
"b28",
"b9",
"b29",
"b10",
"b30",
"b11",
"b31",
"b12",
"b32",
"b13",
"b33",
"b14",
"b34",
"b15",
"b35",
"b16",
"b36",
"b17",
"b37",
"b18",
"b38",
"b19",
"b39"
],
"function": "kA",
"op": "call"
}
}
]
}
],
"name": "counter",
"variables": [
{
"initial-value": 1,
"name": "b",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 2
}
},
{
"initial-value": 1,
"name": "party",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 2
}
}
]
},
{
"edges": [
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b0 <- 2",
"ref": "b0",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b20 <- 2",
"ref": "b20",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 0))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b1 <- 2",
"ref": "b1",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b21 <- 2",
"ref": "b21",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 1))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b2 <- 2",
"ref": "b2",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b22 <- 2",
"ref": "b22",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 2))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b3 <- 2",
"ref": "b3",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b23 <- 2",
"ref": "b23",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 3))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b4 <- 2",
"ref": "b4",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b24 <- 2",
"ref": "b24",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 4))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b5 <- 2",
"ref": "b5",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b25 <- 2",
"ref": "b25",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 5))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 5
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b6 <- 2",
"ref": "b6",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b26 <- 2",
"ref": "b26",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 6))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b7 <- 2",
"ref": "b7",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b27 <- 2",
"ref": "b27",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 7))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 7
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b8 <- 2",
"ref": "b8",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b28 <- 2",
"ref": "b28",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 8))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 8
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b9 <- 2",
"ref": "b9",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b29 <- 2",
"ref": "b29",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 9))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b10 <- 2",
"ref": "b10",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b30 <- 2",
"ref": "b30",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 10))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 10
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b11 <- 2",
"ref": "b11",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b31 <- 2",
"ref": "b31",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 11))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 11
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b12 <- 2",
"ref": "b12",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b32 <- 2",
"ref": "b32",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 12))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 12
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b13 <- 2",
"ref": "b13",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b33 <- 2",
"ref": "b33",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 13))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 13
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b14 <- 2",
"ref": "b14",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b34 <- 2",
"ref": "b34",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 14))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 14
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b15 <- 2",
"ref": "b15",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b35 <- 2",
"ref": "b35",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 15))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 15
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b16 <- 2",
"ref": "b16",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b36 <- 2",
"ref": "b36",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 16))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 16
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b17 <- 2",
"ref": "b17",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b37 <- 2",
"ref": "b37",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 17))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 17
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b18 <- 2",
"ref": "b18",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b38 <- 2",
"ref": "b38",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 18))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 18
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b19 <- 2",
"ref": "b19",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "b39 <- 2",
"ref": "b39",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 19))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 19
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b0 <- (min((b0 + 1), 2))",
"ref": "b0",
"value": {
"left": {
"left": "b0",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 0))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b1 <- (min((b1 + 1), 2))",
"ref": "b1",
"value": {
"left": {
"left": "b1",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 1))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b2 <- (min((b2 + 1), 2))",
"ref": "b2",
"value": {
"left": {
"left": "b2",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 2))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b3 <- (min((b3 + 1), 2))",
"ref": "b3",
"value": {
"left": {
"left": "b3",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 3))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b4 <- (min((b4 + 1), 2))",
"ref": "b4",
"value": {
"left": {
"left": "b4",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 4))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b5 <- (min((b5 + 1), 2))",
"ref": "b5",
"value": {
"left": {
"left": "b5",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 5))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 5
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b6 <- (min((b6 + 1), 2))",
"ref": "b6",
"value": {
"left": {
"left": "b6",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 6))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b7 <- (min((b7 + 1), 2))",
"ref": "b7",
"value": {
"left": {
"left": "b7",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 7))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 7
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b8 <- (min((b8 + 1), 2))",
"ref": "b8",
"value": {
"left": {
"left": "b8",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 8))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 8
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b9 <- (min((b9 + 1), 2))",
"ref": "b9",
"value": {
"left": {
"left": "b9",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 9))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b10 <- (min((b10 + 1), 2))",
"ref": "b10",
"value": {
"left": {
"left": "b10",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 10))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 10
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b11 <- (min((b11 + 1), 2))",
"ref": "b11",
"value": {
"left": {
"left": "b11",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 11))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 11
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b12 <- (min((b12 + 1), 2))",
"ref": "b12",
"value": {
"left": {
"left": "b12",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 12))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 12
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b13 <- (min((b13 + 1), 2))",
"ref": "b13",
"value": {
"left": {
"left": "b13",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 13))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 13
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b14 <- (min((b14 + 1), 2))",
"ref": "b14",
"value": {
"left": {
"left": "b14",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 14))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 14
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b15 <- (min((b15 + 1), 2))",
"ref": "b15",
"value": {
"left": {
"left": "b15",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 15))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 15
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b16 <- (min((b16 + 1), 2))",
"ref": "b16",
"value": {
"left": {
"left": "b16",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 16))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 16
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b17 <- (min((b17 + 1), 2))",
"ref": "b17",
"value": {
"left": {
"left": "b17",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 17))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 17
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b18 <- (min((b18 + 1), 2))",
"ref": "b18",
"value": {
"left": {
"left": "b18",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 18))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 18
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b19 <- (min((b19 + 1), 2))",
"ref": "b19",
"value": {
"left": {
"left": "b19",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 19))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 19
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b20 <- (min((b20 + 1), 2))",
"ref": "b20",
"value": {
"left": {
"left": "b20",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 0))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b21 <- (min((b21 + 1), 2))",
"ref": "b21",
"value": {
"left": {
"left": "b21",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 1))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b22 <- (min((b22 + 1), 2))",
"ref": "b22",
"value": {
"left": {
"left": "b22",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 2))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b23 <- (min((b23 + 1), 2))",
"ref": "b23",
"value": {
"left": {
"left": "b23",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 3))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b24 <- (min((b24 + 1), 2))",
"ref": "b24",
"value": {
"left": {
"left": "b24",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 4))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b25 <- (min((b25 + 1), 2))",
"ref": "b25",
"value": {
"left": {
"left": "b25",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 5))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 5
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b26 <- (min((b26 + 1), 2))",
"ref": "b26",
"value": {
"left": {
"left": "b26",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 6))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b27 <- (min((b27 + 1), 2))",
"ref": "b27",
"value": {
"left": {
"left": "b27",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 7))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 7
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b28 <- (min((b28 + 1), 2))",
"ref": "b28",
"value": {
"left": {
"left": "b28",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 8))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 8
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b29 <- (min((b29 + 1), 2))",
"ref": "b29",
"value": {
"left": {
"left": "b29",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 9))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b30 <- (min((b30 + 1), 2))",
"ref": "b30",
"value": {
"left": {
"left": "b30",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 10))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 10
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b31 <- (min((b31 + 1), 2))",
"ref": "b31",
"value": {
"left": {
"left": "b31",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 11))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 11
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b32 <- (min((b32 + 1), 2))",
"ref": "b32",
"value": {
"left": {
"left": "b32",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 12))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 12
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b33 <- (min((b33 + 1), 2))",
"ref": "b33",
"value": {
"left": {
"left": "b33",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 13))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 13
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b34 <- (min((b34 + 1), 2))",
"ref": "b34",
"value": {
"left": {
"left": "b34",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 14))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 14
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b35 <- (min((b35 + 1), 2))",
"ref": "b35",
"value": {
"left": {
"left": "b35",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 15))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 15
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b36 <- (min((b36 + 1), 2))",
"ref": "b36",
"value": {
"left": {
"left": "b36",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 16))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 16
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b37 <- (min((b37 + 1), 2))",
"ref": "b37",
"value": {
"left": {
"left": "b37",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 17))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 17
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b38 <- (min((b38 + 1), 2))",
"ref": "b38",
"value": {
"left": {
"left": "b38",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 18))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 18
}
}
},
"location": "l"
},
{
"action": "receiveA",
"destinations": [
{
"assignments": [
{
"comment": "b39 <- (min((b39 + 1), 2))",
"ref": "b39",
"value": {
"left": {
"left": "b39",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 19))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 19
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "partyA",
"variables": []
},
{
"edges": [
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a0 <- 2",
"ref": "a0",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a20 <- 2",
"ref": "a20",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 0))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a1 <- 2",
"ref": "a1",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a21 <- 2",
"ref": "a21",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 1))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a2 <- 2",
"ref": "a2",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a22 <- 2",
"ref": "a22",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 2))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a3 <- 2",
"ref": "a3",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a23 <- 2",
"ref": "a23",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 3))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a4 <- 2",
"ref": "a4",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a24 <- 2",
"ref": "a24",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 4))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a5 <- 2",
"ref": "a5",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a25 <- 2",
"ref": "a25",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 5))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 5
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a6 <- 2",
"ref": "a6",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a26 <- 2",
"ref": "a26",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 6))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a7 <- 2",
"ref": "a7",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a27 <- 2",
"ref": "a27",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 7))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 7
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a8 <- 2",
"ref": "a8",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a28 <- 2",
"ref": "a28",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 8))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 8
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a9 <- 2",
"ref": "a9",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a29 <- 2",
"ref": "a29",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 9))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a10 <- 2",
"ref": "a10",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a30 <- 2",
"ref": "a30",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 10))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 10
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a11 <- 2",
"ref": "a11",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a31 <- 2",
"ref": "a31",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 11))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 11
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a12 <- 2",
"ref": "a12",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a32 <- 2",
"ref": "a32",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 12))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 12
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a13 <- 2",
"ref": "a13",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a33 <- 2",
"ref": "a33",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 13))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 13
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a14 <- 2",
"ref": "a14",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a34 <- 2",
"ref": "a34",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 14))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 14
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a15 <- 2",
"ref": "a15",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a35 <- 2",
"ref": "a35",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 15))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 15
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a16 <- 2",
"ref": "a16",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a36 <- 2",
"ref": "a36",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 16))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 16
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a17 <- 2",
"ref": "a17",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a37 <- 2",
"ref": "a37",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 17))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 17
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a18 <- 2",
"ref": "a18",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a38 <- 2",
"ref": "a38",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 18))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 18
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a19 <- 2",
"ref": "a19",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "a39 <- 2",
"ref": "a39",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
}
],
"guard": {
"comment": "((phase = 1) & (n = 19))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 19
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a0 <- (min((a0 + 1), 2))",
"ref": "a0",
"value": {
"left": {
"left": "a0",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 0))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a1 <- (min((a1 + 1), 2))",
"ref": "a1",
"value": {
"left": {
"left": "a1",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 1))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a2 <- (min((a2 + 1), 2))",
"ref": "a2",
"value": {
"left": {
"left": "a2",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 2))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a3 <- (min((a3 + 1), 2))",
"ref": "a3",
"value": {
"left": {
"left": "a3",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 3))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a4 <- (min((a4 + 1), 2))",
"ref": "a4",
"value": {
"left": {
"left": "a4",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 4))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a5 <- (min((a5 + 1), 2))",
"ref": "a5",
"value": {
"left": {
"left": "a5",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 5))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 5
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a6 <- (min((a6 + 1), 2))",
"ref": "a6",
"value": {
"left": {
"left": "a6",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 6))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a7 <- (min((a7 + 1), 2))",
"ref": "a7",
"value": {
"left": {
"left": "a7",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 7))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 7
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a8 <- (min((a8 + 1), 2))",
"ref": "a8",
"value": {
"left": {
"left": "a8",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 8))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 8
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a9 <- (min((a9 + 1), 2))",
"ref": "a9",
"value": {
"left": {
"left": "a9",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 9))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a10 <- (min((a10 + 1), 2))",
"ref": "a10",
"value": {
"left": {
"left": "a10",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 10))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 10
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a11 <- (min((a11 + 1), 2))",
"ref": "a11",
"value": {
"left": {
"left": "a11",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 11))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 11
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a12 <- (min((a12 + 1), 2))",
"ref": "a12",
"value": {
"left": {
"left": "a12",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 12))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 12
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a13 <- (min((a13 + 1), 2))",
"ref": "a13",
"value": {
"left": {
"left": "a13",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 13))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 13
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a14 <- (min((a14 + 1), 2))",
"ref": "a14",
"value": {
"left": {
"left": "a14",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 14))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 14
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a15 <- (min((a15 + 1), 2))",
"ref": "a15",
"value": {
"left": {
"left": "a15",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 15))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 15
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a16 <- (min((a16 + 1), 2))",
"ref": "a16",
"value": {
"left": {
"left": "a16",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 16))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 16
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a17 <- (min((a17 + 1), 2))",
"ref": "a17",
"value": {
"left": {
"left": "a17",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 17))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 17
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a18 <- (min((a18 + 1), 2))",
"ref": "a18",
"value": {
"left": {
"left": "a18",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 18))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 18
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a19 <- (min((a19 + 1), 2))",
"ref": "a19",
"value": {
"left": {
"left": "a19",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 2) & (n = 19))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 19
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a20 <- (min((a20 + 1), 2))",
"ref": "a20",
"value": {
"left": {
"left": "a20",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 0))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a21 <- (min((a21 + 1), 2))",
"ref": "a21",
"value": {
"left": {
"left": "a21",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 1))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a22 <- (min((a22 + 1), 2))",
"ref": "a22",
"value": {
"left": {
"left": "a22",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 2))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a23 <- (min((a23 + 1), 2))",
"ref": "a23",
"value": {
"left": {
"left": "a23",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 3))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a24 <- (min((a24 + 1), 2))",
"ref": "a24",
"value": {
"left": {
"left": "a24",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 4))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a25 <- (min((a25 + 1), 2))",
"ref": "a25",
"value": {
"left": {
"left": "a25",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 5))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 5
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a26 <- (min((a26 + 1), 2))",
"ref": "a26",
"value": {
"left": {
"left": "a26",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 6))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a27 <- (min((a27 + 1), 2))",
"ref": "a27",
"value": {
"left": {
"left": "a27",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 7))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 7
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a28 <- (min((a28 + 1), 2))",
"ref": "a28",
"value": {
"left": {
"left": "a28",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 8))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 8
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a29 <- (min((a29 + 1), 2))",
"ref": "a29",
"value": {
"left": {
"left": "a29",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 9))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 9
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a30 <- (min((a30 + 1), 2))",
"ref": "a30",
"value": {
"left": {
"left": "a30",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 10))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 10
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a31 <- (min((a31 + 1), 2))",
"ref": "a31",
"value": {
"left": {
"left": "a31",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 11))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 11
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a32 <- (min((a32 + 1), 2))",
"ref": "a32",
"value": {
"left": {
"left": "a32",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 12))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 12
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a33 <- (min((a33 + 1), 2))",
"ref": "a33",
"value": {
"left": {
"left": "a33",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 13))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 13
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a34 <- (min((a34 + 1), 2))",
"ref": "a34",
"value": {
"left": {
"left": "a34",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 14))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 14
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a35 <- (min((a35 + 1), 2))",
"ref": "a35",
"value": {
"left": {
"left": "a35",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 15))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 15
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a36 <- (min((a36 + 1), 2))",
"ref": "a36",
"value": {
"left": {
"left": "a36",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 16))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 16
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a37 <- (min((a37 + 1), 2))",
"ref": "a37",
"value": {
"left": {
"left": "a37",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 17))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 17
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a38 <- (min((a38 + 1), 2))",
"ref": "a38",
"value": {
"left": {
"left": "a38",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 18))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 18
}
}
},
"location": "l"
},
{
"action": "receiveB",
"destinations": [
{
"assignments": [
{
"comment": "a39 <- (min((a39 + 1), 2))",
"ref": "a39",
"value": {
"left": {
"left": "a39",
"op": "+",
"right": 1
},
"op": "min",
"right": 2
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((phase = 3) & (n = 19))",
"exp": {
"left": {
"left": "phase",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "n",
"op": "=",
"right": 19
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "partyB",
"variables": []
}
],
"constants": [
{
"name": "N",
"type": "int",
"value": 10
},
{
"name": "L",
"type": "int",
"value": 2
}
],
"features": [
"derived-operators",
"functions"
],
"functions": [
{
"body": {
"left": {
"left": {
"left": {
"left": {
"left": {
"left": {
"left": "kA__param__b19",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b39",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b21",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kA__param__b10",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b30",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b9",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b29",
"op": "=",
"right": 2
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": "kA__param__b15",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b35",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b4",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b24",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kA__param__b14",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b34",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b5",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b25",
"op": "=",
"right": 2
}
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": "kA__param__b17",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b37",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b2",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b22",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kA__param__b12",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b32",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b7",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b27",
"op": "=",
"right": 2
}
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": {
"left": "kA__param__b18",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b38",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b0",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b20",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kA__param__b11",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b31",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b8",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b28",
"op": "=",
"right": 2
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": "kA__param__b16",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b36",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b3",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b23",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kA__param__b13",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b33",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kA__param__b6",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kA__param__b26",
"op": "=",
"right": 2
}
}
}
}
}
},
"name": "kA",
"parameters": [
{
"name": "kA__param__b0",
"type": "int"
},
{
"name": "kA__param__b20",
"type": "int"
},
{
"name": "kA__param__b1",
"type": "int"
},
{
"name": "kA__param__b21",
"type": "int"
},
{
"name": "kA__param__b2",
"type": "int"
},
{
"name": "kA__param__b22",
"type": "int"
},
{
"name": "kA__param__b3",
"type": "int"
},
{
"name": "kA__param__b23",
"type": "int"
},
{
"name": "kA__param__b4",
"type": "int"
},
{
"name": "kA__param__b24",
"type": "int"
},
{
"name": "kA__param__b5",
"type": "int"
},
{
"name": "kA__param__b25",
"type": "int"
},
{
"name": "kA__param__b6",
"type": "int"
},
{
"name": "kA__param__b26",
"type": "int"
},
{
"name": "kA__param__b7",
"type": "int"
},
{
"name": "kA__param__b27",
"type": "int"
},
{
"name": "kA__param__b8",
"type": "int"
},
{
"name": "kA__param__b28",
"type": "int"
},
{
"name": "kA__param__b9",
"type": "int"
},
{
"name": "kA__param__b29",
"type": "int"
},
{
"name": "kA__param__b10",
"type": "int"
},
{
"name": "kA__param__b30",
"type": "int"
},
{
"name": "kA__param__b11",
"type": "int"
},
{
"name": "kA__param__b31",
"type": "int"
},
{
"name": "kA__param__b12",
"type": "int"
},
{
"name": "kA__param__b32",
"type": "int"
},
{
"name": "kA__param__b13",
"type": "int"
},
{
"name": "kA__param__b33",
"type": "int"
},
{
"name": "kA__param__b14",
"type": "int"
},
{
"name": "kA__param__b34",
"type": "int"
},
{
"name": "kA__param__b15",
"type": "int"
},
{
"name": "kA__param__b35",
"type": "int"
},
{
"name": "kA__param__b16",
"type": "int"
},
{
"name": "kA__param__b36",
"type": "int"
},
{
"name": "kA__param__b17",
"type": "int"
},
{
"name": "kA__param__b37",
"type": "int"
},
{
"name": "kA__param__b18",
"type": "int"
},
{
"name": "kA__param__b38",
"type": "int"
},
{
"name": "kA__param__b19",
"type": "int"
},
{
"name": "kA__param__b39",
"type": "int"
}
],
"type": "bool"
},
{
"body": {
"left": {
"left": {
"left": {
"left": {
"left": {
"left": {
"left": "kB__param__a19",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a39",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a21",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kB__param__a10",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a30",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a9",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a29",
"op": "=",
"right": 2
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": "kB__param__a15",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a35",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a4",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a24",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kB__param__a14",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a34",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a5",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a25",
"op": "=",
"right": 2
}
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": "kB__param__a17",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a37",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a2",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a22",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kB__param__a12",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a32",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a7",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a27",
"op": "=",
"right": 2
}
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": {
"left": "kB__param__a18",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a38",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a0",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a20",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kB__param__a11",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a31",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a8",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a28",
"op": "=",
"right": 2
}
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": {
"left": "kB__param__a16",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a36",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a3",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a23",
"op": "=",
"right": 2
}
}
},
"op": "∨",
"right": {
"left": {
"left": {
"left": "kB__param__a13",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a33",
"op": "=",
"right": 2
}
},
"op": "∨",
"right": {
"left": {
"left": "kB__param__a6",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "kB__param__a26",
"op": "=",
"right": 2
}
}
}
}
}
},
"name": "kB",
"parameters": [
{
"name": "kB__param__a0",
"type": "int"
},
{
"name": "kB__param__a20",
"type": "int"
},
{
"name": "kB__param__a1",
"type": "int"
},
{
"name": "kB__param__a21",
"type": "int"
},
{
"name": "kB__param__a2",
"type": "int"
},
{
"name": "kB__param__a22",
"type": "int"
},
{
"name": "kB__param__a3",
"type": "int"
},
{
"name": "kB__param__a23",
"type": "int"
},
{
"name": "kB__param__a4",
"type": "int"
},
{
"name": "kB__param__a24",
"type": "int"
},
{
"name": "kB__param__a5",
"type": "int"
},
{
"name": "kB__param__a25",
"type": "int"
},
{
"name": "kB__param__a6",
"type": "int"
},
{
"name": "kB__param__a26",
"type": "int"
},
{
"name": "kB__param__a7",
"type": "int"
},
{
"name": "kB__param__a27",
"type": "int"
},
{
"name": "kB__param__a8",
"type": "int"
},
{
"name": "kB__param__a28",
"type": "int"
},
{
"name": "kB__param__a9",
"type": "int"
},
{
"name": "kB__param__a29",
"type": "int"
},
{
"name": "kB__param__a10",
"type": "int"
},
{
"name": "kB__param__a30",
"type": "int"
},
{
"name": "kB__param__a11",
"type": "int"
},
{
"name": "kB__param__a31",
"type": "int"
},
{
"name": "kB__param__a12",
"type": "int"
},
{
"name": "kB__param__a32",
"type": "int"
},
{
"name": "kB__param__a13",
"type": "int"
},
{
"name": "kB__param__a33",
"type": "int"
},
{
"name": "kB__param__a14",
"type": "int"
},
{
"name": "kB__param__a34",
"type": "int"
},
{
"name": "kB__param__a15",
"type": "int"
},
{
"name": "kB__param__a35",
"type": "int"
},
{
"name": "kB__param__a16",
"type": "int"
},
{
"name": "kB__param__a36",
"type": "int"
},
{
"name": "kB__param__a17",
"type": "int"
},
{
"name": "kB__param__a37",
"type": "int"
},
{
"name": "kB__param__a18",
"type": "int"
},
{
"name": "kB__param__a38",
"type": "int"
},
{
"name": "kB__param__a19",
"type": "int"
},
{
"name": "kB__param__a39",
"type": "int"
}
],
"type": "bool"
}
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "values",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"exp": {
"left": true,
"op": "U",
"right": {
"left": {
"exp": "knowA",
"op": "¬"
},
"op": "∧",
"right": "knowB"
}
},
"op": "Pmin"
}
},
"name": "unfairA"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "counter"
},
{
"automaton": "partyA"
},
{
"automaton": "partyB"
}
],
"syncs": [
{
"result": "receiveA",
"synchronise": [
"receiveA",
"receiveA",
null
]
},
{
"result": "receiveB",
"synchronise": [
"receiveB",
null,
"receiveB"
]
}
]
},
"type": "dtmc",
"variables": [
{
"initial-value": false,
"name": "knowB",
"transient": true,
"type": "bool"
},
{
"initial-value": false,
"name": "knowA",
"transient": true,
"type": "bool"
},
{
"initial-value": 0,
"name": "n",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 9
}
},
{
"initial-value": 1,
"name": "phase",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 5
}
},
{
"initial-value": 0,
"name": "b0",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b20",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b21",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b22",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b3",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b23",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b4",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b24",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b5",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b25",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b6",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b26",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b7",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b27",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b8",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b28",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b9",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b29",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b10",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b30",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b11",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b31",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b12",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b32",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b13",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b33",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b14",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b34",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b15",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b35",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b16",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b36",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b17",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b37",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b18",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b38",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b19",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "b39",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a0",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a20",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a21",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a22",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a3",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a23",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a4",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a24",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a5",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a25",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a6",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a26",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a7",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a27",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a8",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a28",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a9",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a29",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a10",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a30",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a11",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a31",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a12",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a32",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a13",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a33",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a14",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a34",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a15",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a35",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a16",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a36",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a17",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a37",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a18",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a38",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a19",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "a39",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
}
]
}