{
    "actions": [],
    "automata": [
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x <- 99",
                                    "ref": "x",
                                    "value": 99
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "7/10",
                                "exp": 0.7
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x <- 101",
                                    "ref": "x",
                                    "value": 101
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 - 7/10)",
                                "exp": 0.3
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(x = 100)",
                        "exp": {
                            "left": "x",
                            "op": "=",
                            "right": 100
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x <- (x - 1)",
                                    "ref": "x",
                                    "value": {
                                        "left": "x",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "1/2",
                                "exp": 0.5
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x <- 100",
                                    "ref": "x",
                                    "value": 100
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 - 1/2)",
                                "exp": 0.5
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((x > 0) & (x < 100))",
                        "exp": {
                            "left": {
                                "left": "x",
                                "op": ">",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "x",
                                "op": "<",
                                "right": 100
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "x <- (x + 1)",
                                    "ref": "x",
                                    "value": {
                                        "left": "x",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "1/2",
                                "exp": 0.5
                            }
                        },
                        {
                            "assignments": [
                                {
                                    "comment": "x <- 100",
                                    "ref": "x",
                                    "value": 100
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 - 1/2)",
                                "exp": 0.5
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((x > 100) & (x < (2 * 100)))",
                        "exp": {
                            "left": {
                                "left": "x",
                                "op": ">",
                                "right": 100
                            },
                            "op": "∧",
                            "right": {
                                "left": "x",
                                "op": "<",
                                "right": 200
                            }
                        }
                    },
                    "location": "l"
                },
                {
                    "destinations": [
                        {
                            "location": "l"
                        }
                    ],
                    "guard": {
                        "comment": "((x = 0) | (x = (2 * 100)))",
                        "exp": {
                            "left": {
                                "left": "x",
                                "op": "=",
                                "right": 0
                            },
                            "op": "∨",
                            "right": {
                                "left": "x",
                                "op": "=",
                                "right": 200
                            }
                        }
                    },
                    "location": "l"
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l",
                    "transient-values": [
                        {
                            "comment": "Target <- (x = 0)",
                            "ref": "Target",
                            "value": {
                                "left": "x",
                                "op": "=",
                                "right": 0
                            }
                        }
                    ]
                }
            ],
            "name": "main",
            "variables": []
        }
    ],
    "constants": [
        {
            "name": "N",
            "type": "int",
            "value": 100
        },
        {
            "name": "p",
            "type": "real",
            "value": 0.7
        },
        {
            "name": "q",
            "type": "real",
            "value": 0.5
        }
    ],
    "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": "target"
        }
    ],
    "restrict-initial": {
        "exp": true
    },
    "system": {
        "elements": [
            {
                "automaton": "main"
            }
        ]
    },
    "type": "dtmc",
    "variables": [
        {
            "initial-value": false,
            "name": "Target",
            "transient": true,
            "type": "bool"
        },
        {
            "initial-value": 100,
            "name": "x",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 200
            }
        }
    ]
}