diff --git a/lib/stormpy/examples/files/dtmc/brp.jani b/lib/stormpy/examples/files/dtmc/brp.jani new file mode 100644 index 0000000..8420dc2 --- /dev/null +++ b/lib/stormpy/examples/files/dtmc/brp.jani @@ -0,0 +1,2033 @@ + +{ + "jani-version":1, + "name":"brp", + "type":"dtmc", + "features":[ + "derived-operators" + ], + "actions":[ + { + "name":"NewFile" + }, + { + "name":"aF" + }, + { + "name":"aB" + }, + { + "name":"TO_Msg" + }, + { + "name":"TO_Ack" + }, + { + "name":"τ" + }, + { + "name":"SyncWait" + }, + { + "name":"aG" + }, + { + "name":"aA" + } + ], + "constants":[ + { + "name":"N", + "type":"int" + }, + { + "name":"MAX", + "type":"int" + } + ], + "variables":[ + { + "name":"s", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":6 + } + }, + { + "name":"srep", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":3 + } + }, + { + "name":"nrtr", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":"MAX" + } + }, + { + "name":"i", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":"N" + } + }, + { + "name":"bs", + "type":"bool" + }, + { + "name":"s_ab", + "type":"bool" + }, + { + "name":"fs", + "type":"bool" + }, + { + "name":"ls", + "type":"bool" + }, + { + "name":"r", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":5 + } + }, + { + "name":"rrep", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":4 + } + }, + { + "name":"fr", + "type":"bool" + }, + { + "name":"lr", + "type":"bool" + }, + { + "name":"br", + "type":"bool" + }, + { + "name":"r_ab", + "type":"bool" + }, + { + "name":"recv", + "type":"bool" + }, + { + "name":"T", + "type":"bool" + }, + { + "name":"k", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":2 + } + }, + { + "name":"l", + "type":{ + "kind":"bounded", + "base":"int", + "lower-bound":0, + "upper-bound":2 + } + }, + { + "name":"reward_", + "type":"real", + "initial-value":0.0, + "transient":true + } + ], + "restrict-initial":{ + "exp":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":0 + }, + "right":{ + "op":"=", + "left":"srep", + "right":0 + } + }, + "right":{ + "op":"=", + "left":"nrtr", + "right":0 + } + }, + "right":{ + "op":"=", + "left":"i", + "right":0 + } + }, + "right":{ + "op":"=", + "left":"bs", + "right":false + } + }, + "right":{ + "op":"=", + "left":"s_ab", + "right":false + } + }, + "right":{ + "op":"=", + "left":"fs", + "right":false + } + }, + "right":{ + "op":"=", + "left":"ls", + "right":false + } + }, + "right":{ + "op":"=", + "left":"r", + "right":0 + } + }, + "right":{ + "op":"=", + "left":"rrep", + "right":0 + } + }, + "right":{ + "op":"=", + "left":"fr", + "right":false + } + }, + "right":{ + "op":"=", + "left":"lr", + "right":false + } + }, + "right":{ + "op":"=", + "left":"br", + "right":false + } + }, + "right":{ + "op":"=", + "left":"r_ab", + "right":false + } + }, + "right":{ + "op":"=", + "left":"recv", + "right":false + } + }, + "right":{ + "op":"=", + "left":"T", + "right":false + } + }, + "right":{ + "op":"=", + "left":"k", + "right":0 + } + }, + "right":{ + "op":"=", + "left":"l", + "right":0 + } + } + }, + "properties":[ + { + "name":"Property_brp_0", + "expression":{ + "op":"filter", + "fun":"min", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"srep", + "right":1 + }, + "right":{ + "op":"=", + "left":"rrep", + "right":3 + } + }, + "right":"recv" + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F srep=1 & rrep=3 & recv ]" + }, + { + "name":"Property_brp_1", + "expression":{ + "op":"filter", + "fun":"max", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"srep", + "right":1 + }, + "right":{ + "op":"=", + "left":"rrep", + "right":3 + } + }, + "right":"recv" + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F srep=1 & rrep=3 & recv ]" + }, + { + "name":"Property_brp_2", + "expression":{ + "op":"filter", + "fun":"min", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"srep", + "right":3 + }, + "right":{ + "op":"¬", + "exp":{ + "op":"=", + "left":"rrep", + "right":3 + } + } + }, + "right":"recv" + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F srep=3 & !(rrep=3) & recv ]" + }, + { + "name":"Property_brp_3", + "expression":{ + "op":"filter", + "fun":"max", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"srep", + "right":3 + }, + "right":{ + "op":"¬", + "exp":{ + "op":"=", + "left":"rrep", + "right":3 + } + } + }, + "right":"recv" + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F srep=3 & !(rrep=3) & recv ]" + }, + { + "name":"Property_brp_4", + "expression":{ + "op":"filter", + "fun":"min", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"=", + "left":"s", + "right":5 + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F s=5 ]" + }, + { + "name":"Property_brp_5", + "expression":{ + "op":"filter", + "fun":"max", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"=", + "left":"s", + "right":5 + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F s=5 ]" + }, + { + "name":"Property_brp_6", + "expression":{ + "op":"filter", + "fun":"min", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":5 + }, + "right":{ + "op":"=", + "left":"srep", + "right":2 + } + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F s=5 & srep=2 ]" + }, + { + "name":"Property_brp_7", + "expression":{ + "op":"filter", + "fun":"max", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":5 + }, + "right":{ + "op":"=", + "left":"srep", + "right":2 + } + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F s=5 & srep=2 ]" + }, + { + "name":"Property_brp_8", + "expression":{ + "op":"filter", + "fun":"min", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":5 + }, + "right":{ + "op":"=", + "left":"srep", + "right":1 + } + }, + "right":{ + "op":">", + "left":"i", + "right":8 + } + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F s=5 & srep=1 & i>8 ]" + }, + { + "name":"Property_brp_9", + "expression":{ + "op":"filter", + "fun":"max", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":5 + }, + "right":{ + "op":"=", + "left":"srep", + "right":1 + } + }, + "right":{ + "op":">", + "left":"i", + "right":8 + } + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F s=5 & srep=1 & i>8 ]" + }, + { + "name":"Property_brp_10", + "expression":{ + "op":"filter", + "fun":"min", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"¬", + "exp":{ + "op":"=", + "left":"srep", + "right":0 + } + }, + "right":{ + "op":"¬", + "exp":"recv" + } + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F !(srep=0) & !recv ]" + }, + { + "name":"Property_brp_11", + "expression":{ + "op":"filter", + "fun":"max", + "values":{ + "op":"Pmax", + "exp":{ + "op":"U", + "left":true, + "right":{ + "op":"∧", + "left":{ + "op":"¬", + "exp":{ + "op":"=", + "left":"srep", + "right":0 + } + }, + "right":{ + "op":"¬", + "exp":"recv" + } + } + } + }, + "states":{ + "op":"initial" + } + }, + "comment":"P=?[ F !(srep=0) & !recv ]" + } + ], + "automata":[ + { + "name":"sender", + "locations":[ + { + "name":"location" + } + ], + "initial-locations":[ + "location" + ], + "edges":[ + { + "location":"location", + "action":"NewFile", + "guard":{ + "exp":{ + "op":"=", + "left":"s", + "right":0 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":1 + }, + { + "ref":"i", + "value":1 + }, + { + "ref":"srep", + "value":0 + } + ] + } + ] + }, + { + "location":"location", + "action":"aF", + "guard":{ + "exp":{ + "op":"=", + "left":"s", + "right":1 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":2 + }, + { + "ref":"fs", + "value":{ + "op":"=", + "left":"i", + "right":1 + } + }, + { + "ref":"ls", + "value":{ + "op":"=", + "left":"i", + "right":"N" + } + }, + { + "ref":"bs", + "value":"s_ab" + }, + { + "ref":"nrtr", + "value":0 + }, + { + "ref":"reward_", + "value":{ + "op":"ite", + "if":{ + "op":"=", + "left":"i", + "right":1 + }, + "then":1, + "else":0 + } + } + ] + } + ] + }, + { + "location":"location", + "action":"aB", + "guard":{ + "exp":{ + "op":"=", + "left":"s", + "right":2 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":4 + }, + { + "ref":"s_ab", + "value":{ + "op":"¬", + "exp":"s_ab" + } + } + ] + } + ] + }, + { + "location":"location", + "action":"TO_Msg", + "guard":{ + "exp":{ + "op":"=", + "left":"s", + "right":2 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":3 + } + ] + } + ] + }, + { + "location":"location", + "action":"TO_Ack", + "guard":{ + "exp":{ + "op":"=", + "left":"s", + "right":2 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":3 + } + ] + } + ] + }, + { + "location":"location", + "action":"aF", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":3 + }, + "right":{ + "op":"<", + "left":"nrtr", + "right":"MAX" + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":2 + }, + { + "ref":"fs", + "value":{ + "op":"=", + "left":"i", + "right":1 + } + }, + { + "ref":"ls", + "value":{ + "op":"=", + "left":"i", + "right":"N" + } + }, + { + "ref":"bs", + "value":"s_ab" + }, + { + "ref":"nrtr", + "value":{ + "op":"+", + "left":"nrtr", + "right":1 + } + }, + { + "ref":"reward_", + "value":{ + "op":"ite", + "if":{ + "op":"=", + "left":"i", + "right":1 + }, + "then":1, + "else":0 + } + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":3 + }, + "right":{ + "op":"=", + "left":"nrtr", + "right":"MAX" + } + }, + "right":{ + "op":"<", + "left":"i", + "right":"N" + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":5 + }, + { + "ref":"srep", + "value":1 + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":3 + }, + "right":{ + "op":"=", + "left":"nrtr", + "right":"MAX" + } + }, + "right":{ + "op":"=", + "left":"i", + "right":"N" + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":5 + }, + { + "ref":"srep", + "value":2 + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":4 + }, + "right":{ + "op":"<", + "left":"i", + "right":"N" + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":1 + }, + { + "ref":"i", + "value":{ + "op":"+", + "left":"i", + "right":1 + } + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"=", + "left":"s", + "right":4 + }, + "right":{ + "op":"=", + "left":"i", + "right":"N" + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":0 + }, + { + "ref":"srep", + "value":3 + } + ] + } + ] + }, + { + "location":"location", + "action":"SyncWait", + "guard":{ + "exp":{ + "op":"=", + "left":"s", + "right":5 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":6 + } + ] + } + ] + }, + { + "location":"location", + "action":"SyncWait", + "guard":{ + "exp":{ + "op":"=", + "left":"s", + "right":6 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"s", + "value":0 + }, + { + "ref":"s_ab", + "value":false + } + ] + } + ] + } + ] + }, + { + "name":"receiver", + "locations":[ + { + "name":"location" + } + ], + "initial-locations":[ + "location" + ], + "edges":[ + { + "location":"location", + "action":"SyncWait", + "guard":{ + "exp":{ + "op":"=", + "left":"r", + "right":0 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":0 + } + ] + } + ] + }, + { + "location":"location", + "action":"aG", + "guard":{ + "exp":{ + "op":"=", + "left":"r", + "right":0 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":1 + }, + { + "ref":"fr", + "value":"fs" + }, + { + "ref":"lr", + "value":"ls" + }, + { + "ref":"br", + "value":"bs" + }, + { + "ref":"recv", + "value":"T" + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"=", + "left":"r", + "right":1 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":2 + }, + { + "ref":"r_ab", + "value":"br" + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"r", + "right":2 + }, + "right":{ + "op":"=", + "left":"r_ab", + "right":"br" + } + }, + "right":{ + "op":"=", + "left":"fr", + "right":true + } + }, + "right":{ + "op":"=", + "left":"lr", + "right":false + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":3 + }, + { + "ref":"rrep", + "value":1 + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"r", + "right":2 + }, + "right":{ + "op":"=", + "left":"r_ab", + "right":"br" + } + }, + "right":{ + "op":"=", + "left":"fr", + "right":false + } + }, + "right":{ + "op":"=", + "left":"lr", + "right":false + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":3 + }, + { + "ref":"rrep", + "value":2 + } + ] + } + ] + }, + { + "location":"location", + "action":"τ", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"∧", + "left":{ + "op":"=", + "left":"r", + "right":2 + }, + "right":{ + "op":"=", + "left":"r_ab", + "right":"br" + } + }, + "right":{ + "op":"=", + "left":"fr", + "right":false + } + }, + "right":{ + "op":"=", + "left":"lr", + "right":true + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":3 + }, + { + "ref":"rrep", + "value":3 + } + ] + } + ] + }, + { + "location":"location", + "action":"aA", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"=", + "left":"r", + "right":2 + }, + "right":{ + "op":"¬", + "exp":{ + "op":"=", + "left":"r_ab", + "right":"br" + } + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":4 + } + ] + } + ] + }, + { + "location":"location", + "action":"aA", + "guard":{ + "exp":{ + "op":"=", + "left":"r", + "right":3 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":4 + }, + { + "ref":"r_ab", + "value":{ + "op":"¬", + "exp":"r_ab" + } + } + ] + } + ] + }, + { + "location":"location", + "action":"aG", + "guard":{ + "exp":{ + "op":"=", + "left":"r", + "right":4 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":2 + }, + { + "ref":"fr", + "value":"fs" + }, + { + "ref":"lr", + "value":"ls" + }, + { + "ref":"br", + "value":"bs" + }, + { + "ref":"recv", + "value":"T" + } + ] + } + ] + }, + { + "location":"location", + "action":"SyncWait", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"=", + "left":"r", + "right":4 + }, + "right":{ + "op":"=", + "left":"ls", + "right":true + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":5 + } + ] + } + ] + }, + { + "location":"location", + "action":"SyncWait", + "guard":{ + "exp":{ + "op":"∧", + "left":{ + "op":"=", + "left":"r", + "right":4 + }, + "right":{ + "op":"=", + "left":"ls", + "right":false + } + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":5 + }, + { + "ref":"rrep", + "value":4 + } + ] + } + ] + }, + { + "location":"location", + "action":"SyncWait", + "guard":{ + "exp":{ + "op":"=", + "left":"r", + "right":5 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"r", + "value":0 + }, + { + "ref":"rrep", + "value":0 + } + ] + } + ] + } + ] + }, + { + "name":"checker", + "locations":[ + { + "name":"location" + } + ], + "initial-locations":[ + "location" + ], + "edges":[ + { + "location":"location", + "action":"NewFile", + "guard":{ + "exp":{ + "op":"=", + "left":"T", + "right":false + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"T", + "value":true + } + ] + } + ] + } + ] + }, + { + "name":"channelK", + "locations":[ + { + "name":"location" + } + ], + "initial-locations":[ + "location" + ], + "edges":[ + { + "location":"location", + "action":"aF", + "guard":{ + "exp":{ + "op":"=", + "left":"k", + "right":0 + } + }, + "destinations":[ + { + "probability":{ + "exp":0.9800000 + }, + "location":"location", + "assignments":[ + { + "ref":"k", + "value":1 + } + ] + }, + { + "probability":{ + "exp":0.0200000 + }, + "location":"location", + "assignments":[ + { + "ref":"k", + "value":2 + } + ] + } + ] + }, + { + "location":"location", + "action":"aG", + "guard":{ + "exp":{ + "op":"=", + "left":"k", + "right":1 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"k", + "value":0 + } + ] + } + ] + }, + { + "location":"location", + "action":"TO_Msg", + "guard":{ + "exp":{ + "op":"=", + "left":"k", + "right":2 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"k", + "value":0 + } + ] + } + ] + } + ] + }, + { + "name":"channelL", + "locations":[ + { + "name":"location" + } + ], + "initial-locations":[ + "location" + ], + "edges":[ + { + "location":"location", + "action":"aA", + "guard":{ + "exp":{ + "op":"=", + "left":"l", + "right":0 + } + }, + "destinations":[ + { + "probability":{ + "exp":0.9900000 + }, + "location":"location", + "assignments":[ + { + "ref":"l", + "value":1 + } + ] + }, + { + "probability":{ + "exp":0.0100000 + }, + "location":"location", + "assignments":[ + { + "ref":"l", + "value":2 + } + ] + } + ] + }, + { + "location":"location", + "action":"aB", + "guard":{ + "exp":{ + "op":"=", + "left":"l", + "right":1 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"l", + "value":0 + } + ] + } + ] + }, + { + "location":"location", + "action":"TO_Ack", + "guard":{ + "exp":{ + "op":"=", + "left":"l", + "right":2 + } + }, + "destinations":[ + { + "probability":{ + "exp":1 + }, + "location":"location", + "assignments":[ + { + "ref":"l", + "value":0 + } + ] + } + ] + } + ] + } + ], + "system":{ + "elements":[ + { + "automaton":"sender" + }, + { + "automaton":"receiver" + }, + { + "automaton":"checker" + }, + { + "automaton":"channelK" + }, + { + "automaton":"channelL" + } + ], + "syncs":[ + { + "synchronise":[ + "aB", + null, + null, + null, + "aB" + ], + "result":"aB" + }, + { + "synchronise":[ + "TO_Ack", + null, + null, + null, + "TO_Ack" + ], + "result":"TO_Ack" + }, + { + "synchronise":[ + null, + "aA", + null, + null, + "aA" + ], + "result":"aA" + }, + { + "synchronise":[ + "aF", + null, + null, + "aF", + null + ], + "result":"aF" + }, + { + "synchronise":[ + "TO_Msg", + null, + null, + "TO_Msg", + null + ], + "result":"TO_Msg" + }, + { + "synchronise":[ + null, + "aG", + null, + "aG", + null + ], + "result":"aG" + }, + { + "synchronise":[ + "NewFile", + null, + "NewFile", + null, + null + ], + "result":"NewFile" + }, + { + "synchronise":[ + "SyncWait", + "SyncWait", + null, + null, + null + ], + "result":"SyncWait" + }, + { + "synchronise":[ + "τ", + null, + null, + null, + null + ], + "result":"τ" + }, + { + "synchronise":[ + null, + "τ", + null, + null, + null + ], + "result":"τ" + } + ] + } +} diff --git a/src/core/input.cpp b/src/core/input.cpp index b5152a3..6786588 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -14,8 +14,10 @@ void define_property(py::module& m) { // Define python bindings void define_input(py::module& m) { - // Parse prism program - m.def("parse_prism_program", &storm::api::parseProgram, "Parse prism program", py::arg("path")); + // Parse Prism program + m.def("parse_prism_program", &storm::api::parseProgram, "Parse Prism program", py::arg("path")); + // Parse Jani model + m.def("parse_jani_model", &storm::api::parseJaniModel, "Parse Jani model", py::arg("path")); // PrismType py::enum_(m, "PrismModelType", "Type of the prism model") @@ -27,13 +29,6 @@ void define_input(py::module& m) { .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED) ; - // Jani Model - py::class_(m, "JaniModel", "Jani Model") - .def_property_readonly("name", &storm::jani::Model::getName, "Name of the jani model") - .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type"); - - - // PrismProgram py::class_(m, "PrismProgram", "Prism program") .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules") @@ -41,13 +36,43 @@ void define_input(py::module& m) { .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants") .def("__str__", &streamToString) ; + + // JaniType + py::enum_(m, "JaniModelType", "Type of the Jani model") + .value("DTMC", storm::jani::ModelType::DTMC) + .value("CTMC", storm::jani::ModelType::CTMC) + .value("MDP", storm::jani::ModelType::MDP) + .value("CTMDP", storm::jani::ModelType::CTMDP) + .value("MA", storm::jani::ModelType::MA) + .value("LTS", storm::jani::ModelType::LTS) + .value("TA", storm::jani::ModelType::TA) + .value("PTA", storm::jani::ModelType::PTA) + .value("STA", storm::jani::ModelType::STA) + .value("HA", storm::jani::ModelType::HA) + .value("PHA", storm::jani::ModelType::PHA) + .value("SHA", storm::jani::ModelType::SHA) + .value("UNDEFINED", storm::jani::ModelType::UNDEFINED) + ; + + // Jani Model + py::class_(m, "JaniModel", "Jani Model") + .def_property_readonly("name", &storm::jani::Model::getName, "Name of the jani model") + .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type") + .def_property_readonly("has_undefined_constants", &storm::jani::Model::hasUndefinedConstants, "Flag if Jani model has undefined constants") + ; // SymbolicModelDescription py::class_(m, "SymbolicModelDescription", "Symbolic description of model") .def(py::init(), "Construct from Prism program", py::arg("prism_program")) + .def(py::init(), "Construct from Jani model", py::arg("jani_model")) .def_property_readonly("is_prism_program", &storm::storage::SymbolicModelDescription::isPrismProgram, "Flag if program is in Prism format") + .def_property_readonly("is_jani_model", &storm::storage::SymbolicModelDescription::isJaniModel, "Flag if program is in Jani format") + .def("instantiate_constants", [](storm::storage::SymbolicModelDescription const& description, std::map const& constantDefinitions) { + return description.preprocess(constantDefinitions); + }, "Instantiate constants in symbolic model description", py::arg("constant_definitions")) ; - // PrismProgram can be converted into SymbolicModelDescription + // PrismProgram and JaniModel can be converted into SymbolicModelDescription py::implicitly_convertible(); + py::implicitly_convertible(); } diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 910311d..22d2737 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -9,6 +9,9 @@ class TestParse: assert program.nr_modules == 1 assert program.model_type == stormpy.PrismModelType.DTMC assert not program.has_undefined_constants + description = stormpy.SymbolicModelDescription(program) + assert description.is_prism_program + assert not description.is_jani_model def test_parse_parametric_prism_program(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) @@ -16,6 +19,15 @@ class TestParse: assert program.model_type == stormpy.PrismModelType.DTMC assert program.has_undefined_constants + def test_parse_jani_model(self): + jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) + assert jani_model.name == "brp" + assert jani_model.model_type == stormpy.JaniModelType.DTMC + assert jani_model.has_undefined_constants + description = stormpy.SymbolicModelDescription(jani_model) + assert not description.is_prism_program + assert description.is_jani_model + def test_parse_formula(self): formula = "P=? [F \"one\"]" properties = stormpy.parse_properties(formula)