{ "actions": [], "automata": [ { "edges": [ { "destinations": [ { "assignments": [ { "comment": "S1 <- 50", "ref": "S1", "value": 50 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50) / ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } ], "guard": { "comment": "(S1 = 0)", "exp": { "left": "S1", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)", "exp": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } }, { "destinations": [ { "assignments": [ { "comment": "S1 <- 0", "ref": "S1", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * S1) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } }, { "assignments": [ { "comment": "S1 <- 100", "ref": "S1", "value": 100 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } } ], "guard": { "comment": "(S1 = 50)", "exp": { "left": "S1", "op": "=", "right": 50 } }, "location": "l", "rate": { "comment": "(((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } }, { "destinations": [ { "assignments": [ { "comment": "S1 <- 50", "ref": "S1", "value": 50 } ], "location": "l", "probability": { "comment": "(((3/400 * S1) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } }, { "assignments": [ { "comment": "S1 <- 150", "ref": "S1", "value": 150 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } } ], "guard": { "comment": "(S1 = 100)", "exp": { "left": "S1", "op": "=", "right": 100 } }, "location": "l", "rate": { "comment": "(((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } }, { "destinations": [ { "assignments": [ { "comment": "S1 <- 100", "ref": "S1", "value": 100 } ], "location": "l", "probability": { "comment": "(((3/400 * S1) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } }, { "assignments": [ { "comment": "S1 <- 200", "ref": "S1", "value": 200 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } } ], "guard": { "comment": "(S1 = 150)", "exp": { "left": "S1", "op": "=", "right": 150 } }, "location": "l", "rate": { "comment": "(((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } }, { "destinations": [ { "assignments": [ { "comment": "S1 <- 150", "ref": "S1", "value": 150 } ], "location": "l", "probability": { "comment": "(((3/400 * S1) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } }, { "assignments": [ { "comment": "S1 <- 250", "ref": "S1", "value": 250 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50) / (((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } } } ], "guard": { "comment": "(S1 = 200)", "exp": { "left": "S1", "op": "=", "right": 200 } }, "location": "l", "rate": { "comment": "(((3/400 * S1) / 50) + ((10 * (((99/1000 / (199/100 + ((1/2 * XX) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * Y) ^ 2))) * 10))) / 50))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "XX" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Y" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 50 } } } }, { "destinations": [ { "assignments": [ { "comment": "S1 <- 200", "ref": "S1", "value": 200 } ], "location": "l", "probability": { "comment": "(((3/400 * S1) / 50) / ((3/400 * S1) / 50))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 } } } } ], "guard": { "comment": "(S1 = 250)", "exp": { "left": "S1", "op": "=", "right": 250 } }, "location": "l", "rate": { "comment": "((3/400 * S1) / 50)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "S1" }, "op": "/", "right": 50 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l", "transient-values": [ { "comment": "target <- ((S2 > 80) & (S3 < 20))", "ref": "target", "value": { "left": { "left": "S2", "op": ">", "right": 80 }, "op": "∧", "right": { "left": "S3", "op": "<", "right": 20 } } } ] } ], "name": "S1_def", "variables": [] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "S2 <- 10", "ref": "S2", "value": 10 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } ], "guard": { "comment": "(S2 = 0)", "exp": { "left": "S2", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)", "exp": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 0", "ref": "S2", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 20", "ref": "S2", "value": 20 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 10)", "exp": { "left": "S2", "op": "=", "right": 10 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 10", "ref": "S2", "value": 10 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 30", "ref": "S2", "value": 30 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 20)", "exp": { "left": "S2", "op": "=", "right": 20 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 20", "ref": "S2", "value": 20 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 40", "ref": "S2", "value": 40 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 30)", "exp": { "left": "S2", "op": "=", "right": 30 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 30", "ref": "S2", "value": 30 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 50", "ref": "S2", "value": 50 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 40)", "exp": { "left": "S2", "op": "=", "right": 40 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 40", "ref": "S2", "value": 40 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 60", "ref": "S2", "value": 60 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 50)", "exp": { "left": "S2", "op": "=", "right": 50 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 50", "ref": "S2", "value": 50 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 70", "ref": "S2", "value": 70 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 60)", "exp": { "left": "S2", "op": "=", "right": 60 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 60", "ref": "S2", "value": 60 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 80", "ref": "S2", "value": 80 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 70)", "exp": { "left": "S2", "op": "=", "right": 70 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 70", "ref": "S2", "value": 70 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 90", "ref": "S2", "value": 90 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 80)", "exp": { "left": "S2", "op": "=", "right": 80 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 80", "ref": "S2", "value": 80 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } }, { "assignments": [ { "comment": "S2 <- 100", "ref": "S2", "value": 100 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10) / (((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } } } ], "guard": { "comment": "(S2 = 90)", "exp": { "left": "S2", "op": "=", "right": 90 } }, "location": "l", "rate": { "comment": "(((3/400 * S2) / 10) + ((10 * (((99/1000 / (199/100 + ((1/2 * S1) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S1" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 10 } } } }, { "destinations": [ { "assignments": [ { "comment": "S2 <- 90", "ref": "S2", "value": 90 } ], "location": "l", "probability": { "comment": "(((3/400 * S2) / 10) / ((3/400 * S2) / 10))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 } } } } ], "guard": { "comment": "(S2 = 100)", "exp": { "left": "S2", "op": "=", "right": 100 } }, "location": "l", "rate": { "comment": "((3/400 * S2) / 10)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "S2" }, "op": "/", "right": 10 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "S2_def", "variables": [] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "S3 <- 15", "ref": "S3", "value": 15 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } ], "guard": { "comment": "(S3 = 0)", "exp": { "left": "S3", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)", "exp": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 0", "ref": "S3", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 30", "ref": "S3", "value": 30 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 15)", "exp": { "left": "S3", "op": "=", "right": 15 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 15", "ref": "S3", "value": 15 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 45", "ref": "S3", "value": 45 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 30)", "exp": { "left": "S3", "op": "=", "right": 30 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 30", "ref": "S3", "value": 30 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 60", "ref": "S3", "value": 60 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 45)", "exp": { "left": "S3", "op": "=", "right": 45 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 45", "ref": "S3", "value": 45 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 75", "ref": "S3", "value": 75 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 60)", "exp": { "left": "S3", "op": "=", "right": 60 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 60", "ref": "S3", "value": 60 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 90", "ref": "S3", "value": 90 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 75)", "exp": { "left": "S3", "op": "=", "right": 75 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 75", "ref": "S3", "value": 75 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 105", "ref": "S3", "value": 105 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 90)", "exp": { "left": "S3", "op": "=", "right": 90 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 90", "ref": "S3", "value": 90 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 120", "ref": "S3", "value": 120 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 105)", "exp": { "left": "S3", "op": "=", "right": 105 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 105", "ref": "S3", "value": 105 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 135", "ref": "S3", "value": 135 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 120)", "exp": { "left": "S3", "op": "=", "right": 120 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 120", "ref": "S3", "value": 120 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } }, { "assignments": [ { "comment": "S3 <- 150", "ref": "S3", "value": 150 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15) / (((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } } } ], "guard": { "comment": "(S3 = 135)", "exp": { "left": "S3", "op": "=", "right": 135 } }, "location": "l", "rate": { "comment": "(((3/400 * S3) / 15) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 15 } } } }, { "destinations": [ { "assignments": [ { "comment": "S3 <- 135", "ref": "S3", "value": 135 } ], "location": "l", "probability": { "comment": "(((3/400 * S3) / 15) / ((3/400 * S3) / 15))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 } } } } ], "guard": { "comment": "(S3 = 150)", "exp": { "left": "S3", "op": "=", "right": 150 } }, "location": "l", "rate": { "comment": "((3/400 * S3) / 15)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "S3" }, "op": "/", "right": 15 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "S3_def", "variables": [] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "S4 <- 40", "ref": "S4", "value": 40 } ], "location": "l", "probability": { "comment": "(((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40) / ((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } } } ], "guard": { "comment": "(S4 = 0)", "exp": { "left": "S4", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40)", "exp": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } }, { "destinations": [ { "assignments": [ { "comment": "S4 <- 0", "ref": "S4", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * S4) / 40) / (((3/400 * S4) / 40) + ((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } } } }, { "assignments": [ { "comment": "S4 <- 80", "ref": "S4", "value": 80 } ], "location": "l", "probability": { "comment": "(((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40) / (((3/400 * S4) / 40) + ((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } } } } ], "guard": { "comment": "(S4 = 40)", "exp": { "left": "S4", "op": "=", "right": 40 } }, "location": "l", "rate": { "comment": "(((3/400 * S4) / 40) + ((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } } }, { "destinations": [ { "assignments": [ { "comment": "S4 <- 40", "ref": "S4", "value": 40 } ], "location": "l", "probability": { "comment": "(((3/400 * S4) / 40) / (((3/400 * S4) / 40) + ((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } } } }, { "assignments": [ { "comment": "S4 <- 120", "ref": "S4", "value": 120 } ], "location": "l", "probability": { "comment": "(((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40) / (((3/400 * S4) / 40) + ((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } } } } ], "guard": { "comment": "(S4 = 80)", "exp": { "left": "S4", "op": "=", "right": 80 } }, "location": "l", "rate": { "comment": "(((3/400 * S4) / 40) + ((10 * ((((99/1000 / (199/100 + ((1/2 * 0) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * 120) ^ 2))) * 10)) + ((99/1000 / (199/100 + ((1/2 * S2) ^ 2))) * 10))) / 40))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": 35679402.0, "op": "/", "right": 71679601.0 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S2" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 40 } } } }, { "destinations": [ { "assignments": [ { "comment": "S4 <- 80", "ref": "S4", "value": 80 } ], "location": "l", "probability": { "comment": "(((3/400 * S4) / 40) / ((3/400 * S4) / 40))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 } } } } ], "guard": { "comment": "(S4 = 120)", "exp": { "left": "S4", "op": "=", "right": 120 } }, "location": "l", "rate": { "comment": "((3/400 * S4) / 40)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "S4" }, "op": "/", "right": 40 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "S4_def", "variables": [] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "Y <- 30", "ref": "Y", "value": 30 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30) / ((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30))", "exp": 1.0 } } ], "guard": { "comment": "(Y = 0)", "exp": { "left": "Y", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30)", "exp": { "left": 33.0, "op": "/", "right": 360199.0 } } }, { "destinations": [ { "assignments": [ { "comment": "Y <- 0", "ref": "Y", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * Y) / 30) / (((3/400 * Y) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 360199.0 } } } } }, { "assignments": [ { "comment": "Y <- 60", "ref": "Y", "value": 60 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30) / (((3/400 * Y) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": 33.0, "op": "/", "right": 360199.0 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 360199.0 } } } } } ], "guard": { "comment": "(Y = 30)", "exp": { "left": "Y", "op": "=", "right": 30 } }, "location": "l", "rate": { "comment": "(((3/400 * Y) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 360199.0 } } } }, { "destinations": [ { "assignments": [ { "comment": "Y <- 30", "ref": "Y", "value": 30 } ], "location": "l", "probability": { "comment": "(((3/400 * Y) / 30) / (((3/400 * Y) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 360199.0 } } } } }, { "assignments": [ { "comment": "Y <- 90", "ref": "Y", "value": 90 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30) / (((3/400 * Y) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": 33.0, "op": "/", "right": 360199.0 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 360199.0 } } } } } ], "guard": { "comment": "(Y = 60)", "exp": { "left": "Y", "op": "=", "right": 60 } }, "location": "l", "rate": { "comment": "(((3/400 * Y) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 120) ^ 2))) * 10) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 360199.0 } } } }, { "destinations": [ { "assignments": [ { "comment": "Y <- 60", "ref": "Y", "value": 60 } ], "location": "l", "probability": { "comment": "(((3/400 * Y) / 30) / ((3/400 * Y) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 } } } } ], "guard": { "comment": "(Y = 90)", "exp": { "left": "Y", "op": "=", "right": 90 } }, "location": "l", "rate": { "comment": "((3/400 * Y) / 30)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "Y" }, "op": "/", "right": 30 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "Y_def", "variables": [] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "Z <- 30", "ref": "Z", "value": 30 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30) / ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } } } ], "guard": { "comment": "(Z = 0)", "exp": { "left": "Z", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30)", "exp": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } }, { "destinations": [ { "assignments": [ { "comment": "Z <- 0", "ref": "Z", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * Z) / 30) / (((3/400 * Z) / 30) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } } } }, { "assignments": [ { "comment": "Z <- 60", "ref": "Z", "value": 60 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30) / (((3/400 * Z) / 30) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } } } } ], "guard": { "comment": "(Z = 30)", "exp": { "left": "Z", "op": "=", "right": 30 } }, "location": "l", "rate": { "comment": "(((3/400 * Z) / 30) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } } }, { "destinations": [ { "assignments": [ { "comment": "Z <- 30", "ref": "Z", "value": 30 } ], "location": "l", "probability": { "comment": "(((3/400 * Z) / 30) / (((3/400 * Z) / 30) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } } } }, { "assignments": [ { "comment": "Z <- 90", "ref": "Z", "value": 90 } ], "location": "l", "probability": { "comment": "(((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30) / (((3/400 * Z) / 30) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30)))", "exp": { "left": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } } } } ], "guard": { "comment": "(Z = 60)", "exp": { "left": "Z", "op": "=", "right": 60 } }, "location": "l", "rate": { "comment": "(((3/400 * Z) / 30) + ((10 * (((99/1000 / (199/100 + ((1/2 * S4) ^ 2))) * 10) + ((99/1000 / (199/100 + ((1/2 * S3) ^ 2))) * 10))) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": { "left": 10, "op": "*", "right": { "left": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S4" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "+", "right": { "left": { "left": { "left": 99.0, "op": "/", "right": 1000.0 }, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "S3" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 } } }, "op": "/", "right": 30 } } } }, { "destinations": [ { "assignments": [ { "comment": "Z <- 60", "ref": "Z", "value": 60 } ], "location": "l", "probability": { "comment": "(((3/400 * Z) / 30) / ((3/400 * Z) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 } } } } ], "guard": { "comment": "(Z = 90)", "exp": { "left": "Z", "op": "=", "right": 90 } }, "location": "l", "rate": { "comment": "((3/400 * Z) / 30)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "Z" }, "op": "/", "right": 30 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "Z_def", "variables": [] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "CC <- 40", "ref": "CC", "value": 40 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40) / ((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40))", "exp": { "left": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } } } ], "guard": { "comment": "(CC = 0)", "exp": { "left": "CC", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40)", "exp": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } }, { "destinations": [ { "assignments": [ { "comment": "CC <- 0", "ref": "CC", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * CC) / 40) / (((3/400 * CC) / 40) + ((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } } } }, { "assignments": [ { "comment": "CC <- 80", "ref": "CC", "value": 80 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40) / (((3/400 * CC) / 40) + ((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40)))", "exp": { "left": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } } } } ], "guard": { "comment": "(CC = 40)", "exp": { "left": "CC", "op": "=", "right": 40 } }, "location": "l", "rate": { "comment": "(((3/400 * CC) / 40) + ((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } } }, { "destinations": [ { "assignments": [ { "comment": "CC <- 40", "ref": "CC", "value": 40 } ], "location": "l", "probability": { "comment": "(((3/400 * CC) / 40) / (((3/400 * CC) / 40) + ((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } } } }, { "assignments": [ { "comment": "CC <- 120", "ref": "CC", "value": 120 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40) / (((3/400 * CC) / 40) + ((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40)))", "exp": { "left": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } } } } ], "guard": { "comment": "(CC = 80)", "exp": { "left": "CC", "op": "=", "right": 80 } }, "location": "l", "rate": { "comment": "(((3/400 * CC) / 40) + ((((10 * 99/1000) / (199/100 + ((1/2 * Z) ^ 2))) * 10) / 40))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "+", "right": { "left": { "left": { "left": 0.99, "op": "/", "right": { "left": 1.99, "op": "+", "right": { "left": { "left": 0.5, "op": "*", "right": "Z" }, "op": "pow", "right": 2 } } }, "op": "*", "right": 10 }, "op": "/", "right": 40 } } } }, { "destinations": [ { "assignments": [ { "comment": "CC <- 80", "ref": "CC", "value": 80 } ], "location": "l", "probability": { "comment": "(((3/400 * CC) / 40) / ((3/400 * CC) / 40))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 } } } } ], "guard": { "comment": "(CC = 120)", "exp": { "left": "CC", "op": "=", "right": 120 } }, "location": "l", "rate": { "comment": "((3/400 * CC) / 40)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "CC" }, "op": "/", "right": 40 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "CC_def", "variables": [ { "initial-value": 120, "name": "CC", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 120 } } ] }, { "edges": [ { "destinations": [ { "assignments": [ { "comment": "XX <- 30", "ref": "XX", "value": 30 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30) / ((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30))", "exp": 1.0 } } ], "guard": { "comment": "(XX = 0)", "exp": { "left": "XX", "op": "=", "right": 0 } }, "location": "l", "rate": { "comment": "((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30)", "exp": { "left": 33.0, "op": "/", "right": 199.0 } } }, { "destinations": [ { "assignments": [ { "comment": "XX <- 0", "ref": "XX", "value": 0 } ], "location": "l", "probability": { "comment": "(((3/400 * XX) / 30) / (((3/400 * XX) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 199.0 } } } } }, { "assignments": [ { "comment": "XX <- 60", "ref": "XX", "value": 60 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30) / (((3/400 * XX) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": 33.0, "op": "/", "right": 199.0 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 199.0 } } } } } ], "guard": { "comment": "(XX = 30)", "exp": { "left": "XX", "op": "=", "right": 30 } }, "location": "l", "rate": { "comment": "(((3/400 * XX) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 199.0 } } } }, { "destinations": [ { "assignments": [ { "comment": "XX <- 30", "ref": "XX", "value": 30 } ], "location": "l", "probability": { "comment": "(((3/400 * XX) / 30) / (((3/400 * XX) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 199.0 } } } } }, { "assignments": [ { "comment": "XX <- 90", "ref": "XX", "value": 90 } ], "location": "l", "probability": { "comment": "(((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30) / (((3/400 * XX) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30)))", "exp": { "left": { "left": 33.0, "op": "/", "right": 199.0 }, "op": "/", "right": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 199.0 } } } } } ], "guard": { "comment": "(XX = 60)", "exp": { "left": "XX", "op": "=", "right": 60 } }, "location": "l", "rate": { "comment": "(((3/400 * XX) / 30) + ((((10 * 99/1000) / (199/100 + ((1/2 * 0) ^ 2))) * 10) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "+", "right": { "left": 33.0, "op": "/", "right": 199.0 } } } }, { "destinations": [ { "assignments": [ { "comment": "XX <- 60", "ref": "XX", "value": 60 } ], "location": "l", "probability": { "comment": "(((3/400 * XX) / 30) / ((3/400 * XX) / 30))", "exp": { "left": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 }, "op": "/", "right": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 } } } } ], "guard": { "comment": "(XX = 90)", "exp": { "left": "XX", "op": "=", "right": 90 } }, "location": "l", "rate": { "comment": "((3/400 * XX) / 30)", "exp": { "left": { "left": 0.0075, "op": "*", "right": "XX" }, "op": "/", "right": 30 } } } ], "initial-locations": [ "l" ], "locations": [ { "name": "l" } ], "name": "XX_def", "variables": [] } ], "constants": [ { "name": "T", "type": "int", "value": 2100 }, { "name": "AA", "type": "int", "value": 0 }, { "name": "B", "type": "int", "value": 120 } ], "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", "time-bounds": { "upper": 2100, "upper-exclusive": false } }, "op": "Pmin" } }, "name": "change_state" } ], "restrict-initial": { "exp": true }, "system": { "elements": [ { "automaton": "S1_def" }, { "automaton": "S2_def" }, { "automaton": "S3_def" }, { "automaton": "S4_def" }, { "automaton": "Y_def" }, { "automaton": "Z_def" }, { "automaton": "CC_def" }, { "automaton": "XX_def" } ] }, "type": "ctmc", "variables": [ { "initial-value": false, "name": "target", "transient": true, "type": "bool" }, { "initial-value": 200, "name": "S1", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 250 } }, { "initial-value": 0, "name": "S2", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 100 } }, { "initial-value": 120, "name": "S3", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 150 } }, { "initial-value": 0, "name": "S4", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 120 } }, { "initial-value": 0, "name": "Y", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 90 } }, { "initial-value": 0, "name": "Z", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 90 } }, { "initial-value": 0, "name": "XX", "type": { "base": "int", "kind": "bounded", "lower-bound": 0, "upper-bound": 90 } } ] }