|
|
{ "jani-version":1, "features":[ "derived-operators" ], "name":"Converted from PRISM by IscasMC", "type":"ctmc", "actions":[ { "name":"loop1a" }, { "name":"loop1b" }, { "name":"serve1" }, { "name":"loop2a" }, { "name":"loop2b" }, { "name":"serve2" }, { "name":"loop3a" }, { "name":"loop3b" }, { "name":"serve3" }, { "name":"loop4a" }, { "name":"loop4b" }, { "name":"serve4" }, { "name":"tau__" } ], "variables":[ { "name":"s", "type":{ "kind":"bounded", "base":"int", "lower-bound":1, "upper-bound":4 } }, { "name":"a", "type":{ "kind":"bounded", "base":"int", "lower-bound":0, "upper-bound":1 } }, { "name":"s1", "type":{ "kind":"bounded", "base":"int", "lower-bound":0, "upper-bound":1 } }, { "name":"s2", "type":{ "kind":"bounded", "base":"int", "lower-bound":0, "upper-bound":1 } }, { "name":"s3", "type":{ "kind":"bounded", "base":"int", "lower-bound":0, "upper-bound":1 } }, { "name":"s4", "type":{ "kind":"bounded", "base":"int", "lower-bound":0, "upper-bound":1 } } ], "observables":[ { "name":"\"waiting\"" }, { "name":"\"served\"" } ], "initial-states":{ "exp":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":1 }, "right":{ "op":"=", "left":"a", "right":0 } }, "right":{ "op":"=", "left":"s1", "right":0 } }, "right":{ "op":"=", "left":"s2", "right":0 } }, "right":{ "op":"=", "left":"s3", "right":0 } }, "right":{ "op":"=", "left":"s4", "right":0 } } }, "automata":[ { "name":"server", "locations":[ { "name":"location", "observables":[ { "ref":"\"waiting\"", "value":{ "op":"?:", "args":[ { "op":"∧", "left":{ "op":"=", "left":"s1", "right":1 }, "right":{ "op":"¬", "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":1 }, "right":{ "op":"=", "left":"a", "right":1 } } } }, 1, 0 ] } } ] } ], "initial-locations":[ "location" ], "edges":[ { "location":"location", "action":"loop1a", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":1 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"s", "value":{ "op":"+", "left":"s", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"loop1b", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":1 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"a", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"serve1", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":1 }, "right":{ "op":"=", "left":"a", "right":1 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s", "value":{ "op":"+", "left":"s", "right":1 } }, { "ref":"a", "value":0 } ], "observables":[ { "ref":"\"served\"", "value":1 } ] } ] }, { "location":"location", "action":"loop2a", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":2 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"s", "value":{ "op":"+", "left":"s", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"loop2b", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":2 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"a", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"serve2", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":2 }, "right":{ "op":"=", "left":"a", "right":1 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s", "value":{ "op":"+", "left":"s", "right":1 } }, { "ref":"a", "value":0 } ], "observables":[ ] } ] }, { "location":"location", "action":"loop3a", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":3 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"s", "value":{ "op":"+", "left":"s", "right":1 } } ], "observables":[ ] } ] }, { "location":"location", "action":"loop3b", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":3 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"a", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"serve3", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":3 }, "right":{ "op":"=", "left":"a", "right":1 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s", "value":{ "op":"+", "left":"s", "right":1 } }, { "ref":"a", "value":0 } ], "observables":[ ] } ] }, { "location":"location", "action":"loop4a", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":4 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"s", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"loop4b", "rate":{ "exp":200 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":4 }, "right":{ "op":"=", "left":"a", "right":0 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":200, "right":200 } }, "location":"location", "assignments":[ { "ref":"a", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"serve4", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"∧", "left":{ "op":"=", "left":"s", "right":4 }, "right":{ "op":"=", "left":"a", "right":1 } } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s", "value":1 }, { "ref":"a", "value":0 } ], "observables":[ ] } ] } ] }, { "name":"station1", "locations":[ { "name":"location" } ], "initial-locations":[ "location" ], "edges":[ { "location":"location", "action":"loop1a", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s1", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s1", "value":0 } ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":1, "right":4 } }, "guard":{ "exp":{ "op":"=", "left":"s1", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":1, "right":4 }, "right":{ "op":"/", "left":1, "right":4 } } }, "location":"location", "assignments":[ { "ref":"s1", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"loop1b", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s1", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s1", "value":1 } ] } ] }, { "location":"location", "action":"serve1", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s1", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s1", "value":0 } ] } ] } ] }, { "name":"station2", "locations":[ { "name":"location" } ], "initial-locations":[ "location" ], "edges":[ { "location":"location", "action":"loop2a", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s2", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s2", "value":0 } ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":1, "right":4 } }, "guard":{ "exp":{ "op":"=", "left":"s2", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":1, "right":4 }, "right":{ "op":"/", "left":1, "right":4 } } }, "location":"location", "assignments":[ { "ref":"s2", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"loop2b", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s2", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s2", "value":1 } ] } ] }, { "location":"location", "action":"serve2", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s2", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s2", "value":0 } ] } ] } ] }, { "name":"station3", "locations":[ { "name":"location" } ], "initial-locations":[ "location" ], "edges":[ { "location":"location", "action":"loop3a", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s3", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s3", "value":0 } ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":1, "right":4 } }, "guard":{ "exp":{ "op":"=", "left":"s3", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":1, "right":4 }, "right":{ "op":"/", "left":1, "right":4 } } }, "location":"location", "assignments":[ { "ref":"s3", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"loop3b", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s3", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s3", "value":1 } ] } ] }, { "location":"location", "action":"serve3", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s3", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s3", "value":0 } ] } ] } ] }, { "name":"station4", "locations":[ { "name":"location" } ], "initial-locations":[ "location" ], "edges":[ { "location":"location", "action":"loop4a", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s4", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s4", "value":0 } ] } ] }, { "location":"location", "action":"tau__", "rate":{ "exp":{ "op":"/", "left":1, "right":4 } }, "guard":{ "exp":{ "op":"=", "left":"s4", "right":0 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":{ "op":"/", "left":1, "right":4 }, "right":{ "op":"/", "left":1, "right":4 } } }, "location":"location", "assignments":[ { "ref":"s4", "value":1 } ], "observables":[ ] } ] }, { "location":"location", "action":"loop4b", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s4", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s4", "value":1 } ] } ] }, { "location":"location", "action":"serve4", "rate":{ "exp":1 }, "guard":{ "exp":{ "op":"=", "left":"s4", "right":1 } }, "destinations":[ { "probability":{ "exp":{ "op":"/", "left":1, "right":1 } }, "location":"location", "assignments":[ { "ref":"s4", "value":0 } ] } ] } ] } ], "system":{ "elements":[ { "automaton":"server" }, { "automaton":"station1" }, { "automaton":"station2" }, { "automaton":"station3" }, { "automaton":"station4" } ], "syncs":[ { "synchronise":[ "loop4a", null, null, null, "loop4a" ], "result":"loop4a" }, { "synchronise":[ "loop4b", null, null, null, "loop4b" ], "result":"loop4b" }, { "synchronise":[ "serve4", null, null, null, "serve4" ], "result":"serve4" }, { "synchronise":[ "loop3a", null, null, "loop3a", null ], "result":"loop3a" }, { "synchronise":[ "loop3b", null, null, "loop3b", null ], "result":"loop3b" }, { "synchronise":[ "serve3", null, null, "serve3", null ], "result":"serve3" }, { "synchronise":[ "loop2a", null, "loop2a", null, null ], "result":"loop2a" }, { "synchronise":[ "loop2b", null, "loop2b", null, null ], "result":"loop2b" }, { "synchronise":[ "serve2", null, "serve2", null, null ], "result":"serve2" }, { "synchronise":[ "loop1a", "loop1a", null, null, null ], "result":"loop1a" }, { "synchronise":[ "loop1b", "loop1b", null, null, null ], "result":"loop1b" }, { "synchronise":[ "serve1", "serve1", null, null, null ], "result":"serve1" }, { "synchronise":[ null, "tau__", null, null, null ], "result":"tau__" }, { "synchronise":[ null, null, "tau__", null, null ], "result":"tau__" }, { "synchronise":[ null, null, null, "tau__", null ], "result":"tau__" }, { "synchronise":[ null, null, null, null, "tau__" ], "result":"tau__" } ] }}
|
