{
    "actions": [
        {
            "name": "finish1"
        },
        {
            "name": "finish2"
        },
        {
            "name": "send1"
        },
        {
            "name": "send2"
        },
        {
            "name": "time"
        }
    ],
    "automata": [
        {
            "edges": [
                {
                    "action": "finish1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "c1 <- 0",
                                    "ref": "c1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(c1 > 0)",
                        "exp": {
                            "left": "c1",
                            "op": ">",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "finish2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "c2 <- 0",
                                    "ref": "c2",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(c2 > 0)",
                        "exp": {
                            "left": "c2",
                            "op": ">",
                            "right": 0
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "c1 <- 1",
                                    "ref": "c1",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((c1 = 0) & (c2 = 0))",
                        "exp": {
                            "left": {
                                "left": "c1",
                                "op": "=",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "c2",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "col <- (min((col + 1), 0))",
                                    "ref": "col",
                                    "value": {
                                        "left": {
                                            "left": "col",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 0
                                    }
                                },
                                {
                                    "comment": "c1 <- 2",
                                    "ref": "c1",
                                    "value": 2
                                },
                                {
                                    "comment": "c2 <- 2",
                                    "ref": "c2",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((c1 = 0) & (c2 > 0))",
                        "exp": {
                            "left": {
                                "left": "c1",
                                "op": "=",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "c2",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "c2 <- 1",
                                    "ref": "c2",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((c2 = 0) & (c1 = 0))",
                        "exp": {
                            "left": {
                                "left": "c2",
                                "op": "=",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "c1",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "col <- (min((col + 1), 0))",
                                    "ref": "col",
                                    "value": {
                                        "left": {
                                            "left": "col",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 0
                                    }
                                },
                                {
                                    "comment": "c1 <- 2",
                                    "ref": "c1",
                                    "value": 2
                                },
                                {
                                    "comment": "c2 <- 2",
                                    "ref": "c2",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((c2 = 0) & (c1 > 0))",
                        "exp": {
                            "left": {
                                "left": "c2",
                                "op": "=",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "c1",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l",
                    "transient-values": [
                        {
                            "comment": "target <- ((s1 = 12) & (s2 = 12))",
                            "ref": "target",
                            "value": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 12
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 12
                                }
                            }
                        }
                    ]
                }
            ],
            "name": "medium",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "col",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 1
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 8",
                                    "ref": "s1",
                                    "value": 8
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 1) & ((x1 = 3) | (x1 = (3 - 1))))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 2
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 1) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 2) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 3) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 3
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 0",
                                    "ref": "slot1",
                                    "value": 0
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 0",
                                    "ref": "slot1",
                                    "value": 0
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 1",
                                    "ref": "slot1",
                                    "value": 1
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 0",
                                    "ref": "slot1",
                                    "value": 0
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 1",
                                    "ref": "slot1",
                                    "value": 1
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 2",
                                    "ref": "slot1",
                                    "value": 2
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 3",
                                    "ref": "slot1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 0",
                                    "ref": "slot1",
                                    "value": 0
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 1",
                                    "ref": "slot1",
                                    "value": 1
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 2",
                                    "ref": "slot1",
                                    "value": 2
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 3",
                                    "ref": "slot1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 4",
                                    "ref": "slot1",
                                    "value": 4
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 5",
                                    "ref": "slot1",
                                    "value": 5
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 6",
                                    "ref": "slot1",
                                    "value": 6
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 7",
                                    "ref": "slot1",
                                    "value": 7
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 3))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": "=",
                                "right": 3
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 0",
                                    "ref": "slot1",
                                    "value": 0
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 1",
                                    "ref": "slot1",
                                    "value": 1
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 2",
                                    "ref": "slot1",
                                    "value": 2
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 3",
                                    "ref": "slot1",
                                    "value": 3
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 4",
                                    "ref": "slot1",
                                    "value": 4
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 5",
                                    "ref": "slot1",
                                    "value": 5
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 6",
                                    "ref": "slot1",
                                    "value": 6
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 7",
                                    "ref": "slot1",
                                    "value": 7
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 8",
                                    "ref": "slot1",
                                    "value": 8
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 9",
                                    "ref": "slot1",
                                    "value": 9
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 10",
                                    "ref": "slot1",
                                    "value": 10
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 11",
                                    "ref": "slot1",
                                    "value": 11
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 12",
                                    "ref": "slot1",
                                    "value": 12
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 13",
                                    "ref": "slot1",
                                    "value": 13
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 14",
                                    "ref": "slot1",
                                    "value": 14
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 4",
                                    "ref": "s1",
                                    "value": 4
                                },
                                {
                                    "comment": "slot1 <- 15",
                                    "ref": "slot1",
                                    "value": 15
                                },
                                {
                                    "comment": "bc1 <- (min((bc1 + 1), 4))",
                                    "ref": "bc1",
                                    "value": {
                                        "left": {
                                            "left": "bc1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & ((x1 = 3) | (x1 = (3 - 1)))) & (bc1 = 4))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc1",
                                "op": "=",
                                "right": 4
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 0",
                                    "ref": "backoff1",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 1",
                                    "ref": "backoff1",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 2",
                                    "ref": "backoff1",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 3",
                                    "ref": "backoff1",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 4",
                                    "ref": "backoff1",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 5",
                                    "ref": "backoff1",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 6",
                                    "ref": "backoff1",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 7",
                                    "ref": "backoff1",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 8",
                                    "ref": "backoff1",
                                    "value": 8
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 9",
                                    "ref": "backoff1",
                                    "value": 9
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 10",
                                    "ref": "backoff1",
                                    "value": 10
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 11",
                                    "ref": "backoff1",
                                    "value": 11
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 12",
                                    "ref": "backoff1",
                                    "value": 12
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 13",
                                    "ref": "backoff1",
                                    "value": 13
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 14",
                                    "ref": "backoff1",
                                    "value": 14
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- 15",
                                    "ref": "backoff1",
                                    "value": 15
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(s1 = 4)",
                        "exp": {
                            "left": "s1",
                            "op": "=",
                            "right": 4
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff1 <- (backoff1 - 1)",
                                    "ref": "backoff1",
                                    "value": {
                                        "left": "backoff1",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 5) & (x1 = 1)) & (backoff1 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 5
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "backoff1",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                },
                                {
                                    "comment": "slot1 <- (slot1 - 1)",
                                    "ref": "slot1",
                                    "value": {
                                        "left": "slot1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "backoff1 <- 15",
                                    "ref": "backoff1",
                                    "value": 15
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s1 = 5) & (x1 = 1)) & (backoff1 = 0)) & (slot1 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "slot1",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "backoff1",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 5
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 8",
                                    "ref": "s1",
                                    "value": 8
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s1 = 5) & (x1 = 1)) & (backoff1 = 0)) & (slot1 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "slot1",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "backoff1",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 5
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 6",
                                    "ref": "s1",
                                    "value": 6
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 5) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 5
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 7",
                                    "ref": "s1",
                                    "value": 7
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 6) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 6
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 5",
                                    "ref": "s1",
                                    "value": 5
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 7) & ((x1 = 3) | (x1 = (3 - 1))))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 7
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 2
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 6",
                                    "ref": "s1",
                                    "value": 6
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 7) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 7
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s1 = 10) & (c1 = 0)) & (x1 = 0)) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "args": [
                                        "c1",
                                        "c2"
                                    ],
                                    "function": "busy",
                                    "op": "call"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 10
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 11) & (x1 = 0)) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 11
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 3",
                                    "ref": "s1",
                                    "value": 3
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 11) & (x1 = 6))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 11
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "=",
                                "right": 6
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "finish1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 10",
                                    "ref": "s1",
                                    "value": 10
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 9) & (x1 >= 4)) & (c1 = 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 9
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "≥",
                                    "right": 4
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "c1",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "finish1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 11",
                                    "ref": "s1",
                                    "value": 11
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 9) & (x1 >= 4)) & (c1 = 2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 9
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "≥",
                                    "right": 4
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "c1",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "finish1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 12",
                                    "ref": "s1",
                                    "value": 12
                                },
                                {
                                    "comment": "bc1 <- 0",
                                    "ref": "bc1",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 10) & (c1 = 1)) & ((x1 = 4) | (x1 = (4 - 1))))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 10
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c1",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 4
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 3
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 9",
                                    "ref": "s1",
                                    "value": 9
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 8) & ((x1 = 1) | (x1 = (1 - 1))))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 8
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- 0",
                                    "ref": "x1",
                                    "value": 0
                                },
                                {
                                    "comment": "s1 <- 10",
                                    "ref": "s1",
                                    "value": 10
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 10) & (c1 = 0)) & ((x1 = 1) | ((x1 = (1 - 1)) & free(c1, c2))))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 10
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": {
                                        "left": "x1",
                                        "op": "=",
                                        "right": 0
                                    },
                                    "op": "∧",
                                    "right": {
                                        "args": [
                                            "c1",
                                            "c2"
                                        ],
                                        "function": "free",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 1) & (x1 < 3)) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "<",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 2",
                                    "ref": "s1",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 2) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 3) & (x1 < 3)) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "<",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 5) & (x1 < 1)) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 5
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "<",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 6",
                                    "ref": "s1",
                                    "value": 6
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 6) & busy(c1, c2))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 6
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 7) & (x1 < 3)) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 7
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "<",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 8) & (x1 < 1))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 8
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "<",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s1 = 9) & (x1 < 10))",
                        "exp": {
                            "left": {
                                "left": "s1",
                                "op": "=",
                                "right": 9
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "<",
                                "right": 10
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s1 = 10) & (c1 = 0)) & (x1 = 0)) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "args": [
                                        "c1",
                                        "c2"
                                    ],
                                    "function": "free",
                                    "op": "call"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 10
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 10) & (c1 = 1)) & (x1 < 4))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 10
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c1",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "<",
                                "right": 4
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 11) & (x1 = 0)) & free(c1, c2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 11
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c1",
                                    "c2"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x1 <- (min((x1 + 1), 11))",
                                    "ref": "x1",
                                    "value": {
                                        "left": {
                                            "left": "x1",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s1 = 11) & (x1 > 0)) & (x1 < 6))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s1",
                                    "op": "=",
                                    "right": 11
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x1",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "x1",
                                "op": "<",
                                "right": 6
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s1 <- 12",
                                    "ref": "s1",
                                    "value": 12
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s1 = 12)",
                        "exp": {
                            "left": "s1",
                            "op": "=",
                            "right": 12
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "station1",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "x1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 11
                    }
                },
                {
                    "initial-value": 0,
                    "name": "slot1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 15
                    }
                },
                {
                    "initial-value": 0,
                    "name": "backoff1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 15
                    }
                },
                {
                    "initial-value": 0,
                    "name": "bc1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 4
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 8",
                                    "ref": "s2",
                                    "value": 8
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 1) & ((x2 = 3) | (x2 = (3 - 1))))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 2
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 1) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 2) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 3) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 3
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 0",
                                    "ref": "slot2",
                                    "value": 0
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 0",
                                    "ref": "slot2",
                                    "value": 0
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 1",
                                    "ref": "slot2",
                                    "value": 1
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 2)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 2
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 0",
                                    "ref": "slot2",
                                    "value": 0
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 1",
                                    "ref": "slot2",
                                    "value": 1
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 2",
                                    "ref": "slot2",
                                    "value": 2
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 3",
                                    "ref": "slot2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 4)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 4
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 0",
                                    "ref": "slot2",
                                    "value": 0
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 1",
                                    "ref": "slot2",
                                    "value": 1
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 2",
                                    "ref": "slot2",
                                    "value": 2
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 3",
                                    "ref": "slot2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 4",
                                    "ref": "slot2",
                                    "value": 4
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 5",
                                    "ref": "slot2",
                                    "value": 5
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 6",
                                    "ref": "slot2",
                                    "value": 6
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 7",
                                    "ref": "slot2",
                                    "value": 7
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 8)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 8
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 3))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": "=",
                                "right": 3
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 0",
                                    "ref": "slot2",
                                    "value": 0
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 1",
                                    "ref": "slot2",
                                    "value": 1
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 2",
                                    "ref": "slot2",
                                    "value": 2
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 3",
                                    "ref": "slot2",
                                    "value": 3
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 4",
                                    "ref": "slot2",
                                    "value": 4
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 5",
                                    "ref": "slot2",
                                    "value": 5
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 6",
                                    "ref": "slot2",
                                    "value": 6
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 7",
                                    "ref": "slot2",
                                    "value": 7
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 8",
                                    "ref": "slot2",
                                    "value": 8
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 9",
                                    "ref": "slot2",
                                    "value": 9
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 10",
                                    "ref": "slot2",
                                    "value": 10
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 11",
                                    "ref": "slot2",
                                    "value": 11
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 12",
                                    "ref": "slot2",
                                    "value": 12
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 13",
                                    "ref": "slot2",
                                    "value": 13
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 14",
                                    "ref": "slot2",
                                    "value": 14
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 4",
                                    "ref": "s2",
                                    "value": 4
                                },
                                {
                                    "comment": "slot2 <- 15",
                                    "ref": "slot2",
                                    "value": 15
                                },
                                {
                                    "comment": "bc2 <- (min((bc2 + 1), 4))",
                                    "ref": "bc2",
                                    "value": {
                                        "left": {
                                            "left": "bc2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 4
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & ((x2 = 3) | (x2 = (3 - 1)))) & (bc2 = 4))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 3
                                    },
                                    "op": "∨",
                                    "right": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 2
                                    }
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "bc2",
                                "op": "=",
                                "right": 4
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 0",
                                    "ref": "backoff2",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 1",
                                    "ref": "backoff2",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 2",
                                    "ref": "backoff2",
                                    "value": 2
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 3",
                                    "ref": "backoff2",
                                    "value": 3
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 4",
                                    "ref": "backoff2",
                                    "value": 4
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 5",
                                    "ref": "backoff2",
                                    "value": 5
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 6",
                                    "ref": "backoff2",
                                    "value": 6
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 7",
                                    "ref": "backoff2",
                                    "value": 7
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 8",
                                    "ref": "backoff2",
                                    "value": 8
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 9",
                                    "ref": "backoff2",
                                    "value": 9
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 10",
                                    "ref": "backoff2",
                                    "value": 10
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 11",
                                    "ref": "backoff2",
                                    "value": 11
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 12",
                                    "ref": "backoff2",
                                    "value": 12
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 13",
                                    "ref": "backoff2",
                                    "value": 13
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 14",
                                    "ref": "backoff2",
                                    "value": 14
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- 15",
                                    "ref": "backoff2",
                                    "value": 15
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 16)",
                                "exp": {
                                    "left": 1,
                                    "op": "/",
                                    "right": 16
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(s2 = 4)",
                        "exp": {
                            "left": "s2",
                            "op": "=",
                            "right": 4
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "backoff2 <- (backoff2 - 1)",
                                    "ref": "backoff2",
                                    "value": {
                                        "left": "backoff2",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 5) & (x2 = 1)) & (backoff2 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 5
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "backoff2",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                },
                                {
                                    "comment": "slot2 <- (slot2 - 1)",
                                    "ref": "slot2",
                                    "value": {
                                        "left": "slot2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "backoff2 <- 15",
                                    "ref": "backoff2",
                                    "value": 15
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s2 = 5) & (x2 = 1)) & (backoff2 = 0)) & (slot2 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "slot2",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "backoff2",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 5
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 8",
                                    "ref": "s2",
                                    "value": 8
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s2 = 5) & (x2 = 1)) & (backoff2 = 0)) & (slot2 = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "slot2",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "backoff2",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 5
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 6",
                                    "ref": "s2",
                                    "value": 6
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 5) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 5
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 7",
                                    "ref": "s2",
                                    "value": 7
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 6) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 6
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 5",
                                    "ref": "s2",
                                    "value": 5
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 7) & ((x2 = 3) | (x2 = (3 - 1))))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 7
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 2
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 6",
                                    "ref": "s2",
                                    "value": 6
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 7) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 7
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s2 = 10) & (c2 = 0)) & (x2 = 0)) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "args": [
                                        "c2",
                                        "c1"
                                    ],
                                    "function": "busy",
                                    "op": "call"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 10
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 11) & (x2 = 0)) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 11
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 3",
                                    "ref": "s2",
                                    "value": 3
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 11) & (x2 = 6))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 11
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "=",
                                "right": 6
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "finish2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 10",
                                    "ref": "s2",
                                    "value": 10
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 9) & (x2 >= 4)) & (c2 = 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 9
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "≥",
                                    "right": 4
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "c2",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "finish2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 11",
                                    "ref": "s2",
                                    "value": 11
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 9) & (x2 >= 4)) & (c2 = 2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 9
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "≥",
                                    "right": 4
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "c2",
                                "op": "=",
                                "right": 2
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "finish2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 12",
                                    "ref": "s2",
                                    "value": 12
                                },
                                {
                                    "comment": "bc2 <- 0",
                                    "ref": "bc2",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 10) & (c2 = 1)) & ((x2 = 4) | (x2 = (4 - 1))))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 10
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c2",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 4
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 3
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 9",
                                    "ref": "s2",
                                    "value": 9
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 8) & ((x2 = 1) | (x2 = (1 - 1))))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 8
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "send2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- 0",
                                    "ref": "x2",
                                    "value": 0
                                },
                                {
                                    "comment": "s2 <- 10",
                                    "ref": "s2",
                                    "value": 10
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 10) & (c2 = 0)) & ((x2 = 1) | ((x2 = (1 - 1)) & free(c2, c1))))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 10
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∨",
                                "right": {
                                    "left": {
                                        "left": "x2",
                                        "op": "=",
                                        "right": 0
                                    },
                                    "op": "∧",
                                    "right": {
                                        "args": [
                                            "c2",
                                            "c1"
                                        ],
                                        "function": "free",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 1) & (x2 < 3)) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "<",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 2",
                                    "ref": "s2",
                                    "value": 2
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 2) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 3) & (x2 < 3)) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "<",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 5) & (x2 < 1)) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 5
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "<",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 6",
                                    "ref": "s2",
                                    "value": 6
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 6) & busy(c2, c1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 6
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "busy",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 7) & (x2 < 3)) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 7
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "<",
                                    "right": 3
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 8) & (x2 < 1))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 8
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "<",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s2 = 9) & (x2 < 10))",
                        "exp": {
                            "left": {
                                "left": "s2",
                                "op": "=",
                                "right": 9
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "<",
                                "right": 10
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s2 = 10) & (c2 = 0)) & (x2 = 0)) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "args": [
                                        "c2",
                                        "c1"
                                    ],
                                    "function": "free",
                                    "op": "call"
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 10
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 10) & (c2 = 1)) & (x2 < 4))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 10
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c2",
                                    "op": "=",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "<",
                                "right": 4
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 11) & (x2 = 0)) & free(c2, c1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 11
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "args": [
                                    "c2",
                                    "c1"
                                ],
                                "function": "free",
                                "op": "call"
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x2 <- (min((x2 + 1), 11))",
                                    "ref": "x2",
                                    "value": {
                                        "left": {
                                            "left": "x2",
                                            "op": "+",
                                            "right": 1
                                        },
                                        "op": "min",
                                        "right": 11
                                    }
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s2 = 11) & (x2 > 0)) & (x2 < 6))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s2",
                                    "op": "=",
                                    "right": 11
                                },
                                "op": "∧",
                                "right": {
                                    "left": "x2",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "x2",
                                "op": "<",
                                "right": 6
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "action": "time",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s2 <- 12",
                                    "ref": "s2",
                                    "value": 12
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s2 = 12)",
                        "exp": {
                            "left": "s2",
                            "op": "=",
                            "right": 12
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "station2",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "x2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 11
                    }
                },
                {
                    "initial-value": 0,
                    "name": "slot2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 15
                    }
                },
                {
                    "initial-value": 0,
                    "name": "backoff2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 15
                    }
                },
                {
                    "initial-value": 0,
                    "name": "bc2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 4
                    }
                }
            ]
        }
    ],
    "constants": [
        {
            "name": "COL",
            "type": "int",
            "value": 0
        },
        {
            "name": "ASLOTTIME",
            "type": "int",
            "value": 1
        },
        {
            "name": "DIFS",
            "type": "int",
            "value": 3
        },
        {
            "name": "VULN",
            "type": "int",
            "value": 1
        },
        {
            "name": "TRANS_TIME_MAX",
            "type": "int",
            "value": 10
        },
        {
            "name": "TRANS_TIME_MIN",
            "type": "int",
            "value": 4
        },
        {
            "name": "ACK_TO",
            "type": "int",
            "value": 6
        },
        {
            "name": "ACK",
            "type": "int",
            "value": 4
        },
        {
            "name": "SIFS",
            "type": "int",
            "value": 1
        },
        {
            "name": "TIME_MAX",
            "type": "int",
            "value": 11
        },
        {
            "name": "MAX_BACKOFF",
            "type": "int",
            "value": 4
        }
    ],
    "features": [
        "derived-operators",
        "functions"
    ],
    "functions": [
        {
            "body": {
                "left": {
                    "left": "free__param__c1",
                    "op": "=",
                    "right": 0
                },
                "op": "∧",
                "right": {
                    "left": "free__param__c2",
                    "op": "=",
                    "right": 0
                }
            },
            "name": "free",
            "parameters": [
                {
                    "name": "free__param__c1",
                    "type": "int"
                },
                {
                    "name": "free__param__c2",
                    "type": "int"
                }
            ],
            "type": "bool"
        },
        {
            "body": {
                "left": {
                    "left": "busy__param__c1",
                    "op": ">",
                    "right": 0
                },
                "op": "∨",
                "right": {
                    "left": "busy__param__c2",
                    "op": ">",
                    "right": 0
                }
            },
            "name": "busy",
            "parameters": [
                {
                    "name": "busy__param__c1",
                    "type": "int"
                },
                {
                    "name": "busy__param__c2",
                    "type": "int"
                }
            ],
            "type": "bool"
        }
    ],
    "jani-version": 1,
    "name": "model",
    "properties": [
        {
            "expression": {
                "fun": "values",
                "op": "filter",
                "states": {
                    "op": "initial"
                },
                "values": {
                    "left": {
                        "exp": {
                            "left": true,
                            "op": "U",
                            "right": "target"
                        },
                        "op": "Pmin"
                    },
                    "op": "≥",
                    "right": 1
                }
            },
            "name": "sent"
        }
    ],
    "restrict-initial": {
        "exp": true
    },
    "system": {
        "elements": [
            {
                "automaton": "medium"
            },
            {
                "automaton": "station1"
            },
            {
                "automaton": "station2"
            }
        ],
        "syncs": [
            {
                "result": "finish1",
                "synchronise": [
                    "finish1",
                    "finish1",
                    null
                ]
            },
            {
                "result": "finish2",
                "synchronise": [
                    "finish2",
                    null,
                    "finish2"
                ]
            },
            {
                "result": "send1",
                "synchronise": [
                    "send1",
                    "send1",
                    null
                ]
            },
            {
                "result": "send2",
                "synchronise": [
                    "send2",
                    null,
                    "send2"
                ]
            },
            {
                "result": "time",
                "synchronise": [
                    null,
                    "time",
                    "time"
                ]
            }
        ]
    },
    "type": "mdp",
    "variables": [
        {
            "initial-value": false,
            "name": "target",
            "transient": true,
            "type": "bool"
        },
        {
            "initial-value": 0,
            "name": "c1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 2
            }
        },
        {
            "initial-value": 0,
            "name": "c2",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 2
            }
        },
        {
            "initial-value": 1,
            "name": "s1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 1,
                "upper-bound": 12
            }
        },
        {
            "initial-value": 1,
            "name": "s2",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 1,
                "upper-bound": 12
            }
        }
    ]
}