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.
// WLAN PROTOCOL (two stations) // discrete time model // gxn/jzs 20/02/02 mdp // COLLISIONS const int COL=0; // maximum number of collisions // TIMING CONSTRAINTS // we have used the FHSS parameters // then scaled by the value of ASLOTTIME const int ASLOTTIME = 1; const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice const int TRANS_TIME_MAX = 10; // scaling up const int TRANS_TIME_MIN = 4; // scaling down const int ACK_TO = 6; const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice // maximum constant used in timing constraints + 1 const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; // CONTENTION WINDOW // CWMIN =15 & CWMAX =255 // this means that MAX_BACKOFF IS 4 const int MAX_BACKOFF = 4; //-----------------------------------------------------------------// // THE MEDIUM/CHANNEL // FORMULAE FOR THE CHANNEL // channel is busy formula busy = c1>0 | c2>0; // channel is free formula free = c1=0 & c2=0; module medium // number of collisions col : [0..COL+1]; // medium status c1 : [0..2]; c2 : [0..2]; // ci corresponds to messages associated with station i // 0 nothing being sent // 1 being sent correctly // 2 being sent garbled // begin sending message and nothing else currently being sent [send1] c1=0 & c2=0 -> (c1'=1); [send2] c2=0 & c1=0 -> (c2'=1); // begin sending message and something is already being sent // in this case both messages become garbled [send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); // finish sending message [finish1] c1>0 -> (c1'=0); [finish2] c2>0 -> (c2'=0); endmodule //-----------------------------------------------------------------// // STATION 1 module station1 // clock for station 1 x1 : [0..TIME_MAX]; // local state s1 : [1..12]; // 1 sense // 2 wait until free before setting backoff // 3 wait for DIFS then set slot // 4 set backoff // 5 backoff // 6 wait until free in backoff // 7 wait for DIFS then resume backoff // 8 vulnerable // 9 transmit // 11 wait for SIFS and then ACK // 10 wait for ACT_TO // 12 done // BACKOFF // separate into slots slot1 : [0..15]; backoff1 : [0..15]; // BACKOFF COUNTER bc1 : [0..MAX_BACKOFF]; // SENSE // let time pass [time] s1=1 & x1(x1'=min(x1+1,TIME_MAX)); // ready to transmit [] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0); // found channel busy so wait until free [] s1=1 & busy -> (s1'=2) & (x1'=0); // WAIT UNTIL FREE BEFORE SETTING BACKOFF // let time pass (no need for the clock x1 to change) [time] s1=2 & busy -> (s1'=2); // find that channel is free so check its free for DIFS before setting backoff [] s1=2 & free -> (s1'=3); // WAIT FOR DIFS THEN SET BACKOFF // let time pass [time] s1=3 & x1 (x1'=min(x1+1,TIME_MAX)); // found channel busy so wait until free [] s1=3 & busy -> (s1'=2) & (x1'=0); // start backoff first uniformly choose slot // backoff counter 0 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)); // backoff counter 1 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); // backoff counter 2 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); // backoff counter 3 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF)); // backoff counter 4 [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) + 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)); // SET BACKOFF (no time can pass) // chosen slot now set backoff [] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 ) + 1/16 : (s1'=5) & (backoff1'=1 ) + 1/16 : (s1'=5) & (backoff1'=2 ) + 1/16 : (s1'=5) & (backoff1'=3 ) + 1/16 : (s1'=5) & (backoff1'=4 ) + 1/16 : (s1'=5) & (backoff1'=5 ) + 1/16 : (s1'=5) & (backoff1'=6 ) + 1/16 : (s1'=5) & (backoff1'=7 ) + 1/16 : (s1'=5) & (backoff1'=8 ) + 1/16 : (s1'=5) & (backoff1'=9 ) + 1/16 : (s1'=5) & (backoff1'=10) + 1/16 : (s1'=5) & (backoff1'=11) + 1/16 : (s1'=5) & (backoff1'=12) + 1/16 : (s1'=5) & (backoff1'=13) + 1/16 : (s1'=5) & (backoff1'=14) + 1/16 : (s1'=5) & (backoff1'=15); // BACKOFF // let time pass [time] s1=5 & x1 (x1'=min(x1+1,TIME_MAX)); // decrement backoff [] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1); [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1); // finish backoff [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0); // found channel busy [] s1=5 & busy -> (s1'=6) & (x1'=0); // WAIT UNTIL FREE IN BACKOFF // let time pass (no need for the clock x1 to change) [time] s1=6 & busy -> (s1'=6); // find that channel is free [] s1=6 & free -> (s1'=7); // WAIT FOR DIFS THEN RESUME BACKOFF // let time pass [time] s1=7 & x1 (x1'=min(x1+1,TIME_MAX)); // resume backoff (start again from previous backoff) [] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0); // found channel busy [] s1=7 & busy -> (s1'=6) & (x1'=0); // VULNERABLE // let time pass [time] s1=8 & x1 (x1'=min(x1+1,TIME_MAX)); // move to transmit [send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0); // TRANSMIT // let time pass [time] s1=9 & x1 (x1'=min(x1+1,TIME_MAX)); // finish transmission successful [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0); // finish transmission garbled [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0); // WAIT FOR SIFS THEN WAIT FOR ACK // WAIT FOR SIFS i.e. c1=0 // check channel and busy: go into backoff [] s1=10 & c1=0 & x1=0 & busy -> (s1'=2); // check channel and free: let time pass [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); // let time pass // following guard is always false as SIFS=1 // [time] s1=10 & c1=0 & x1>0 & x1 (x1'=min(x1+1,TIME_MAX)); // ack is sent after SIFS (since SIFS-1=0 add condition that channel is free) [send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0); // WAIT FOR ACK i.e. c1=1 // let time pass [time] s1=10 & c1=1 & x1 (x1'=min(x1+1,TIME_MAX)); // get acknowledgement so packet sent correctly and move to done [finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0); // WAIT FOR ACK_TO // check channel and busy: go into backoff [] s1=11 & x1=0 & busy -> (s1'=2); // check channel and free: let time pass [time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); // let time pass [time] s1=11 & x1>0 & x1 (x1'=min(x1+1,TIME_MAX)); // no acknowledgement (go to backoff waiting DIFS first) [] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0); // DONE [time] s1=12 -> (s1'=12); endmodule // ---------------------------------------------------------------------------- // // STATION 2 (rename STATION 1) module station2=station1[x1=x2, s1=s2, s2=s1, c1=c2, c2=c1, slot1=slot2, backoff1=backoff2, bc1=bc2, send1=send2, finish1=finish2] endmodule // ---------------------------------------------------------------------------- // label "target" = s1=12 & s2=12;
"sent": P>=1 [ F "target" ];
{
"actions": [
{
"name": "finish1"
},
{
"name": "finish2"
},
{
"name": "send1"
},
{
"name": "send2"
},
{
"name": "time"
}
],
"automata": [
{
"edges": [
{
"action": "finish1",
"destinations": [
{
"assignments": [
{
"comment": "c1 <- 0",
"ref": "c1",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(c1 > 0)",
"exp": {
"left": "c1",
"op": ">",
"right": 0
}
},
"location": "l"
},
{
"action": "finish2",
"destinations": [
{
"assignments": [
{
"comment": "c2 <- 0",
"ref": "c2",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(c2 > 0)",
"exp": {
"left": "c2",
"op": ">",
"right": 0
}
},
"location": "l"
},
{
"action": "send1",
"destinations": [
{
"assignments": [
{
"comment": "c1 <- 1",
"ref": "c1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((c1 = 0) & (c2 = 0))",
"exp": {
"left": {
"left": "c1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "send1",
"destinations": [
{
"assignments": [
{
"comment": "col <- (min((col + 1), 0))",
"ref": "col",
"value": {
"left": {
"left": "col",
"op": "+",
"right": 1
},
"op": "min",
"right": 0
}
},
{
"comment": "c1 <- 2",
"ref": "c1",
"value": 2
},
{
"comment": "c2 <- 2",
"ref": "c2",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((c1 = 0) & (c2 > 0))",
"exp": {
"left": {
"left": "c1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "c2",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"action": "send2",
"destinations": [
{
"assignments": [
{
"comment": "c2 <- 1",
"ref": "c2",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((c2 = 0) & (c1 = 0))",
"exp": {
"left": {
"left": "c2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "send2",
"destinations": [
{
"assignments": [
{
"comment": "col <- (min((col + 1), 0))",
"ref": "col",
"value": {
"left": {
"left": "col",
"op": "+",
"right": 1
},
"op": "min",
"right": 0
}
},
{
"comment": "c1 <- 2",
"ref": "c1",
"value": 2
},
{
"comment": "c2 <- 2",
"ref": "c2",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((c2 = 0) & (c1 > 0))",
"exp": {
"left": {
"left": "c2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "c1",
"op": ">",
"right": 0
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "target <- ((s1 = 12) & (s2 = 12))",
"ref": "target",
"value": {
"left": {
"left": "s1",
"op": "=",
"right": 12
},
"op": "∧",
"right": {
"left": "s2",
"op": "=",
"right": 12
}
}
}
]
}
],
"name": "medium",
"variables": [
{
"initial-value": 0,
"name": "col",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 8",
"ref": "s1",
"value": 8
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 1) & ((x1 = 3) | (x1 = (3 - 1))))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 2
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 2",
"ref": "s1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 1) & busy(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 3",
"ref": "s1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 2) & free(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 2",
"ref": "s1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 3) & busy(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 0",
"ref": "slot1",
"value": 0
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 0))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc1",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 0",
"ref": "slot1",
"value": 0
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 2)",
"exp": {
"left": 1,
"op": "/",
"right": 2
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 1",
"ref": "slot1",
"value": 1
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 2)",
"exp": {
"left": 1,
"op": "/",
"right": 2
}
}
}
],
"guard": {
"comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 1))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc1",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 0",
"ref": "slot1",
"value": 0
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 1",
"ref": "slot1",
"value": 1
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 2",
"ref": "slot1",
"value": 2
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 3",
"ref": "slot1",
"value": 3
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
}
],
"guard": {
"comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc1",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 0",
"ref": "slot1",
"value": 0
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 1",
"ref": "slot1",
"value": 1
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 2",
"ref": "slot1",
"value": 2
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 3",
"ref": "slot1",
"value": 3
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 4",
"ref": "slot1",
"value": 4
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 5",
"ref": "slot1",
"value": 5
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 6",
"ref": "slot1",
"value": 6
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 7",
"ref": "slot1",
"value": 7
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
}
],
"guard": {
"comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 3))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc1",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 0",
"ref": "slot1",
"value": 0
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 1",
"ref": "slot1",
"value": 1
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 2",
"ref": "slot1",
"value": 2
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 3",
"ref": "slot1",
"value": 3
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 4",
"ref": "slot1",
"value": 4
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 5",
"ref": "slot1",
"value": 5
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 6",
"ref": "slot1",
"value": 6
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 7",
"ref": "slot1",
"value": 7
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 8",
"ref": "slot1",
"value": 8
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 9",
"ref": "slot1",
"value": 9
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 10",
"ref": "slot1",
"value": 10
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 11",
"ref": "slot1",
"value": 11
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 12",
"ref": "slot1",
"value": 12
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 13",
"ref": "slot1",
"value": 13
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 14",
"ref": "slot1",
"value": 14
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 4",
"ref": "s1",
"value": 4
},
{
"comment": "slot1 <- 15",
"ref": "slot1",
"value": 15
},
{
"comment": "bc1 <- (min((bc1 + 1), 4))",
"ref": "bc1",
"value": {
"left": {
"left": "bc1",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
}
],
"guard": {
"comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 4))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc1",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 0",
"ref": "backoff1",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 1",
"ref": "backoff1",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 2",
"ref": "backoff1",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 3",
"ref": "backoff1",
"value": 3
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 4",
"ref": "backoff1",
"value": 4
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 5",
"ref": "backoff1",
"value": 5
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 6",
"ref": "backoff1",
"value": 6
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 7",
"ref": "backoff1",
"value": 7
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 8",
"ref": "backoff1",
"value": 8
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 9",
"ref": "backoff1",
"value": 9
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 10",
"ref": "backoff1",
"value": 10
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 11",
"ref": "backoff1",
"value": 11
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 12",
"ref": "backoff1",
"value": 12
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 13",
"ref": "backoff1",
"value": 13
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 14",
"ref": "backoff1",
"value": 14
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- 15",
"ref": "backoff1",
"value": 15
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
}
],
"guard": {
"comment": "(s1 = 4)",
"exp": {
"left": "s1",
"op": "=",
"right": 4
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "backoff1 <- (backoff1 - 1)",
"ref": "backoff1",
"value": {
"left": "backoff1",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 5) & (x1 = 1)) & (backoff1 > 0))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "x1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": "backoff1",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
},
{
"comment": "slot1 <- (slot1 - 1)",
"ref": "slot1",
"value": {
"left": "slot1",
"op": "-",
"right": 1
}
},
{
"comment": "backoff1 <- 15",
"ref": "backoff1",
"value": 15
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s1 = 5) & (x1 = 1)) & (backoff1 = 0)) & (slot1 > 0))",
"exp": {
"left": {
"left": {
"left": "slot1",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "x1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "backoff1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s1",
"op": "=",
"right": 5
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 8",
"ref": "s1",
"value": 8
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s1 = 5) & (x1 = 1)) & (backoff1 = 0)) & (slot1 = 0))",
"exp": {
"left": {
"left": {
"left": "slot1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "x1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "backoff1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s1",
"op": "=",
"right": 5
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 6",
"ref": "s1",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 5) & busy(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 7",
"ref": "s1",
"value": 7
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 6) & free(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 6
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 5",
"ref": "s1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 7) & ((x1 = 3) | (x1 = (3 - 1))))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 2
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 6",
"ref": "s1",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 7) & busy(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 2",
"ref": "s1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s1 = 10) & (c1 = 0)) & (x1 = 0)) & busy(c1, c2))",
"exp": {
"left": {
"left": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s1",
"op": "=",
"right": 10
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 2",
"ref": "s1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 11) & (x1 = 0)) & busy(c1, c2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 3",
"ref": "s1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 11) & (x1 = 6))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x1",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "finish1",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 10",
"ref": "s1",
"value": 10
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 9) & (x1 >= 4)) & (c1 = 1))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "x1",
"op": "≥",
"right": 4
}
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "finish1",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 11",
"ref": "s1",
"value": 11
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 9) & (x1 >= 4)) & (c1 = 2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "x1",
"op": "≥",
"right": 4
}
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "finish1",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 12",
"ref": "s1",
"value": 12
},
{
"comment": "bc1 <- 0",
"ref": "bc1",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 10) & (c1 = 1)) & ((x1 = 4) | (x1 = (4 - 1))))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 4
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 3
}
}
}
},
"location": "l"
},
{
"action": "send1",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 9",
"ref": "s1",
"value": 9
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 8) & ((x1 = 1) | (x1 = (1 - 1))))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 8
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 1
},
"op": "∨",
"right": {
"left": "x1",
"op": "=",
"right": 0
}
}
}
},
"location": "l"
},
{
"action": "send1",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
},
{
"comment": "s1 <- 10",
"ref": "s1",
"value": 10
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 10) & (c1 = 0)) & ((x1 = 1) | ((x1 = (1 - 1)) & free(c1, c2))))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 1
},
"op": "∨",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 1) & (x1 < 3)) & free(c1, c2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 3
}
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 2",
"ref": "s1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 2) & busy(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 3) & (x1 < 3)) & free(c1, c2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 3
}
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 5) & (x1 < 1)) & free(c1, c2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 1
}
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 6",
"ref": "s1",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 6) & busy(c1, c2))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 6
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 7) & (x1 < 3)) & free(c1, c2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 3
}
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 8) & (x1 < 1))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 8
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 1
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((s1 = 9) & (x1 < 10))",
"exp": {
"left": {
"left": "s1",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 10
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s1 = 10) & (c1 = 0)) & (x1 = 0)) & free(c1, c2))",
"exp": {
"left": {
"left": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "x1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s1",
"op": "=",
"right": 10
}
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 10) & (c1 = 1)) & (x1 < 4))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "c1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 4
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 11) & (x1 = 0)) & free(c1, c2))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"args": [
"c1",
"c2"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- (min((x1 + 1), 11))",
"ref": "x1",
"value": {
"left": {
"left": "x1",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s1 = 11) & (x1 > 0)) & (x1 < 6))",
"exp": {
"left": {
"left": {
"left": "s1",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x1",
"op": ">",
"right": 0
}
},
"op": "∧",
"right": {
"left": "x1",
"op": "<",
"right": 6
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 12",
"ref": "s1",
"value": 12
}
],
"location": "l"
}
],
"guard": {
"comment": "(s1 = 12)",
"exp": {
"left": "s1",
"op": "=",
"right": 12
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station1",
"variables": [
{
"initial-value": 0,
"name": "x1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 11
}
},
{
"initial-value": 0,
"name": "slot1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 15
}
},
{
"initial-value": 0,
"name": "backoff1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 15
}
},
{
"initial-value": 0,
"name": "bc1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 8",
"ref": "s2",
"value": 8
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 1) & ((x2 = 3) | (x2 = (3 - 1))))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 2
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 2",
"ref": "s2",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 1) & busy(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 3",
"ref": "s2",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 2) & free(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 2",
"ref": "s2",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 3) & busy(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 0",
"ref": "slot2",
"value": 0
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 0))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc2",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 0",
"ref": "slot2",
"value": 0
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 2)",
"exp": {
"left": 1,
"op": "/",
"right": 2
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 1",
"ref": "slot2",
"value": 1
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 2)",
"exp": {
"left": 1,
"op": "/",
"right": 2
}
}
}
],
"guard": {
"comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc2",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 0",
"ref": "slot2",
"value": 0
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 1",
"ref": "slot2",
"value": 1
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 2",
"ref": "slot2",
"value": 2
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 3",
"ref": "slot2",
"value": 3
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 4)",
"exp": {
"left": 1,
"op": "/",
"right": 4
}
}
}
],
"guard": {
"comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 2))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc2",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 0",
"ref": "slot2",
"value": 0
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 1",
"ref": "slot2",
"value": 1
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 2",
"ref": "slot2",
"value": 2
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 3",
"ref": "slot2",
"value": 3
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 4",
"ref": "slot2",
"value": 4
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 5",
"ref": "slot2",
"value": 5
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 6",
"ref": "slot2",
"value": 6
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 7",
"ref": "slot2",
"value": 7
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 8)",
"exp": {
"left": 1,
"op": "/",
"right": 8
}
}
}
],
"guard": {
"comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 3))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc2",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 0",
"ref": "slot2",
"value": 0
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 1",
"ref": "slot2",
"value": 1
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 2",
"ref": "slot2",
"value": 2
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 3",
"ref": "slot2",
"value": 3
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 4",
"ref": "slot2",
"value": 4
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 5",
"ref": "slot2",
"value": 5
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 6",
"ref": "slot2",
"value": 6
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 7",
"ref": "slot2",
"value": 7
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 8",
"ref": "slot2",
"value": 8
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 9",
"ref": "slot2",
"value": 9
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 10",
"ref": "slot2",
"value": 10
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 11",
"ref": "slot2",
"value": 11
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 12",
"ref": "slot2",
"value": 12
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 13",
"ref": "slot2",
"value": 13
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 14",
"ref": "slot2",
"value": 14
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 4",
"ref": "s2",
"value": 4
},
{
"comment": "slot2 <- 15",
"ref": "slot2",
"value": 15
},
{
"comment": "bc2 <- (min((bc2 + 1), 4))",
"ref": "bc2",
"value": {
"left": {
"left": "bc2",
"op": "+",
"right": 1
},
"op": "min",
"right": 4
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
}
],
"guard": {
"comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 4))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 2
}
}
},
"op": "∧",
"right": {
"left": "bc2",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 0",
"ref": "backoff2",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 1",
"ref": "backoff2",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 2",
"ref": "backoff2",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 3",
"ref": "backoff2",
"value": 3
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 4",
"ref": "backoff2",
"value": 4
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 5",
"ref": "backoff2",
"value": 5
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 6",
"ref": "backoff2",
"value": 6
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 7",
"ref": "backoff2",
"value": 7
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 8",
"ref": "backoff2",
"value": 8
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 9",
"ref": "backoff2",
"value": 9
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 10",
"ref": "backoff2",
"value": 10
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 11",
"ref": "backoff2",
"value": 11
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 12",
"ref": "backoff2",
"value": 12
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 13",
"ref": "backoff2",
"value": 13
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 14",
"ref": "backoff2",
"value": 14
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
},
{
"assignments": [
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- 15",
"ref": "backoff2",
"value": 15
}
],
"location": "l",
"probability": {
"comment": "(1 / 16)",
"exp": {
"left": 1,
"op": "/",
"right": 16
}
}
}
],
"guard": {
"comment": "(s2 = 4)",
"exp": {
"left": "s2",
"op": "=",
"right": 4
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "backoff2 <- (backoff2 - 1)",
"ref": "backoff2",
"value": {
"left": "backoff2",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 5) & (x2 = 1)) & (backoff2 > 0))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "x2",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": "backoff2",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
},
{
"comment": "slot2 <- (slot2 - 1)",
"ref": "slot2",
"value": {
"left": "slot2",
"op": "-",
"right": 1
}
},
{
"comment": "backoff2 <- 15",
"ref": "backoff2",
"value": 15
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s2 = 5) & (x2 = 1)) & (backoff2 = 0)) & (slot2 > 0))",
"exp": {
"left": {
"left": {
"left": "slot2",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "x2",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "backoff2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s2",
"op": "=",
"right": 5
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 8",
"ref": "s2",
"value": 8
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s2 = 5) & (x2 = 1)) & (backoff2 = 0)) & (slot2 = 0))",
"exp": {
"left": {
"left": {
"left": "slot2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "x2",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "backoff2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s2",
"op": "=",
"right": 5
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 6",
"ref": "s2",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 5) & busy(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 7",
"ref": "s2",
"value": 7
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 6) & free(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 6
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 5",
"ref": "s2",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 7) & ((x2 = 3) | (x2 = (3 - 1))))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 3
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 2
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 6",
"ref": "s2",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 7) & busy(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 2",
"ref": "s2",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s2 = 10) & (c2 = 0)) & (x2 = 0)) & busy(c2, c1))",
"exp": {
"left": {
"left": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s2",
"op": "=",
"right": 10
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 2",
"ref": "s2",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 11) & (x2 = 0)) & busy(c2, c1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 3",
"ref": "s2",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 11) & (x2 = 6))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x2",
"op": "=",
"right": 6
}
}
},
"location": "l"
},
{
"action": "finish2",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 10",
"ref": "s2",
"value": 10
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 9) & (x2 >= 4)) & (c2 = 1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "x2",
"op": "≥",
"right": 4
}
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "finish2",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 11",
"ref": "s2",
"value": 11
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 9) & (x2 >= 4)) & (c2 = 2))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "x2",
"op": "≥",
"right": 4
}
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "finish2",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 12",
"ref": "s2",
"value": 12
},
{
"comment": "bc2 <- 0",
"ref": "bc2",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 10) & (c2 = 1)) & ((x2 = 4) | (x2 = (4 - 1))))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 4
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 3
}
}
}
},
"location": "l"
},
{
"action": "send2",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 9",
"ref": "s2",
"value": 9
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 8) & ((x2 = 1) | (x2 = (1 - 1))))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 8
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 1
},
"op": "∨",
"right": {
"left": "x2",
"op": "=",
"right": 0
}
}
}
},
"location": "l"
},
{
"action": "send2",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
},
{
"comment": "s2 <- 10",
"ref": "s2",
"value": 10
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 10) & (c2 = 0)) & ((x2 = 1) | ((x2 = (1 - 1)) & free(c2, c1))))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 1
},
"op": "∨",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 1) & (x2 < 3)) & free(c2, c1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 3
}
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 2",
"ref": "s2",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 2) & busy(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 3) & (x2 < 3)) & free(c2, c1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 3
}
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 5) & (x2 < 1)) & free(c2, c1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 1
}
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 6",
"ref": "s2",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 6) & busy(c2, c1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 6
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "busy",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 7) & (x2 < 3)) & free(c2, c1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 3
}
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 8) & (x2 < 1))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 8
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 1
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((s2 = 9) & (x2 < 10))",
"exp": {
"left": {
"left": "s2",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 10
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((((s2 = 10) & (c2 = 0)) & (x2 = 0)) & free(c2, c1))",
"exp": {
"left": {
"left": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "x2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "s2",
"op": "=",
"right": 10
}
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 10) & (c2 = 1)) & (x2 < 4))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "c2",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 4
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 11) & (x2 = 0)) & free(c2, c1))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"args": [
"c2",
"c1"
],
"function": "free",
"op": "call"
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- (min((x2 + 1), 11))",
"ref": "x2",
"value": {
"left": {
"left": "x2",
"op": "+",
"right": 1
},
"op": "min",
"right": 11
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s2 = 11) & (x2 > 0)) & (x2 < 6))",
"exp": {
"left": {
"left": {
"left": "s2",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "x2",
"op": ">",
"right": 0
}
},
"op": "∧",
"right": {
"left": "x2",
"op": "<",
"right": 6
}
}
},
"location": "l"
},
{
"action": "time",
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 12",
"ref": "s2",
"value": 12
}
],
"location": "l"
}
],
"guard": {
"comment": "(s2 = 12)",
"exp": {
"left": "s2",
"op": "=",
"right": 12
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station2",
"variables": [
{
"initial-value": 0,
"name": "x2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 11
}
},
{
"initial-value": 0,
"name": "slot2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 15
}
},
{
"initial-value": 0,
"name": "backoff2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 15
}
},
{
"initial-value": 0,
"name": "bc2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
}
]
}
],
"constants": [
{
"name": "COL",
"type": "int",
"value": 0
},
{
"name": "ASLOTTIME",
"type": "int",
"value": 1
},
{
"name": "DIFS",
"type": "int",
"value": 3
},
{
"name": "VULN",
"type": "int",
"value": 1
},
{
"name": "TRANS_TIME_MAX",
"type": "int",
"value": 10
},
{
"name": "TRANS_TIME_MIN",
"type": "int",
"value": 4
},
{
"name": "ACK_TO",
"type": "int",
"value": 6
},
{
"name": "ACK",
"type": "int",
"value": 4
},
{
"name": "SIFS",
"type": "int",
"value": 1
},
{
"name": "TIME_MAX",
"type": "int",
"value": 11
},
{
"name": "MAX_BACKOFF",
"type": "int",
"value": 4
}
],
"features": [
"derived-operators",
"functions"
],
"functions": [
{
"body": {
"left": {
"left": "free__param__c1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "free__param__c2",
"op": "=",
"right": 0
}
},
"name": "free",
"parameters": [
{
"name": "free__param__c1",
"type": "int"
},
{
"name": "free__param__c2",
"type": "int"
}
],
"type": "bool"
},
{
"body": {
"left": {
"left": "busy__param__c1",
"op": ">",
"right": 0
},
"op": "∨",
"right": {
"left": "busy__param__c2",
"op": ">",
"right": 0
}
},
"name": "busy",
"parameters": [
{
"name": "busy__param__c1",
"type": "int"
},
{
"name": "busy__param__c2",
"type": "int"
}
],
"type": "bool"
}
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "values",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"left": {
"exp": {
"left": true,
"op": "U",
"right": "target"
},
"op": "Pmin"
},
"op": "≥",
"right": 1
}
},
"name": "sent"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "medium"
},
{
"automaton": "station1"
},
{
"automaton": "station2"
}
],
"syncs": [
{
"result": "finish1",
"synchronise": [
"finish1",
"finish1",
null
]
},
{
"result": "finish2",
"synchronise": [
"finish2",
null,
"finish2"
]
},
{
"result": "send1",
"synchronise": [
"send1",
"send1",
null
]
},
{
"result": "send2",
"synchronise": [
"send2",
null,
"send2"
]
},
{
"result": "time",
"synchronise": [
null,
"time",
"time"
]
}
]
},
"type": "mdp",
"variables": [
{
"initial-value": false,
"name": "target",
"transient": true,
"type": "bool"
},
{
"initial-value": 0,
"name": "c1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "c2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 1,
"name": "s1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 12
}
},
{
"initial-value": 1,
"name": "s2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 12
}
}
]
}