|
|
{ "jani-version":1, "features":[ "derived-operators" ], "name":"Converted from PRISM by IscasMC", "type":"ctmc", "actions":[ { "name":"tau__" } ], "constants":[ { "name":"n", "type":"int" } ], "variables":[ { "name":"x1", "type":{ "kind":"bounded", "base":"int", "lower-bound":1, "upper-bound":"n" } }, { "name":"y1", "type":{ "kind":"bounded", "base":"int", "lower-bound":1, "upper-bound":"n" } }, { "name":"c", "type":{ "kind":"bounded", "base":"int", "lower-bound":0, "upper-bound":1 } }, { "name":"x2", "type":{ "kind":"bounded", "base":"int", "lower-bound":1, "upper-bound":"n" } }, { "name":"y2", "type":{ "kind":"bounded", "base":"int", "lower-bound":1, "upper-bound":"n" } } ], "observables":[ ], "initial-states":{ "exp":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"=", "left":"x1", "right":1 }, "right":{ "op":"=", "left":"y1", "right":1 } }, "right":{ "op":"=", "left":"c", "right":0 } }, "right":{ "op":"=", "left":"x2", "right":"n" } }, "right":{ "op":"=", "left":"y2", "right":"n" } } }, "automata":[ { "name":"robot", "locations":[ { "name":"location" } ], "initial-locations":[ "location" ], "edges":[ { "location":"location", "action":"tau__", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"<", "left":"x1", "right":"n" }, "right":{ "op":"=", "left":"c", "right":0 } }, "right":{ "op":"¬", "exp":{ "op":"∧", "left":{ "op":"=", "left":{ "op":"+", "left":"x1", "right":1 }, "right":"x2" }, "right":{ "op":"=", "left":"y1", "right":"y2" } } } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"x1", "value":{ "op":"+", "left":"x1", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"=", "left":"x1", "right":"n" }, "right":{ "op":"<", "left":"y1", "right":"n" } }, "right":{ "op":"=", "left":"c", "right":0 } }, "right":{ "op":"¬", "exp":{ "op":"∧", "left":{ "op":"=", "left":"x1", "right":"x2" }, "right":{ "op":"=", "left":{ "op":"+", "left":"y1", "right":1 }, "right":"y2" } } } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"y1", "value":{ "op":"+", "left":"y1", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":1, "right":10 } }, "guard":{ "exp":{ "op":"=", "left":"c", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":1, "right":10 }, "right":{ "op":"/", "left":1, "right":10 } } }, "location":"location", "assignments":[ { "ref":"c", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":1, "right":2 } }, "guard":{ "exp":{ "op":"=", "left":"c", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":1, "right":2 }, "right":{ "op":"/", "left":1, "right":2 } } }, "location":"location", "assignments":[ { "ref":"c", "value":0 } ], "observables":[ ] } ] } ] }, { "name":"janitor", "locations":[ { "name":"location" } ], "initial-locations":[ "location" ], "edges":[ { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } }, "guard":{ "exp":{ "op":"¬", "exp":{ "op":"∨", "left":{ "op":"=", "left":"y2", "right":"n" }, "right":{ "op":"∧", "left":{ "op":"=", "left":{ "op":"+", "left":"y2", "right":1 }, "right":"y1" }, "right":{ "op":"=", "left":"x2", "right":"x1" } } } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } }, "right":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } } }, "location":"location", "assignments":[ { "ref":"y2", "value":{ "op":"+", "left":"y2", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } }, "guard":{ "exp":{ "op":"¬", "exp":{ "op":"∨", "left":{ "op":"=", "left":"y2", "right":1 }, "right":{ "op":"∧", "left":{ "op":"=", "left":{ "op":"-", "left":"y2", "right":1 }, "right":"y1" }, "right":{ "op":"=", "left":"x2", "right":"x1" } } } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } }, "right":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } } }, "location":"location", "assignments":[ { "ref":"y2", "value":{ "op":"-", "left":"y2", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } }, "guard":{ "exp":{ "op":"¬", "exp":{ "op":"∨", "left":{ "op":"=", "left":"x2", "right":1 }, "right":{ "op":"∧", "left":{ "op":"=", "left":{ "op":"-", "left":"x2", "right":1 }, "right":"x1" }, "right":{ "op":"=", "left":"y2", "right":"y1" } } } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } }, "right":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } } }, "location":"location", "assignments":[ { "ref":"x2", "value":{ "op":"-", "left":"x2", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } }, "guard":{ "exp":{ "op":"¬", "exp":{ "op":"∨", "left":{ "op":"=", "left":"x2", "right":"n" }, "right":{ "op":"∧", "left":{ "op":"=", "left":{ "op":"+", "left":"x2", "right":1 }, "right":"x1" }, "right":{ "op":"=", "left":"y2", "right":"y1" } } } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } }, "right":{ "op":"/", "left":2, "right":{ "op":"+", "left":{ "op":"+", "left":{ "op":"+", "left":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"x2" }, "right":0 } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"x2", "right":1 }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"n", "right":"y2" }, "right":0 } } }, "right":{ "op":"min", "left":1, "right":{ "op":"max", "left":{ "op":"-", "left":"y2", "right":1 }, "right":0 } } } } } }, "location":"location", "assignments":[ { "ref":"x2", "value":{ "op":"+", "left":"x2", "right":1 } } ], "observables":[ ] } ] } ] } ], "system":{ "elements":[ { "automaton":"robot" }, { "automaton":"janitor" } ], "syncs":[ { "synchronise":[ "tau__", null ], "result":"tau__" }, { "synchronise":[ null, "tau__" ], "result":"tau__" } ] }}
|
