{
    "actions": [],
    "automata": [
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 1",
                                    "ref": "s",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((s = 0) & (c < 40))",
                        "exp": {
                            "left": {
                                "left": "s",
                                "op": "=",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "c",
                                "op": "<",
                                "right": 40
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "u <- (u + 1)",
                                    "ref": "u",
                                    "value": {
                                        "left": "u",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "c <- 0",
                                    "ref": "c",
                                    "value": 0
                                },
                                {
                                    "comment": "s <- 1",
                                    "ref": "s",
                                    "value": 1
                                },
                                {
                                    "comment": "z <- 0",
                                    "ref": "z",
                                    "value": 0
                                },
                                {
                                    "comment": "zx <- z",
                                    "ref": "zx",
                                    "value": "z"
                                },
                                {
                                    "comment": "zy <- z",
                                    "ref": "zy",
                                    "value": "z"
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s = 0) & (c = 40)) & (u < ((2 * 4) + 1)))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 40
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "u",
                                "op": "<",
                                "right": 9
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 4",
                                    "ref": "s",
                                    "value": 4
                                },
                                {
                                    "comment": "zx <- 0",
                                    "ref": "zx",
                                    "value": 0
                                },
                                {
                                    "comment": "zy <- 0",
                                    "ref": "zy",
                                    "value": 0
                                },
                                {
                                    "comment": "x <- 0",
                                    "ref": "x",
                                    "value": 0
                                },
                                {
                                    "comment": "y <- 0",
                                    "ref": "y",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s = 0) & (c = 40)) & (u = ((2 * 4) + 1)))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "c",
                                    "op": "=",
                                    "right": 40
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "u",
                                "op": "=",
                                "right": 9
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 2",
                                    "ref": "s",
                                    "value": 2
                                },
                                {
                                    "comment": "x <- 1",
                                    "ref": "x",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "9/10",
                                "exp": {
                                    "left": 9.0,
                                    "op": "/",
                                    "right": 10.0
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 2",
                                    "ref": "s",
                                    "value": 2
                                },
                                {
                                    "comment": "x <- 0",
                                    "ref": "x",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 - 9/10)",
                                "exp": {
                                    "left": 1.0,
                                    "op": "/",
                                    "right": 10.0
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s = 1) & (u = 1))",
                        "exp": {
                            "left": {
                                "left": "s",
                                "op": "=",
                                "right": 1
                            },
                            "op": "∧",
                            "right": {
                                "left": "u",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 2",
                                    "ref": "s",
                                    "value": 2
                                },
                                {
                                    "comment": "zx <- (zx - 1)",
                                    "ref": "zx",
                                    "value": {
                                        "left": "zx",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "x <- 1",
                                    "ref": "x",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s = 1) & (u > 1)) & (zx > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∧",
                                "right": {
                                    "left": "u",
                                    "op": ">",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "zx",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 2",
                                    "ref": "s",
                                    "value": 2
                                },
                                {
                                    "comment": "x <- 0",
                                    "ref": "x",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s = 1) & (u > 1)) & (zx = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 1
                                },
                                "op": "∧",
                                "right": {
                                    "left": "u",
                                    "op": ">",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "zx",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 3",
                                    "ref": "s",
                                    "value": 3
                                },
                                {
                                    "comment": "y <- 1",
                                    "ref": "y",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "9/10",
                                "exp": {
                                    "left": 9.0,
                                    "op": "/",
                                    "right": 10.0
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 3",
                                    "ref": "s",
                                    "value": 3
                                },
                                {
                                    "comment": "y <- 0",
                                    "ref": "y",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 - 9/10)",
                                "exp": {
                                    "left": 1.0,
                                    "op": "/",
                                    "right": 10.0
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((s = 2) & (u = 1))",
                        "exp": {
                            "left": {
                                "left": "s",
                                "op": "=",
                                "right": 2
                            },
                            "op": "∧",
                            "right": {
                                "left": "u",
                                "op": "=",
                                "right": 1
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 3",
                                    "ref": "s",
                                    "value": 3
                                },
                                {
                                    "comment": "zy <- (zy - 1)",
                                    "ref": "zy",
                                    "value": {
                                        "left": "zy",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "y <- 1",
                                    "ref": "y",
                                    "value": 1
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(zy / (40 - c))",
                                "exp": {
                                    "left": "zy",
                                    "op": "/",
                                    "right": {
                                        "left": 40,
                                        "op": "-",
                                        "right": "c"
                                    }
                                }
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 3",
                                    "ref": "s",
                                    "value": 3
                                },
                                {
                                    "comment": "y <- 0",
                                    "ref": "y",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 - (zy / (40 - c)))",
                                "exp": {
                                    "left": 1,
                                    "op": "-",
                                    "right": {
                                        "left": "zy",
                                        "op": "/",
                                        "right": {
                                            "left": 40,
                                            "op": "-",
                                            "right": "c"
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((s = 2) & (u > 1)) & (zy < (40 - c))) & (zy > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "zy",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "u",
                                    "op": ">",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "zy",
                                    "op": "<",
                                    "right": {
                                        "left": 40,
                                        "op": "-",
                                        "right": "c"
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 2
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 3",
                                    "ref": "s",
                                    "value": 3
                                },
                                {
                                    "comment": "zy <- (zy - 1)",
                                    "ref": "zy",
                                    "value": {
                                        "left": "zy",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "y <- 1",
                                    "ref": "y",
                                    "value": 1
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((((s = 2) & (u > 1)) & (zy = (40 - c))) & (c < 40))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "c",
                                    "op": "<",
                                    "right": 40
                                },
                                "op": "∧",
                                "right": {
                                    "left": "u",
                                    "op": ">",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "zy",
                                    "op": "=",
                                    "right": {
                                        "left": 40,
                                        "op": "-",
                                        "right": "c"
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 2
                                }
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "s <- 3",
                                    "ref": "s",
                                    "value": 3
                                },
                                {
                                    "comment": "y <- 0",
                                    "ref": "y",
                                    "value": 0
                                }
                            ],
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(((s = 2) & (u > 1)) & (zy = 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 2
                                },
                                "op": "∧",
                                "right": {
                                    "left": "u",
                                    "op": ">",
                                    "right": 1
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "zy",
                                "op": "=",
                                "right": 0
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "c <- (c + 1)",
                                    "ref": "c",
                                    "value": {
                                        "left": "c",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "s <- 0",
                                    "ref": "s",
                                    "value": 0
                                },
                                {
                                    "comment": "z <- (z + (1 - (x * y)))",
                                    "ref": "z",
                                    "value": {
                                        "left": "z",
                                        "op": "+",
                                        "right": {
                                            "left": 1,
                                            "op": "-",
                                            "right": {
                                                "left": "x",
                                                "op": "*",
                                                "right": "y"
                                            }
                                        }
                                    }
                                },
                                {
                                    "comment": "x <- 0",
                                    "ref": "x",
                                    "value": 0
                                },
                                {
                                    "comment": "y <- 0",
                                    "ref": "y",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 - 1/50)",
                                "exp": 0.98
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "c <- (c + 1)",
                                    "ref": "c",
                                    "value": {
                                        "left": "c",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "s <- 0",
                                    "ref": "s",
                                    "value": 0
                                },
                                {
                                    "comment": "z <- (z + (x * y))",
                                    "ref": "z",
                                    "value": {
                                        "left": "z",
                                        "op": "+",
                                        "right": {
                                            "left": "x",
                                            "op": "*",
                                            "right": "y"
                                        }
                                    }
                                },
                                {
                                    "comment": "x <- 0",
                                    "ref": "x",
                                    "value": 0
                                },
                                {
                                    "comment": "y <- 0",
                                    "ref": "y",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "1/50",
                                "exp": {
                                    "left": 1.0,
                                    "op": "/",
                                    "right": 50.0
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((s = 3) & (z < 40)) & (c < 40))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "z",
                                    "op": "<",
                                    "right": 40
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "c",
                                "op": "<",
                                "right": 40
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "(s = 4)",
                        "exp": {
                            "left": "s",
                            "op": "=",
                            "right": 4
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l",
                    "transient-values": [
                        {
                            "comment": "target <- ((s = 4) & ((z / 40) < 1/10))",
                            "ref": "target",
                            "value": {
                                "left": {
                                    "left": "s",
                                    "op": "=",
                                    "right": 4
                                },
                                "op": "∧",
                                "right": {
                                    "left": {
                                        "left": "z",
                                        "op": "/",
                                        "right": 40
                                    },
                                    "op": "<",
                                    "right": {
                                        "left": 1.0,
                                        "op": "/",
                                        "right": 10.0
                                    }
                                }
                            }
                        }
                    ]
                }
            ],
            "name": "multiplex",
            "variables": [
                {
                    "initial-value": 1,
                    "name": "u",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 1,
                        "upper-bound": 9
                    }
                },
                {
                    "initial-value": 0,
                    "name": "c",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 40
                    }
                },
                {
                    "initial-value": 0,
                    "name": "zx",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 40
                    }
                },
                {
                    "initial-value": 0,
                    "name": "zy",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 40
                    }
                },
                {
                    "initial-value": 0,
                    "name": "x",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 1
                    }
                },
                {
                    "initial-value": 0,
                    "name": "y",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 1
                    }
                }
            ]
        }
    ],
    "constants": [
        {
            "name": "N",
            "type": "int",
            "value": 40
        },
        {
            "name": "K",
            "type": "int",
            "value": 4
        },
        {
            "name": "M",
            "type": "int",
            "value": 9
        },
        {
            "name": "perr",
            "type": "real",
            "value": {
                "left": 1.0,
                "op": "/",
                "right": 50.0
            }
        },
        {
            "name": "prob1",
            "type": "real",
            "value": {
                "left": 9.0,
                "op": "/",
                "right": 10.0
            }
        }
    ],
    "features": [
        "derived-operators"
    ],
    "jani-version": 1,
    "name": "model",
    "properties": [
        {
            "expression": {
                "fun": "values",
                "op": "filter",
                "states": {
                    "op": "initial"
                },
                "values": {
                    "exp": {
                        "left": true,
                        "op": "U",
                        "right": "target"
                    },
                    "op": "Pmin"
                }
            },
            "name": "reliable"
        }
    ],
    "restrict-initial": {
        "exp": true
    },
    "system": {
        "elements": [
            {
                "automaton": "multiplex"
            }
        ]
    },
    "type": "dtmc",
    "variables": [
        {
            "initial-value": false,
            "name": "target",
            "transient": true,
            "type": "bool"
        },
        {
            "initial-value": 0,
            "name": "s",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 4
            }
        },
        {
            "initial-value": 0,
            "name": "z",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 40
            }
        }
    ]
}