model.prism (0.01 MB)
property.props (0.01 MB)
model.jani (0.18 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.

// CSMA/CD protocol - probabilistic version of kronos model (3 stations)
// gxn/dxp 04/12/01

mdp

// note made changes since cannot have strict inequalities
// in digital clocks approach and suppose a station only sends one message

// simplified parameters scaled
const int sigma=1; // time for messages to propagate along the bus
const int lambda=30; // time to send a message

// actual parameters
const int N = 3; // number of processes
const int K = 4; // exponential backoff limit
const int slot = 2*sigma; // length of slot
const int M = floor(pow(2, K))-1 ; // max number of slots to wait
//const int lambda=782;
//const int sigma=26;

//----------------------------------------------------------------------------------------------------------------------------
// the bus
module bus
	
	b : [0..2];
	// b=0 - idle
	// b=1 - active
	// b=2 - collision
	
	// clocks of bus
	y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy)
	y2 : [0..sigma+1]; // time since second send (used to find time until collision detected)
	
	// a sender sends (ok - no other message being sent)
	[send1] (b=0) -> (b'=1);
	[send2] (b=0) -> (b'=1);
	[send3] (b=0) -> (b'=1);
	
	// a sender sends (bus busy - collision)
	[send1] (b=1|b=2) & (y1 (b'=2);
	[send2] (b=1|b=2) & (y1 (b'=2);
	[send3] (b=1|b=2) & (y1 (b'=2);
	
	// finish sending
	[end1] (b=1) -> (b'=0) & (y1'=0);
	[end2] (b=1) -> (b'=0) & (y1'=0);
	[end3] (b=1) -> (b'=0) & (y1'=0);
	
	// bus busy
	[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
	[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
	[busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
	
	// collision detected
	[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0);
	
	// time passage
	[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0
	[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1
	[time] (b=2) & (y2 (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected)
	
endmodule

//----------------------------------------------------------------------------------------------------------------------------
// model of first sender
module station1
	
	// LOCAL STATE
	s1 : [0..5];
	// s1=0 - initial state
	// s1=1 - transmit
	// s1=2 - collision (set backoff)
	// s1=3 - wait (bus busy)
	// s1=4 - successfully sent
	
	// LOCAL CLOCK
	x1 : [0..max(lambda,slot)];
	
	// BACKOFF COUNTER (number of slots to wait)
	bc1 : [0..M];
	
	// COLLISION COUNTER
	cd1 : [0..K];
	
	// start sending
	[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
	[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
	
	// transmitting
	[time] (s1=1) & (x1 (x1'=min(x1+1,lambda)); // let time pass
	[end1]  (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
	[cd]   (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter)
	[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important
	
	// set backoff (no time can pass in this state)
	// probability depends on which transmission this is (cd1)
	[] s1=2 & cd1=1 ->  1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ;
	[] s1=2 & cd1=2 ->  1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ;
	[] s1=2 & cd1=3 ->  1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ;
	[] s1=2 & cd1=4 ->  1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ;
	
	// wait until backoff counter reaches 0 then send again
	[time] (s1=3) & (x1 (x1'=x1+1); // let time pass (in slot)
	[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots)
	[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free)
	[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy)
	
	// once finished nothing matters
	[time] (s1>=4) -> (x1'=0);

endmodule

//----------------------------------------------------------------------------------------------------------------------------

// construct further stations through renaming
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule

//----------------------------------------------------------------------------------------------------------------------------

// labels/formulae
label "all_delivered" = s1=4&s2=4&s3=4;
label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2);

"all_before_max": Pmax=? [ !"collision_max_backoff" U "all_delivered" ];

{
    "actions": [
        {
            "name": "busy1"
        },
        {
            "name": "busy2"
        },
        {
            "name": "busy3"
        },
        {
            "name": "cd"
        },
        {
            "name": "end1"
        },
        {
            "name": "end2"
        },
        {
            "name": "end3"
        },
        {
            "name": "send1"
        },
        {
            "name": "send2"
        },
        {
            "name": "send3"
        },
        {
            "name": "time"
        }
    ],
    "automata": [
        {
            "edges": [
                {
                    "action": "busy1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- b",
                                    "ref": "b",
                                    "value": "b"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((b = 1) | (b = 2)) & (y1 >= 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "≥",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- b",
                                    "ref": "b",
                                    "value": "b"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((b = 1) | (b = 2)) & (y1 >= 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "≥",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- b",
                                    "ref": "b",
                                    "value": "b"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((b = 1) | (b = 2)) & (y1 >= 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "≥",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "cd",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 0",
                                    "ref": "b",
                                    "value": 0
                                },
                                {
                                    "comment": "y1 <- 0",
                                    "ref": "y1",
                                    "value": 0
                                },
                                {
                                    "comment": "y2 <- 0",
                                    "ref": "y2",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((b = 2) & (y2 <= 1))",
                        "exp": {
                            "left": {
                                "left": "b",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "y2",
                                "op": "≤",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "end1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 0",
                                    "ref": "b",
                                    "value": 0
                                },
                                {
                                    "comment": "y1 <- 0",
                                    "ref": "y1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 1)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "end2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 0",
                                    "ref": "b",
                                    "value": 0
                                },
                                {
                                    "comment": "y1 <- 0",
                                    "ref": "y1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 1)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "end3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 0",
                                    "ref": "b",
                                    "value": 0
                                },
                                {
                                    "comment": "y1 <- 0",
                                    "ref": "y1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 1)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 1",
                                    "ref": "b",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 0)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 2",
                                    "ref": "b",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((b = 1) | (b = 2)) & (y1 < 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "<",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 1",
                                    "ref": "b",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 0)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 2",
                                    "ref": "b",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((b = 1) | (b = 2)) & (y1 < 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "<",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 1",
                                    "ref": "b",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 0)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "b <- 2",
                                    "ref": "b",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((b = 1) | (b = 2)) & (y1 < 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "b",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "y1",
                                "op": "<",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- 0",
                                    "ref": "y1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 0)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- (min((y1 + 1), 2))",
                                    "ref": "y1",
                                    "value": {
                                        "left": {
                                            "left": "y1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 2
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(b = 1)",
                        "exp": {
                            "left": "b",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "y1 <- (min((y1 + 1), 2))",
                                    "ref": "y1",
                                    "value": {
                                        "left": {
                                            "left": "y1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 2
                                    }
                                },
                                {
                                    "comment": "y2 <- (min((y2 + 1), 2))",
                                    "ref": "y2",
                                    "value": {
                                        "left": {
                                            "left": "y2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 2
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((b = 2) & (y2 < 1))",
                        "exp": {
                            "left": {
                                "left": "b",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "y2",
                                "op": "<",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l",
                    "transient-values": [
                        {
                            "comment": "all_delivered <- (((s1 = 4) & (s2 = 4)) & (s3 = 4))",
                            "ref": "all_delivered",
                            "value": {
                                "left": {
                                    "left": {
                                        "left": "s1",
                                        "op": "=",
                                        "right": 4
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "s2",
                                        "op": "=",
                                        "right": 4
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s3",
                                    "op": "=",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "comment": "collision_max_backoff <- (((((cd1 = 4) & (s1 = 1)) & (b = 2)) | (((cd2 = 4) & (s2 = 1)) & (b = 2))) | (((cd3 = 4) & (s3 = 1)) & (b = 2)))",
                            "ref": "collision_max_backoff",
                            "value": {
                                "left": {
                                    "left": {
                                        "left": {
                                            "left": {
                                                "left": "cd1",
                                                "op": "=",
                                                "right": 4
                                            },
                                            "op": "∧",
                                            "right": {
                                                "left": "s1",
                                                "op": "=",
                                                "right": 1
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "b",
                                            "op": "=",
                                            "right": 2
                                        }
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": {
                                            "left": {
                                                "left": "cd2",
                                                "op": "=",
                                                "right": 4
                                            },
                                            "op": "∧",
                                            "right": {
                                                "left": "s2",
                                                "op": "=",
                                                "right": 1
                                            }
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "b",
                                            "op": "=",
                                            "right": 2
                                        }
                                    }
                                },
                                "op": "∨",
                                "right": {
                                    "left": {
                                        "left": {
                                            "left": "cd3",
                                            "op": "=",
                                            "right": 4
                                        },
                                        "op": "∧",
                                        "right": {
                                            "left": "s3",
                                            "op": "=",
                                            "right": 1
                                        }
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "b",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            }
                        }
                    ]
                }
            ],
            "name": "bus",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "y1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 2
                    }
                },
                {
                    "initial-value": 0,
                    "name": "y2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 2
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 0",
                                    "ref": "bc1",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 1",
                                    "ref": "bc1",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 2) & (cd1 = 1))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd1",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 0",
                                    "ref": "bc1",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 1",
                                    "ref": "bc1",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 2",
                                    "ref": "bc1",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 3",
                                    "ref": "bc1",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 2) & (cd1 = 2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd1",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 0",
                                    "ref": "bc1",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 1",
                                    "ref": "bc1",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 2",
                                    "ref": "bc1",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 3",
                                    "ref": "bc1",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 4",
                                    "ref": "bc1",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 5",
                                    "ref": "bc1",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 6",
                                    "ref": "bc1",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 7",
                                    "ref": "bc1",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 2) & (cd1 = 3))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd1",
                                "op": "=",
                                "right": 3
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 0",
                                    "ref": "bc1",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 1",
                                    "ref": "bc1",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 2",
                                    "ref": "bc1",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 3",
                                    "ref": "bc1",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 4",
                                    "ref": "bc1",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 5",
                                    "ref": "bc1",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 6",
                                    "ref": "bc1",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 7",
                                    "ref": "bc1",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 8",
                                    "ref": "bc1",
                                    "value": 8
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 9",
                                    "ref": "bc1",
                                    "value": 9
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 10",
                                    "ref": "bc1",
                                    "value": 10
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 11",
                                    "ref": "bc1",
                                    "value": 11
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 12",
                                    "ref": "bc1",
                                    "value": 12
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 13",
                                    "ref": "bc1",
                                    "value": 13
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 14",
                                    "ref": "bc1",
                                    "value": 14
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- 15",
                                    "ref": "bc1",
                                    "value": 15
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 2) & (cd1 = 4))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd1",
                                "op": "=",
                                "right": 4
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                },
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "cd1 <- (min(4, (cd1 + 1)))",
                                    "ref": "cd1",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd1",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s1 = 0)",
                        "exp": {
                            "left": "s1",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                },
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "cd1 <- (min(4, (cd1 + 1)))",
                                    "ref": "cd1",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd1",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & (x1 = (2 * 1))) & (bc1 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "cd",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                },
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "cd1 <- (min(4, (cd1 + 1)))",
                                    "ref": "cd1",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd1",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s1 = 1)",
                        "exp": {
                            "left": "s1",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "cd",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- s1",
                                    "ref": "s1",
                                    "value": "s1"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "!((s1 = 1))",
                        "exp": {
                            "exp": {
                                "left": "s1",
                                "op": "=",
                                "right": 1
                            },
                            "op": "¬"
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "end1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 1) & (x1 = 30))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "=",
                                "right": 30
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 1",
                                    "ref": "s1",
                                    "value": 1
                                },
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s1 = 0)",
                        "exp": {
                            "left": "s1",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 1",
                                    "ref": "s1",
                                    "value": 1
                                },
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & (x1 = (2 * 1))) & (bc1 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 30))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 30
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 1) & (x1 < 30))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "<",
                                "right": 30
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (x1 + 1)",
                                    "ref": "x1",
                                    "value": {
                                        "left": "x1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 3) & (x1 < (2 * 1)))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 3
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "<",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 1",
                                    "ref": "x1",
                                    "value": 1
                                },
                                {
                                    "comment": "bc1 <- (bc1 - 1)",
                                    "ref": "bc1",
                                    "value": {
                                        "left": "bc1",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & (x1 = (2 * 1))) & (bc1 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s1 >= 4)",
                        "exp": {
                            "left": "s1",
                            "op": "≥",
                            "right": 4
                        }
                    },
                    "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": 30
                    }
                },
                {
                    "initial-value": 0,
                    "name": "bc1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 15
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 0",
                                    "ref": "bc2",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 1",
                                    "ref": "bc2",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 2) & (cd2 = 1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd2",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 0",
                                    "ref": "bc2",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 1",
                                    "ref": "bc2",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 2",
                                    "ref": "bc2",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 3",
                                    "ref": "bc2",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 2) & (cd2 = 2))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd2",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 0",
                                    "ref": "bc2",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 1",
                                    "ref": "bc2",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 2",
                                    "ref": "bc2",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 3",
                                    "ref": "bc2",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 4",
                                    "ref": "bc2",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 5",
                                    "ref": "bc2",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 6",
                                    "ref": "bc2",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 7",
                                    "ref": "bc2",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 2) & (cd2 = 3))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd2",
                                "op": "=",
                                "right": 3
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 0",
                                    "ref": "bc2",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 1",
                                    "ref": "bc2",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 2",
                                    "ref": "bc2",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 3",
                                    "ref": "bc2",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 4",
                                    "ref": "bc2",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 5",
                                    "ref": "bc2",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 6",
                                    "ref": "bc2",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 7",
                                    "ref": "bc2",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 8",
                                    "ref": "bc2",
                                    "value": 8
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 9",
                                    "ref": "bc2",
                                    "value": 9
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 10",
                                    "ref": "bc2",
                                    "value": 10
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 11",
                                    "ref": "bc2",
                                    "value": 11
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 12",
                                    "ref": "bc2",
                                    "value": 12
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 13",
                                    "ref": "bc2",
                                    "value": 13
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 14",
                                    "ref": "bc2",
                                    "value": 14
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- 15",
                                    "ref": "bc2",
                                    "value": 15
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 2) & (cd2 = 4))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd2",
                                "op": "=",
                                "right": 4
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                },
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "cd2 <- (min(4, (cd2 + 1)))",
                                    "ref": "cd2",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd2",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s2 = 0)",
                        "exp": {
                            "left": "s2",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                },
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "cd2 <- (min(4, (cd2 + 1)))",
                                    "ref": "cd2",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd2",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & (x2 = (2 * 1))) & (bc2 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "cd",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                },
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "cd2 <- (min(4, (cd2 + 1)))",
                                    "ref": "cd2",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd2",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s2 = 1)",
                        "exp": {
                            "left": "s2",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "cd",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- s2",
                                    "ref": "s2",
                                    "value": "s2"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "!((s2 = 1))",
                        "exp": {
                            "exp": {
                                "left": "s2",
                                "op": "=",
                                "right": 1
                            },
                            "op": "¬"
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "end2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 1) & (x2 = 30))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "=",
                                "right": 30
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 1",
                                    "ref": "s2",
                                    "value": 1
                                },
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s2 = 0)",
                        "exp": {
                            "left": "s2",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 1",
                                    "ref": "s2",
                                    "value": 1
                                },
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & (x2 = (2 * 1))) & (bc2 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 30))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 30
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 1) & (x2 < 30))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "<",
                                "right": 30
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (x2 + 1)",
                                    "ref": "x2",
                                    "value": {
                                        "left": "x2",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 3) & (x2 < (2 * 1)))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 3
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "<",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 1",
                                    "ref": "x2",
                                    "value": 1
                                },
                                {
                                    "comment": "bc2 <- (bc2 - 1)",
                                    "ref": "bc2",
                                    "value": {
                                        "left": "bc2",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & (x2 = (2 * 1))) & (bc2 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s2 >= 4)",
                        "exp": {
                            "left": "s2",
                            "op": "≥",
                            "right": 4
                        }
                    },
                    "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": 30
                    }
                },
                {
                    "initial-value": 0,
                    "name": "bc2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 15
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 0",
                                    "ref": "bc3",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 1",
                                    "ref": "bc3",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s3 = 2) & (cd3 = 1))",
                        "exp": {
                            "left": {
                                "left": "s3",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd3",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 0",
                                    "ref": "bc3",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 1",
                                    "ref": "bc3",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 2",
                                    "ref": "bc3",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 3",
                                    "ref": "bc3",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s3 = 2) & (cd3 = 2))",
                        "exp": {
                            "left": {
                                "left": "s3",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd3",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 0",
                                    "ref": "bc3",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 1",
                                    "ref": "bc3",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 2",
                                    "ref": "bc3",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 3",
                                    "ref": "bc3",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 4",
                                    "ref": "bc3",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 5",
                                    "ref": "bc3",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 6",
                                    "ref": "bc3",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 7",
                                    "ref": "bc3",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s3 = 2) & (cd3 = 3))",
                        "exp": {
                            "left": {
                                "left": "s3",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd3",
                                "op": "=",
                                "right": 3
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 0",
                                    "ref": "bc3",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 1",
                                    "ref": "bc3",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 2",
                                    "ref": "bc3",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 3",
                                    "ref": "bc3",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 4",
                                    "ref": "bc3",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 5",
                                    "ref": "bc3",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 6",
                                    "ref": "bc3",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 7",
                                    "ref": "bc3",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 8",
                                    "ref": "bc3",
                                    "value": 8
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 9",
                                    "ref": "bc3",
                                    "value": 9
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 10",
                                    "ref": "bc3",
                                    "value": 10
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 11",
                                    "ref": "bc3",
                                    "value": 11
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 12",
                                    "ref": "bc3",
                                    "value": 12
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 13",
                                    "ref": "bc3",
                                    "value": 13
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 14",
                                    "ref": "bc3",
                                    "value": 14
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 3",
                                    "ref": "s3",
                                    "value": 3
                                },
                                {
                                    "comment": "bc3 <- 15",
                                    "ref": "bc3",
                                    "value": 15
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s3 = 2) & (cd3 = 4))",
                        "exp": {
                            "left": {
                                "left": "s3",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "cd3",
                                "op": "=",
                                "right": 4
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 2",
                                    "ref": "s3",
                                    "value": 2
                                },
                                {
                                    "comment": "x3 <- 0",
                                    "ref": "x3",
                                    "value": 0
                                },
                                {
                                    "comment": "cd3 <- (min(4, (cd3 + 1)))",
                                    "ref": "cd3",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd3",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s3 = 0)",
                        "exp": {
                            "left": "s3",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "busy3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 2",
                                    "ref": "s3",
                                    "value": 2
                                },
                                {
                                    "comment": "x3 <- 0",
                                    "ref": "x3",
                                    "value": 0
                                },
                                {
                                    "comment": "cd3 <- (min(4, (cd3 + 1)))",
                                    "ref": "cd3",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd3",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s3 = 3) & (x3 = (2 * 1))) & (bc3 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s3",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x3",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc3",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "cd",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 2",
                                    "ref": "s3",
                                    "value": 2
                                },
                                {
                                    "comment": "x3 <- 0",
                                    "ref": "x3",
                                    "value": 0
                                },
                                {
                                    "comment": "cd3 <- (min(4, (cd3 + 1)))",
                                    "ref": "cd3",
                                    "value": {
                                        "left": 4,
                                        "op": "min",
                                        "right": {
                                            "left": "cd3",
                                            "op": "+",
                                            "right": 1
                                        }
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s3 = 1)",
                        "exp": {
                            "left": "s3",
                            "op": "=",
                            "right": 1
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "cd",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- s3",
                                    "ref": "s3",
                                    "value": "s3"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "!((s3 = 1))",
                        "exp": {
                            "exp": {
                                "left": "s3",
                                "op": "=",
                                "right": 1
                            },
                            "op": "¬"
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "end3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 4",
                                    "ref": "s3",
                                    "value": 4
                                },
                                {
                                    "comment": "x3 <- 0",
                                    "ref": "x3",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s3 = 1) & (x3 = 30))",
                        "exp": {
                            "left": {
                                "left": "s3",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": "x3",
                                "op": "=",
                                "right": 30
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 1",
                                    "ref": "s3",
                                    "value": 1
                                },
                                {
                                    "comment": "x3 <- 0",
                                    "ref": "x3",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s3 = 0)",
                        "exp": {
                            "left": "s3",
                            "op": "=",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s3 <- 1",
                                    "ref": "s3",
                                    "value": 1
                                },
                                {
                                    "comment": "x3 <- 0",
                                    "ref": "x3",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s3 = 3) & (x3 = (2 * 1))) & (bc3 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s3",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x3",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc3",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x3 <- (min((x3 + 1), 30))",
                                    "ref": "x3",
                                    "value": {
                                        "left": {
                                            "left": "x3",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 30
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s3 = 1) & (x3 < 30))",
                        "exp": {
                            "left": {
                                "left": "s3",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": "x3",
                                "op": "<",
                                "right": 30
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x3 <- (x3 + 1)",
                                    "ref": "x3",
                                    "value": {
                                        "left": "x3",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s3 = 3) & (x3 < (2 * 1)))",
                        "exp": {
                            "left": {
                                "left": "s3",
                                "op": "=",
                                "right": 3
                            },
                            "op": "∧",
                            "right": {
                                "left": "x3",
                                "op": "<",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x3 <- 1",
                                    "ref": "x3",
                                    "value": 1
                                },
                                {
                                    "comment": "bc3 <- (bc3 - 1)",
                                    "ref": "bc3",
                                    "value": {
                                        "left": "bc3",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s3 = 3) & (x3 = (2 * 1))) & (bc3 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s3",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x3",
                                    "op": "=",
                                    "right": 2
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc3",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x3 <- 0",
                                    "ref": "x3",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s3 >= 4)",
                        "exp": {
                            "left": "s3",
                            "op": "≥",
                            "right": 4
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "station3",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "x3",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 30
                    }
                },
                {
                    "initial-value": 0,
                    "name": "bc3",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 15
                    }
                }
            ]
        }
    ],
    "constants": [
        {
            "name": "sigma",
            "type": "int",
            "value": 1
        },
        {
            "name": "lambda",
            "type": "int",
            "value": 30
        },
        {
            "name": "N",
            "type": "int",
            "value": 3
        },
        {
            "name": "K",
            "type": "int",
            "value": 4
        },
        {
            "name": "slot",
            "type": "int",
            "value": 2
        },
        {
            "name": "M",
            "type": "int",
            "value": 15
        }
    ],
    "features": [
        "derived-operators"
    ],
    "jani-version": 1,
    "name": "model",
    "properties": [
        {
            "expression": {
                "fun": "values",
                "op": "filter",
                "states": {
                    "op": "initial"
                },
                "values": {
                    "exp": {
                        "left": {
                            "exp": "collision_max_backoff",
                            "op": "¬"
                        },
                        "op": "U",
                        "right": "all_delivered"
                    },
                    "op": "Pmax"
                }
            },
            "name": "all_before_max"
        }
    ],
    "restrict-initial": {
        "exp": true
    },
    "system": {
        "elements": [
            {
                "automaton": "bus"
            },
            {
                "automaton": "station1"
            },
            {
                "automaton": "station2"
            },
            {
                "automaton": "station3"
            }
        ],
        "syncs": [
            {
                "result": "busy1",
                "synchronise": [
                    "busy1",
                    "busy1",
                    null,
                    null
                ]
            },
            {
                "result": "busy2",
                "synchronise": [
                    "busy2",
                    null,
                    "busy2",
                    null
                ]
            },
            {
                "result": "busy3",
                "synchronise": [
                    "busy3",
                    null,
                    null,
                    "busy3"
                ]
            },
            {
                "result": "cd",
                "synchronise": [
                    "cd",
                    "cd",
                    "cd",
                    "cd"
                ]
            },
            {
                "result": "end1",
                "synchronise": [
                    "end1",
                    "end1",
                    null,
                    null
                ]
            },
            {
                "result": "end2",
                "synchronise": [
                    "end2",
                    null,
                    "end2",
                    null
                ]
            },
            {
                "result": "end3",
                "synchronise": [
                    "end3",
                    null,
                    null,
                    "end3"
                ]
            },
            {
                "result": "send1",
                "synchronise": [
                    "send1",
                    "send1",
                    null,
                    null
                ]
            },
            {
                "result": "send2",
                "synchronise": [
                    "send2",
                    null,
                    "send2",
                    null
                ]
            },
            {
                "result": "send3",
                "synchronise": [
                    "send3",
                    null,
                    null,
                    "send3"
                ]
            },
            {
                "result": "time",
                "synchronise": [
                    "time",
                    "time",
                    "time",
                    "time"
                ]
            }
        ]
    },
    "type": "mdp",
    "variables": [
        {
            "initial-value": false,
            "name": "all_delivered",
            "transient": true,
            "type": "bool"
        },
        {
            "initial-value": false,
            "name": "collision_max_backoff",
            "transient": true,
            "type": "bool"
        },
        {
            "initial-value": 0,
            "name": "b",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 2
            }
        },
        {
            "initial-value": 0,
            "name": "s1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 5
            }
        },
        {
            "initial-value": 0,
            "name": "cd1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 4
            }
        },
        {
            "initial-value": 0,
            "name": "s2",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 5
            }
        },
        {
            "initial-value": 0,
            "name": "cd2",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 4
            }
        },
        {
            "initial-value": 0,
            "name": "s3",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 5
            }
        },
        {
            "initial-value": 0,
            "name": "cd3",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 4
            }
        }
    ]
}