From 330bbfcf5eefb52b3b22dfa6cfd598ec9ce3e5b3 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 18 May 2016 17:57:43 +0200 Subject: [PATCH] jani examples Former-commit-id: 612da4705f85bbc152225687567e2bd84d32a575 --- examples/jani-examples/beb.jani | 2604 +++++++++++++++++ examples/jani-examples/beb.jani.txt | 27 + examples/jani-examples/beb.modest | 64 + examples/jani-examples/beb.modest.txt | 27 + examples/jani-examples/brp.jani | 2092 +++++++++++++ examples/jani-examples/brp.jani.txt | 63 + examples/jani-examples/brp.modest | 213 ++ examples/jani-examples/brp.modest.txt | 63 + examples/jani-examples/consensus-6.jani | 2129 ++++++++++++++ examples/jani-examples/consensus-6.jani.txt | 27 + examples/jani-examples/consensus-6.modest | 157 + examples/jani-examples/consensus-6.modest.txt | 27 + examples/jani-examples/dice.jani | 354 +++ examples/jani-examples/dice.jani.txt | 29 + 14 files changed, 7876 insertions(+) create mode 100755 examples/jani-examples/beb.jani create mode 100755 examples/jani-examples/beb.jani.txt create mode 100755 examples/jani-examples/beb.modest create mode 100755 examples/jani-examples/beb.modest.txt create mode 100755 examples/jani-examples/brp.jani create mode 100755 examples/jani-examples/brp.jani.txt create mode 100755 examples/jani-examples/brp.modest create mode 100755 examples/jani-examples/brp.modest.txt create mode 100755 examples/jani-examples/consensus-6.jani create mode 100755 examples/jani-examples/consensus-6.jani.txt create mode 100755 examples/jani-examples/consensus-6.modest create mode 100755 examples/jani-examples/consensus-6.modest.txt create mode 100755 examples/jani-examples/dice.jani create mode 100755 examples/jani-examples/dice.jani.txt diff --git a/examples/jani-examples/beb.jani b/examples/jani-examples/beb.jani new file mode 100755 index 000000000..df2d43c66 --- /dev/null +++ b/examples/jani-examples/beb.jani @@ -0,0 +1,2604 @@ +{ + "jani-version": 1, + "name": "modelName", + "type": "mdp", + "actions": [ + { + "name": "tick" + }, + { + "name": "tack" + }, + { + "name": "tock" + } + ], + "variables": [ + { + "name": "cr", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 2 + }, + "initial-value": 0 + }, + { + "name": "line_seized", + "type": "bool", + "initial-value": false + }, + { + "name": "gave_up", + "type": "bool", + "initial-value": false + } + ], + "properties": [ + { + "name": "LineSeized", + "reach": "line_seized", + "type": "probability-max-query" + }, + { + "name": "GaveUp", + "reach": "gave_up", + "type": "probability-max-query" + } + ], + "automata": [ + { + "name": "Clock", + "variables": [], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_1" + } + ] + }, + { + "location": "l_1", + "action": "tack", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_2" + } + ] + }, + { + "location": "l_2", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "cr", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "tock", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + } + ] + }, + { + "name": "Host", + "variables": [ + { + "name": "na", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 3 + }, + "initial-value": 0 + }, + { + "name": "ev", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 4 + }, + "initial-value": 2 + }, + { + "name": "wt", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 4 + }, + "initial-value": 0 + } + ], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + }, + { + "name": "l_4" + }, + { + "name": "l_5" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "tick", + "guard": { + "op": ">", + "args": [ + "wt", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "wt", + "value": { + "op": "-", + "args": [ + "wt", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_0", + "guard": { + "op": "≤", + "args": [ + "wt", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "cr", + "value": { + "op": "min", + "args": [ + 2, + { + "op": "+", + "args": [ + "cr", + 1 + ] + } + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "action": "tack", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + }, + { + "location": "l_2", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_4" + } + ] + }, + { + "location": "l_3", + "action": "tock", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "=", + "args": [ + "cr", + 1 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "line_seized", + "value": true + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "≥", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "gave_up", + "value": true + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 1 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 2 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 2 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 3 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 2 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 3 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + } + ] + }, + { + "name": "Host_1", + "variables": [ + { + "name": "na", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 3 + }, + "initial-value": 0 + }, + { + "name": "ev", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 4 + }, + "initial-value": 2 + }, + { + "name": "wt", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 4 + }, + "initial-value": 0 + } + ], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + }, + { + "name": "l_4" + }, + { + "name": "l_5" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "tick", + "guard": { + "op": ">", + "args": [ + "wt", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "wt", + "value": { + "op": "-", + "args": [ + "wt", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_0", + "guard": { + "op": "≤", + "args": [ + "wt", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "cr", + "value": { + "op": "min", + "args": [ + 2, + { + "op": "+", + "args": [ + "cr", + 1 + ] + } + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "action": "tack", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + }, + { + "location": "l_2", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_4" + } + ] + }, + { + "location": "l_3", + "action": "tock", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "=", + "args": [ + "cr", + 1 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "line_seized", + "value": true + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "≥", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "gave_up", + "value": true + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 1 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 2 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 2 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 3 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 2 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 3 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + } + ] + }, + { + "name": "Host_2", + "variables": [ + { + "name": "na", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 3 + }, + "initial-value": 0 + }, + { + "name": "ev", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 4 + }, + "initial-value": 2 + }, + { + "name": "wt", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 4 + }, + "initial-value": 0 + } + ], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + }, + { + "name": "l_4" + }, + { + "name": "l_5" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "tick", + "guard": { + "op": ">", + "args": [ + "wt", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "wt", + "value": { + "op": "-", + "args": [ + "wt", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_0", + "guard": { + "op": "≤", + "args": [ + "wt", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "cr", + "value": { + "op": "min", + "args": [ + 2, + { + "op": "+", + "args": [ + "cr", + 1 + ] + } + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "action": "tack", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + }, + { + "location": "l_2", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_4" + } + ] + }, + { + "location": "l_3", + "action": "tock", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "=", + "args": [ + "cr", + 1 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "line_seized", + "value": true + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "≥", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "gave_up", + "value": true + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 1 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 2 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 3 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 2 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "na", + 3 + ] + }, + { + "op": "≠", + "args": [ + "cr", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + { + "op": "max", + "args": [ + 0, + { + "op": "-", + "args": [ + "ev", + 1 + ] + } + ] + }, + 3 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 0 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 1 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 2 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 4 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "na", + "value": { + "op": "+", + "args": [ + "na", + 1 + ] + } + }, + { + "ref": "wt", + "value": 3 + }, + { + "ref": "ev", + "value": { + "op": "min", + "args": [ + { + "op": "*", + "args": [ + 2, + "ev" + ] + }, + 4 + ] + } + } + ] + } + ] + } + ] + } + ], + "system": { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + "Clock", + "Host" + ], + "alphabet": [ + "tick", + "tack", + "tock" + ] + }, + "Host_1" + ], + "alphabet": [ + "tick", + "tack", + "tock" + ] + }, + "Host_2" + ], + "alphabet": [ + "tick", + "tack", + "tock" + ] + } +} \ No newline at end of file diff --git a/examples/jani-examples/beb.jani.txt b/examples/jani-examples/beb.jani.txt new file mode 100755 index 000000000..ca4a540d1 --- /dev/null +++ b/examples/jani-examples/beb.jani.txt @@ -0,0 +1,27 @@ +Peak memory usage: 38 MB +Analysis results for beb.jani + ++ State space exploration + States: 4528 + Transitions: 4874 + Branches: 6899 + Time: 0.0 s + Rate: 92408 states/s + ++ LineSeized + Probability: 0.9166259765625 + Time: 0.1 s + + + Value iteration + Final error: 0 + Iterations: 8 + Time: 0.0 s + ++ GaveUp + Probability: 0.0833740234375 + Time: 0.0 s + + + Value iteration + Final error: 0 + Iterations: 9 + Time: 0.0 s diff --git a/examples/jani-examples/beb.modest b/examples/jani-examples/beb.modest new file mode 100755 index 000000000..44f06b30e --- /dev/null +++ b/examples/jani-examples/beb.modest @@ -0,0 +1,64 @@ +// Modest MDP model of the bounded exponential backoff procedure (BEB) +// [BFHH11] +action tick, tack, tock; + +const int K = 4; // maximum value for backoff +const int N = 3; // number of tries before giving up +const int H = 3; // number of hosts (must correspond to the number of Host() instantiations in the global composition) + +int(0..2) cr; // count how many hosts attempt to seize the line in a slot (zero, one, many) +bool line_seized; +bool gave_up; + +property LineSeized = Pmax(<> line_seized); // some host managed to seize the line before any other gave up +property GaveUp = Pmax(<> gave_up); // some host gave up before any other managed to seize the line (does not work with POR) + +process Clock() +{ + tick; tack; tau {= cr = 0 =}; tock; Clock() +} + +process Host() +{ + int(0..N) na; // nr_attempts 0..N + int(0..K) ev = 2; // exp_val 0..K + int(0..K) wt; // slots_to_wait 0..K + + do + { + if(wt > 0) + { + // wait this slot + tick {= wt-- =} + } + else + { + tau {= cr = min(2, cr + 1) =}; // attempt to seize the line + tick; + if(cr == 1) + { + // someone managed to seize the line + tau {= line_seized = true =}; stop + } + else if(na >= N) + { + // maximum number of attempts exceeded + tau {= gave_up = true =}; stop + } + else + { + // backoff + tau {= na++, wt = DiscreteUniform(0, max(0, ev - 1)), ev = min(2 * ev, K) =} + } + }; + tack; tock + } +} + +par +{ +:: Clock() +:: Host() +:: Host() +:: Host() +} diff --git a/examples/jani-examples/beb.modest.txt b/examples/jani-examples/beb.modest.txt new file mode 100755 index 000000000..cbaee0f3d --- /dev/null +++ b/examples/jani-examples/beb.modest.txt @@ -0,0 +1,27 @@ +Peak memory usage: 39 MB +Analysis results for beb.modest + ++ State space exploration + States: 4528 + Transitions: 4874 + Branches: 6899 + Time: 0.0 s + Rate: 94333 states/s + ++ LineSeized + Probability: 0.9166259765625 + Time: 0.1 s + + + Value iteration + Final error: 0 + Iterations: 8 + Time: 0.0 s + ++ GaveUp + Probability: 0.0833740234375 + Time: 0.0 s + + + Value iteration + Final error: 0 + Iterations: 9 + Time: 0.0 s diff --git a/examples/jani-examples/brp.jani b/examples/jani-examples/brp.jani new file mode 100755 index 000000000..bd5d91a38 --- /dev/null +++ b/examples/jani-examples/brp.jani @@ -0,0 +1,2092 @@ +{ + "jani-version": 1, + "name": "modelName", + "type": "mdp", + "actions": [ + { + "name": "put" + }, + { + "name": "get" + }, + { + "name": "put_k" + }, + { + "name": "get_k" + }, + { + "name": "put_l" + }, + { + "name": "get_l" + }, + { + "name": "new_file" + }, + { + "name": "s_ok" + }, + { + "name": "s_dk" + }, + { + "name": "s_nok" + }, + { + "name": "s_restart" + }, + { + "name": "r_ok" + }, + { + "name": "r_inc" + }, + { + "name": "r_fst" + }, + { + "name": "r_nok" + }, + { + "name": "r_timeout" + }, + { + "name": "error" + }, + { + "name": "tick" + } + ], + "variables": [ + { + "name": "ff", + "type": "bool", + "initial-value": false + }, + { + "name": "lf", + "type": "bool", + "initial-value": false + }, + { + "name": "ab", + "type": "bool", + "initial-value": false + }, + { + "name": "i", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 16 + }, + "initial-value": 0 + }, + { + "name": "inTransitK", + "type": "bool", + "initial-value": false + }, + { + "name": "inTransitL", + "type": "bool", + "initial-value": false + }, + { + "name": "first_file_done", + "type": "bool", + "initial-value": false + }, + { + "name": "get_k_seen", + "type": "bool", + "initial-value": false + }, + { + "name": "s_ok_seen", + "type": "bool", + "initial-value": false + }, + { + "name": "s_nok_seen", + "type": "bool", + "initial-value": false + }, + { + "name": "s_dk_seen", + "type": "bool", + "initial-value": false + }, + { + "name": "s_restart_seen", + "type": "bool", + "initial-value": false + }, + { + "name": "r_ok_seen", + "type": "bool", + "initial-value": false + }, + { + "name": "r_timeout_seen", + "type": "bool", + "initial-value": false + }, + { + "name": "premature_timeout", + "type": "bool", + "initial-value": false + }, + { + "name": "channel_k_overflow", + "type": "bool", + "initial-value": false + }, + { + "name": "channel_l_overflow", + "type": "bool", + "initial-value": false + }, + { + "name": "Sender_location", + "type": "int", + "initial-value": 0 + }, + { + "name": "Receiver_location", + "type": "int", + "initial-value": 0 + }, + { + "name": "ChannelK_location", + "type": "int", + "initial-value": 0 + }, + { + "name": "ChannelL_location", + "type": "int", + "initial-value": 0 + }, + { + "name": "Observer_location", + "type": "int", + "initial-value": 0 + } + ], + "properties": [ + { + "name": "P_A", + "reach": { + "op": "∧", + "args": [ + "s_nok_seen", + "r_ok_seen" + ] + }, + "type": "probability-max-query" + }, + { + "name": "P_B", + "reach": { + "op": "∧", + "args": [ + "s_ok_seen", + { + "op": "!", + "args": [ + "r_ok_seen" + ] + } + ] + }, + "type": "probability-max-query" + }, + { + "name": "P_1", + "reach": { + "op": "∨", + "args": [ + "s_nok_seen", + "s_dk_seen" + ] + }, + "type": "probability-max-query" + }, + { + "name": "P_2", + "reach": "s_dk_seen", + "type": "probability-max-query" + }, + { + "name": "P_3", + "reach": { + "op": "∧", + "args": [ + "s_nok_seen", + { + "op": ">", + "args": [ + "i", + 8 + ] + } + ] + }, + "type": "probability-max-query" + }, + { + "name": "P_4", + "reach": { + "op": "∧", + "args": [ + { + "op": "∨", + "args": [ + { + "op": "∨", + "args": [ + "s_ok_seen", + "s_nok_seen" + ] + }, + "s_dk_seen" + ] + }, + { + "op": "!", + "args": [ + "get_k_seen" + ] + } + ] + }, + "type": "probability-max-query" + } + ], + "automata": [ + { + "name": "Sender", + "variables": [ + { + "name": "bit", + "type": "bool", + "initial-value": false + }, + { + "name": "rc", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 2 + }, + "initial-value": 0 + }, + { + "name": "c", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 16 + }, + "initial-value": 0 + } + ], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + }, + { + "name": "l_4" + }, + { + "name": "l_5" + }, + { + "name": "l_6" + }, + { + "name": "l_7" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "guard": { + "op": "<", + "args": [ + "i", + 16 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "i", + "value": { + "op": "+", + "args": [ + "i", + 1 + ] + } + }, + { + "ref": "Sender_location", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "s_ok", + "guard": { + "op": "=", + "args": [ + "i", + 16 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "first_file_done", + "value": true + }, + { + "ref": "Sender_location", + "value": 2 + }, + { + "ref": "c", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "tick", + "guard": { + "op": "∧", + "args": [ + { + "op": "≥", + "args": [ + "i", + 16 + ] + }, + { + "op": "<", + "args": [ + "c", + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "action": "put_k", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "ff", + "value": { + "op": "=", + "args": [ + "i", + 1 + ] + } + }, + { + "ref": "lf", + "value": { + "op": "=", + "args": [ + "i", + 16 + ] + } + }, + { + "ref": "ab", + "value": "bit" + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "Sender_location", + "value": 3 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + }, + { + "location": "l_2", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_4", + "assignments": [ + { + "ref": "Sender_location", + "value": 4 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "get_l", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "bit", + "value": { + "op": "!", + "args": [ + "bit" + ] + } + }, + { + "ref": "rc", + "value": 0 + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "Sender_location", + "value": 5 + } + ] + } + ] + }, + { + "location": "l_3", + "guard": { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "rc", + 2 + ] + }, + { + "op": "≥", + "args": [ + "c", + 3 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "rc", + "value": { + "op": "+", + "args": [ + "rc", + 1 + ] + } + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "Sender_location", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "s_nok", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "<", + "args": [ + "i", + 16 + ] + }, + { + "op": "≥", + "args": [ + "rc", + 2 + ] + } + ] + }, + { + "op": "≥", + "args": [ + "c", + 3 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_6", + "assignments": [ + { + "ref": "rc", + "value": 0 + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "Sender_location", + "value": 6 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "s_dk", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "≥", + "args": [ + "i", + 16 + ] + }, + { + "op": "≥", + "args": [ + "rc", + 2 + ] + } + ] + }, + { + "op": "≥", + "args": [ + "c", + 3 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_6", + "assignments": [ + { + "ref": "rc", + "value": 0 + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "Sender_location", + "value": 6 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 3 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_4" + } + ] + }, + { + "location": "l_5", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "Sender_location", + "value": 7 + } + ] + } + ] + }, + { + "location": "l_6", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_7", + "assignments": [ + { + "ref": "Sender_location", + "value": 8 + } + ] + } + ] + }, + { + "location": "l_7", + "action": "s_restart", + "guard": { + "op": "≥", + "args": [ + "c", + 15 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_4", + "assignments": [ + { + "ref": "bit", + "value": false + }, + { + "ref": "first_file_done", + "value": true + }, + { + "ref": "Sender_location", + "value": 4 + }, + { + "ref": "c", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_7", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 15 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_7", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + } + ] + }, + { + "name": "Receiver", + "variables": [ + { + "name": "r_ff", + "type": "bool", + "initial-value": false + }, + { + "name": "r_lf", + "type": "bool", + "initial-value": false + }, + { + "name": "r_ab", + "type": "bool", + "initial-value": false + }, + { + "name": "bit", + "type": "bool", + "initial-value": false + }, + { + "name": "c", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 16 + }, + "initial-value": 0 + } + ], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + }, + { + "name": "l_4" + }, + { + "name": "l_5" + }, + { + "name": "l_6" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "get_k", + "guard": "ff", + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": 0 + }, + { + "ref": "bit", + "value": "ab" + }, + { + "ref": "r_ff", + "value": "ff" + }, + { + "ref": "r_lf", + "value": "lf" + }, + { + "ref": "r_ab", + "value": "ab" + }, + { + "ref": "Receiver_location", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "get_k", + "guard": { + "op": "!", + "args": [ + "ff" + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "premature_timeout", + "value": true + }, + { + "ref": "Receiver_location", + "value": 2 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + }, + { + "location": "l_1", + "action": "put_l", + "guard": { + "op": "≠", + "args": [ + "r_ab", + "bit" + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "Receiver_location", + "value": 3 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "r_ok", + "guard": { + "op": "∧", + "args": [ + "r_lf", + { + "op": "=", + "args": [ + "r_ab", + "bit" + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_4", + "assignments": [ + { + "ref": "Receiver_location", + "value": 4 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "r_fst", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + "r_ff", + { + "op": "!", + "args": [ + "r_lf" + ] + } + ] + }, + { + "op": "=", + "args": [ + "r_ab", + "bit" + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_4", + "assignments": [ + { + "ref": "Receiver_location", + "value": 4 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "r_inc", + "guard": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "!", + "args": [ + "r_ff" + ] + }, + { + "op": "!", + "args": [ + "r_lf" + ] + } + ] + }, + { + "op": "=", + "args": [ + "r_ab", + "bit" + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_4", + "assignments": [ + { + "ref": "Receiver_location", + "value": 4 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + }, + { + "location": "l_2", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_2" + } + ] + }, + { + "location": "l_3", + "action": "get_k", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": 0 + }, + { + "ref": "r_ff", + "value": "ff" + }, + { + "ref": "r_lf", + "value": "lf" + }, + { + "ref": "r_ab", + "value": "ab" + }, + { + "ref": "Receiver_location", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "r_timeout", + "guard": { + "op": "∧", + "args": [ + "r_lf", + { + "op": "=", + "args": [ + "c", + 15 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "Receiver_location", + "value": 5 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "r_nok", + "guard": { + "op": "∧", + "args": [ + { + "op": "!", + "args": [ + "r_lf" + ] + }, + { + "op": "=", + "args": [ + "c", + 15 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_6", + "assignments": [ + { + "ref": "Receiver_location", + "value": 6 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 15 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + }, + { + "location": "l_4", + "action": "put_l", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "bit", + "value": { + "op": "!", + "args": [ + "bit" + ] + } + }, + { + "ref": "Receiver_location", + "value": 3 + } + ] + } + ] + }, + { + "location": "l_4", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 0 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_4", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + }, + { + "location": "l_5", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "r_ff", + "value": false + }, + { + "ref": "r_lf", + "value": false + }, + { + "ref": "r_ab", + "value": false + }, + { + "ref": "bit", + "value": false + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "Receiver_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_5", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 15 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + }, + { + "location": "l_6", + "action": "r_timeout", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_5", + "assignments": [ + { + "ref": "Receiver_location", + "value": 5 + } + ] + } + ] + }, + { + "location": "l_6", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 15 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_6", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 16 + ] + } + } + ] + } + ] + } + ] + }, + { + "name": "ChannelK", + "variables": [ + { + "name": "c", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 2 + }, + "initial-value": 0 + } + ], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "put_k", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 49, + 50 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": 0 + }, + { + "ref": "inTransitK", + "value": true + }, + { + "ref": "ChannelK_location", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 50 + ] + }, + "location": "l_0", + "assignments": [ + { + "ref": "ChannelK_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + }, + { + "location": "l_1", + "action": "get_k", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "inTransitK", + "value": false + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "ChannelK_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "put_k", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "channel_k_overflow", + "value": true + }, + { + "ref": "ChannelK_location", + "value": 2 + }, + { + "ref": "c", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 1 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 2 + ] + } + } + ] + } + ] + }, + { + "location": "l_2", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_2" + } + ] + } + ] + }, + { + "name": "ChannelL", + "variables": [ + { + "name": "c", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 2 + }, + "initial-value": 0 + } + ], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "put_l", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 99, + 100 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": 0 + }, + { + "ref": "inTransitL", + "value": true + }, + { + "ref": "ChannelL_location", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 100 + ] + }, + "location": "l_0", + "assignments": [ + { + "ref": "ChannelL_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + }, + { + "location": "l_1", + "action": "get_l", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "inTransitL", + "value": false + }, + { + "ref": "c", + "value": 0 + }, + { + "ref": "ChannelL_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "put_l", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "channel_l_overflow", + "value": true + }, + { + "ref": "ChannelL_location", + "value": 2 + }, + { + "ref": "c", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_1", + "action": "tick", + "guard": { + "op": "<", + "args": [ + "c", + 1 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_1", + "assignments": [ + { + "ref": "c", + "value": { + "op": "min", + "args": [ + { + "op": "+", + "args": [ + "c", + 1 + ] + }, + 2 + ] + } + } + ] + } + ] + }, + { + "location": "l_2", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_2" + } + ] + } + ] + }, + { + "name": "Observer", + "variables": [], + "locations": [ + { + "name": "l_0" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "action": "get_k", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "get_k_seen", + "value": true + }, + { + "ref": "Observer_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "s_ok", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "s_ok_seen", + "value": true + }, + { + "ref": "Observer_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "s_nok", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "s_nok_seen", + "value": true + }, + { + "ref": "Observer_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "s_dk", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "s_dk_seen", + "value": true + }, + { + "ref": "Observer_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "s_restart", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "s_restart_seen", + "value": true + }, + { + "ref": "Observer_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "r_ok", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "r_ok_seen", + "value": true + }, + { + "ref": "Observer_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "r_timeout", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0", + "assignments": [ + { + "ref": "r_timeout_seen", + "value": true + }, + { + "ref": "Observer_location", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_0", + "action": "tick", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_0" + } + ] + } + ] + } + ], + "system": { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + "Sender", + "Receiver" + ], + "alphabet": [ + "tick" + ] + }, + "ChannelK" + ], + "alphabet": [ + "put_k", + "get_k", + "tick" + ] + }, + "ChannelL" + ], + "alphabet": [ + "get_l", + "put_l", + "tick" + ] + }, + "Observer" + ], + "alphabet": [ + "s_nok", + "s_dk", + "s_ok", + "s_restart", + "get_k", + "r_ok", + "r_timeout", + "tick" + ] + } +} \ No newline at end of file diff --git a/examples/jani-examples/brp.jani.txt b/examples/jani-examples/brp.jani.txt new file mode 100755 index 000000000..9c0fcd322 --- /dev/null +++ b/examples/jani-examples/brp.jani.txt @@ -0,0 +1,63 @@ +Peak memory usage: 39 MB +Analysis results for brp.jani + ++ State space exploration + States: 3959 + Transitions: 4244 + Branches: 4593 + Time: 0.1 s + Rate: 74698 states/s + ++ P_A + Probability: 0 + Time: 0.0 s + + + Value iteration + Final error: 0 + Iterations: 1 + Time: 0.0 s + ++ P_B + Probability: 0 + Time: 0.0 s + + + Value iteration + Final error: 0 + Iterations: 1 + Time: 0.0 s + ++ P_1 + Probability: 0.000423333443357766 + Time: 0.0 s + + + Value iteration + Final error: 2.35005704803786E-07 + Iterations: 13 + Time: 0.0 s + ++ P_2 + Probability: 2.64530890961023E-05 + Time: 0.0 s + + + Value iteration + Final error: 2.05561452068843E-07 + Iterations: 14 + Time: 0.0 s + ++ P_3 + Probability: 0.000185191226393368 + Time: 0.0 s + + + Value iteration + Final error: 3.32462409056221E-07 + Iterations: 13 + Time: 0.0 s + ++ P_4 + Probability: 8E-06 + Time: 0.0 s + + + Value iteration + Final error: 0 + Iterations: 2 + Time: 0.0 s diff --git a/examples/jani-examples/brp.modest b/examples/jani-examples/brp.modest new file mode 100755 index 000000000..64743232f --- /dev/null +++ b/examples/jani-examples/brp.modest @@ -0,0 +1,213 @@ +// Modest PTA model of the bounded retransmission protocol (BRP) +// [HH09], http://www.modestchecker.net/CaseStudies/BRP/ +action put, get, put_k, get_k, put_l, get_l; +action new_file; +action s_ok, s_dk, s_nok, s_restart; +action r_ok, r_inc, r_fst, r_nok, r_timeout; +exception error; + +const int N = 16; // number of frames per file +const int MAX = 2; // maximum number of retransmissions per frame +const int TD = 1; // transmission delay +const int TS = 2 * TD + 1; // sender timeout +const int TR = 2 * MAX * TS + 3 * TD; // receiver timeout +const int SYNC = TR; + +bool ff, lf, ab; // channel data: first/last frame, alternating bit +int(0..N) i; // sender chunk counter +bool inTransitK = false; +bool inTransitL = false; + +bool first_file_done = false; +bool get_k_seen, s_ok_seen, s_nok_seen, s_dk_seen, s_restart_seen, r_ok_seen, r_timeout_seen; + +// Invariant (timed) properties (from [BrpOnTime], the TA model) +bool premature_timeout, channel_k_overflow, channel_l_overflow; +// "there is at most one message in transit for each channel" +property T_1 = A[] (!(channel_k_overflow || channel_l_overflow)); +// "there is at most one message in transit in total" +property T_2 = A[] (!(inTransitK && inTransitL)); +// Assumption (A1): "no premature timeouts" +property T_A1 = A[] (!premature_timeout); +// Assumption (A2): "sender starts new file only after receiver reacted to failure" +// Note that receiver can only notice failure if it received at least one chunk, i.e. get_k_seen +property T_A2 = A[] (!s_restart_seen || !get_k_seen || r_timeout_seen); + +// Probabilistic reachability properties (from [D'AJJL01], the RAPTURE/PRISM model) +// property A of [D'AJJL01]: "the maximum probability that eventually the sender reports +// a certain unsuccessful transmission but the receiver got the complete file" +property P_A = Pmax(<>(s_nok_seen && r_ok_seen)); +// property B of [D'AJJL01]: "the maximum probability that eventually the sender reports +// a certain successful transmission but the receiver did not get the complete file" +property P_B = Pmax(<>(s_ok_seen && !r_ok_seen)); +// property 1 of [D'AJJL01]: "the maximum probability that eventually the sender +// does not report a successful transmission" +property P_1 = Pmax(<>(s_nok_seen || s_dk_seen)); +// property 2 of [D'AJJL01]: "the maximum probability that eventually the sender +// reports an uncertainty on the success of the transmission" +property P_2 = Pmax(<>(s_dk_seen)); +// property 3 of [D'AJJL01]: "the maximum probability that eventually the sender +// reports an unsuccessful transmission after more than 8 chunks have been sent successfully" +property P_3 = Pmax(<>(s_nok_seen && i > 8)); +// property 4 of [D'AJJL01]: "the maximum probability that eventually the receiver +// does not receive any chunk and the sender tried to send a chunk" +property P_4 = Pmax(<>((s_ok_seen || s_nok_seen || s_dk_seen) && !get_k_seen)); + + +process Sender() +{ + bool bit; + int(0..MAX) rc; + clock c; + + try + { + do { + :: when urgent(i < N) {= i++ =}; + do + { + // send frame + invariant(c <= 0) put_k {= ff = (i == 1), lf = (i == N), ab = bit, c = 0 =}; + invariant(c <= TS) alt { + :: // receive ack + get_l {= bit = !bit, rc = 0, c = 0 =}; + urgent break + :: // timeout + when(c >= TS) + if(rc < MAX) + { + // retry + {= rc++, c = 0 =} + } + else if(i < N) + { + // no retries left + s_nok {= rc = 0, c = 0 =}; + urgent throw(error) + } + else + { + // no retries left + s_dk {= rc = 0, c = 0 =}; + urgent throw(error) + } + } + } + :: when(i == N) + // file transmission successfully completed + invariant(c <= 0) s_ok {= first_file_done = true =}; + urgent break + } + } + catch error + { + // File transfer did not succeed: wait, then restart with next file + invariant(c <= SYNC) when(c >= SYNC) + s_restart {= bit = false, first_file_done = true =} + } +} + +process Receiver() +{ + bool r_ff, r_lf, r_ab; + bool bit; + clock c; + + // receive first frame + if(ff) { get_k {= c = 0, bit = ab, r_ff = ff, r_lf = lf, r_ab = ab =} } + else { get_k {= c = 0, premature_timeout = true =}; stop }; + do + { + invariant(c <= 0) + { + if(r_ab != bit) + { + // repetition, re-ack + put_l + } + else + { + // report frame + if(r_lf) { r_ok } + else if(r_ff) { r_fst } + else { r_inc }; + put_l {= bit = !bit =} + } + }; + invariant(c <= TR) + { + alt { + :: // receive next frame + get_k {= c = 0, r_ff = ff, r_lf = lf, r_ab = ab =} + :: // timeout + when(c == TR) + if(r_lf) + { + // we just got the last frame, though + r_timeout; break + } + else + { + r_nok; + // abort transfer + r_timeout; break + } + } + } + }; + Receiver() +} + +process ChannelK() +{ + clock c; + + put_k palt + { + :98: {= c = 0, inTransitK = true =}; + invariant(c <= TD) alt { + :: get_k {= inTransitK = false =} + :: put_k {= channel_k_overflow = true =}; stop + } + : 2: {==} + }; + ChannelK() +} + +process ChannelL() +{ + clock c; + + put_l palt + { + :99: {= c = 0, inTransitL = true =}; + invariant(c <= TD) alt { + :: get_l {= inTransitL = false =} + :: put_l {= channel_l_overflow = true =}; stop + } + : 1: {==} + }; + ChannelL() +} + +process Observer() +{ + alt { + :: get_k {= get_k_seen = true =} + :: s_ok {= s_ok_seen = true =} + :: s_nok {= s_nok_seen = true =} + :: s_dk {= s_dk_seen = true =} + :: s_restart {= s_restart_seen = true =} + :: r_ok {= r_ok_seen = true =} + :: r_timeout {= r_timeout_seen = true =} + }; + Observer() +} + +par { +:: Sender() +:: Receiver() +:: ChannelK() +:: ChannelL() +:: Observer() +} diff --git a/examples/jani-examples/brp.modest.txt b/examples/jani-examples/brp.modest.txt new file mode 100755 index 000000000..6ec6b0c5e --- /dev/null +++ b/examples/jani-examples/brp.modest.txt @@ -0,0 +1,63 @@ +Peak memory usage: 40 MB +Analysis results for brp.modest + ++ State space exploration + States: 3959 + Transitions: 4244 + Branches: 4593 + Time: 0.1 s + Rate: 73315 states/s + ++ P_A + Probability: 0 + Time: 0.1 s + + + Value iteration + Final error: 0 + Iterations: 1 + Time: 0.0 s + ++ P_B + Probability: 0 + Time: 0.0 s + + + Value iteration + Final error: 0 + Iterations: 1 + Time: 0.0 s + ++ P_1 + Probability: 0.000423333443357766 + Time: 0.0 s + + + Value iteration + Final error: 2.35005704803786E-07 + Iterations: 13 + Time: 0.0 s + ++ P_2 + Probability: 2.64530890961023E-05 + Time: 0.0 s + + + Value iteration + Final error: 2.05561452068843E-07 + Iterations: 14 + Time: 0.0 s + ++ P_3 + Probability: 0.000185191226393368 + Time: 0.0 s + + + Value iteration + Final error: 3.32462409056221E-07 + Iterations: 13 + Time: 0.0 s + ++ P_4 + Probability: 8E-06 + Time: 0.0 s + + + Value iteration + Final error: 0 + Iterations: 2 + Time: 0.0 s diff --git a/examples/jani-examples/consensus-6.jani b/examples/jani-examples/consensus-6.jani new file mode 100755 index 000000000..58acabfef --- /dev/null +++ b/examples/jani-examples/consensus-6.jani @@ -0,0 +1,2129 @@ +{ + "jani-version": 1, + "name": "modelName", + "type": "mdp", + "actions": [ + { + "name": "done" + } + ], + "variables": [ + { + "name": "counter", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 60 + }, + "initial-value": 30 + }, + { + "name": "fin1", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "fin2", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "fin3", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "fin4", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "fin5", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "fin6", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "coin1", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "coin2", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "coin3", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "coin4", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "coin5", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + }, + { + "name": "coin6", + "type": { + "kind": "bounded", + "base": "int", + "lower-bound": 0, + "upper-bound": 1 + }, + "initial-value": 0 + } + ], + "rewards": [ + { + "name": "coin_flips" + } + ], + "properties": [ + { + "name": "C1", + "bound": 1, + "op": "≥", + "reach": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "fin1", + 1 + ] + }, + { + "op": "=", + "args": [ + "fin2", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin3", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin4", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin5", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin6", + 1 + ] + } + ] + }, + "type": "probability-comparison" + }, + { + "name": "C2", + "reach": { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "fin1", + 1 + ] + }, + { + "op": "=", + "args": [ + "fin2", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin3", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin4", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin5", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "fin6", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "coin1", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "coin2", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "coin3", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "coin4", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "coin5", + 1 + ] + } + ] + }, + { + "op": "=", + "args": [ + "coin6", + 1 + ] + } + ] + }, + "type": "probability-min-query" + } + ], + "automata": [ + { + "name": "Tourist1", + "variables": [], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin1", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin1", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin1", + 0 + ] + }, + { + "op": ">", + "args": [ + "counter", + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "-", + "args": [ + "counter", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin1", + 1 + ] + }, + { + "op": "<", + "args": [ + "counter", + 60 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "+", + "args": [ + "counter", + 1 + ] + } + }, + { + "ref": "coin1", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≤", + "args": [ + "counter", + 6 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin1", + "value": 0 + }, + { + "ref": "fin1", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≥", + "args": [ + "counter", + 54 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin1", + "value": 1 + }, + { + "ref": "fin1", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "∧", + "args": [ + { + "op": ">", + "args": [ + "counter", + 6 + ] + }, + { + "op": "<", + "args": [ + "counter", + 54 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin1", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin1", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "done", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + } + ] + }, + { + "name": "Tourist2", + "variables": [], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin2", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin2", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin2", + 0 + ] + }, + { + "op": ">", + "args": [ + "counter", + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "-", + "args": [ + "counter", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin2", + 1 + ] + }, + { + "op": "<", + "args": [ + "counter", + 60 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "+", + "args": [ + "counter", + 1 + ] + } + }, + { + "ref": "coin2", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≤", + "args": [ + "counter", + 6 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin2", + "value": 0 + }, + { + "ref": "fin2", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≥", + "args": [ + "counter", + 54 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin2", + "value": 1 + }, + { + "ref": "fin2", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "∧", + "args": [ + { + "op": ">", + "args": [ + "counter", + 6 + ] + }, + { + "op": "<", + "args": [ + "counter", + 54 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin2", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin2", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "done", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + } + ] + }, + { + "name": "Tourist3", + "variables": [], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin3", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin3", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin3", + 0 + ] + }, + { + "op": ">", + "args": [ + "counter", + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "-", + "args": [ + "counter", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin3", + 1 + ] + }, + { + "op": "<", + "args": [ + "counter", + 60 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "+", + "args": [ + "counter", + 1 + ] + } + }, + { + "ref": "coin3", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≤", + "args": [ + "counter", + 6 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin3", + "value": 0 + }, + { + "ref": "fin3", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≥", + "args": [ + "counter", + 54 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin3", + "value": 1 + }, + { + "ref": "fin3", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "∧", + "args": [ + { + "op": ">", + "args": [ + "counter", + 6 + ] + }, + { + "op": "<", + "args": [ + "counter", + 54 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin3", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin3", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "done", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + } + ] + }, + { + "name": "Tourist4", + "variables": [], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin4", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin4", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin4", + 0 + ] + }, + { + "op": ">", + "args": [ + "counter", + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "-", + "args": [ + "counter", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin4", + 1 + ] + }, + { + "op": "<", + "args": [ + "counter", + 60 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "+", + "args": [ + "counter", + 1 + ] + } + }, + { + "ref": "coin4", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≤", + "args": [ + "counter", + 6 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin4", + "value": 0 + }, + { + "ref": "fin4", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≥", + "args": [ + "counter", + 54 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin4", + "value": 1 + }, + { + "ref": "fin4", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "∧", + "args": [ + { + "op": ">", + "args": [ + "counter", + 6 + ] + }, + { + "op": "<", + "args": [ + "counter", + 54 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin4", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin4", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "done", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + } + ] + }, + { + "name": "Tourist5", + "variables": [], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin5", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin5", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin5", + 0 + ] + }, + { + "op": ">", + "args": [ + "counter", + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "-", + "args": [ + "counter", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin5", + 1 + ] + }, + { + "op": "<", + "args": [ + "counter", + 60 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "+", + "args": [ + "counter", + 1 + ] + } + }, + { + "ref": "coin5", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≤", + "args": [ + "counter", + 6 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin5", + "value": 0 + }, + { + "ref": "fin5", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≥", + "args": [ + "counter", + 54 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin5", + "value": 1 + }, + { + "ref": "fin5", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "∧", + "args": [ + { + "op": ">", + "args": [ + "counter", + 6 + ] + }, + { + "op": "<", + "args": [ + "counter", + 54 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin5", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin5", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "done", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + } + ] + }, + { + "name": "Tourist6", + "variables": [], + "locations": [ + { + "name": "l_0" + }, + { + "name": "l_1" + }, + { + "name": "l_2" + }, + { + "name": "l_3" + } + ], + "initial-location": "l_0", + "edges": [ + { + "location": "l_0", + "guard": true, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin6", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin6", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin6", + 0 + ] + }, + { + "op": ">", + "args": [ + "counter", + 0 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "-", + "args": [ + "counter", + 1 + ] + } + } + ] + } + ] + }, + { + "location": "l_1", + "guard": { + "op": "∧", + "args": [ + { + "op": "=", + "args": [ + "coin6", + 1 + ] + }, + { + "op": "<", + "args": [ + "counter", + 60 + ] + } + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_2", + "assignments": [ + { + "ref": "counter", + "value": { + "op": "+", + "args": [ + "counter", + 1 + ] + } + }, + { + "ref": "coin6", + "value": 0 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≤", + "args": [ + "counter", + 6 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin6", + "value": 0 + }, + { + "ref": "fin6", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "≥", + "args": [ + "counter", + 54 + ] + }, + "destinations": [ + { + "probability": 1, + "location": "l_3", + "assignments": [ + { + "ref": "coin6", + "value": 1 + }, + { + "ref": "fin6", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_2", + "guard": { + "op": "∧", + "args": [ + { + "op": ">", + "args": [ + "counter", + 6 + ] + }, + { + "op": "<", + "args": [ + "counter", + 54 + ] + } + ] + }, + "destinations": [ + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin6", + "value": 0 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + }, + { + "probability": { + "op": "/", + "args": [ + 1, + 2 + ] + }, + "location": "l_1", + "assignments": [ + { + "ref": "coin6", + "value": 1 + } + ], + "reward": [ + { + "ref": "coin_flips", + "value": 1 + } + ] + } + ] + }, + { + "location": "l_3", + "action": "done", + "guard": true, + "destinations": [ + { + "probability": 1, + "location": "l_3" + } + ] + } + ] + } + ], + "system": { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + { + "composition": "parallel", + "elements": [ + "Tourist1", + "Tourist2" + ], + "alphabet": [ + "done" + ] + }, + "Tourist3" + ], + "alphabet": [ + "done" + ] + }, + "Tourist4" + ], + "alphabet": [ + "done" + ] + }, + "Tourist5" + ], + "alphabet": [ + "done" + ] + }, + "Tourist6" + ], + "alphabet": [ + "done" + ] + } +} \ No newline at end of file diff --git a/examples/jani-examples/consensus-6.jani.txt b/examples/jani-examples/consensus-6.jani.txt new file mode 100755 index 000000000..17509db20 --- /dev/null +++ b/examples/jani-examples/consensus-6.jani.txt @@ -0,0 +1,27 @@ +Peak memory usage: 530 MB +Analysis results for consensus-6.jani + ++ State space exploration + States: 2345194 + Transitions: 9418584 + Branches: 13891248 + Time: 8.7 s + Rate: 270964 states/s + ++ C1 + Result: True + Time for min. prob. 0 states: 1.6 s + Time for min. prob. 1 states: 0.1 s + Time: 1.7 s + Min. probability: 1 + ++ C2 + Probability: 0.395776147642961 + Time for min. prob. 0 states: 2.0 s + Time for min. prob. 1 states: 0.1 s + Time: 125.8 s + + + Value iteration + Final error: 9.96634356860147E-07 + Iterations: 2137 + Time: 123.8 s diff --git a/examples/jani-examples/consensus-6.modest b/examples/jani-examples/consensus-6.modest new file mode 100755 index 000000000..6b129af06 --- /dev/null +++ b/examples/jani-examples/consensus-6.modest @@ -0,0 +1,157 @@ +// Modest version of http://www.prismmodelchecker.org/casestudies/consensus_prism.php +// Command line: mcsta.exe consensus-6.modest -S Memory --nochainopt --bounded-alg StateElimination -E "K=2" + +action done; + +// constants +const int N = 6; +const int K = 4; +const int range = 2 * (K + 1) * N; +const int counter_init = (K + 1) * N; +const int left = N; +const int right = 2 * (K + 1) * N - N; + +// shared coin +int(0..range) counter = counter_init; +reward coin_flips; + +property C1 = P(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1)) >= 1; +property C2 = Pmin(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1 && coin1 == 1 && coin2 == 1 && coin3 == 1 && coin4 == 1 && coin5 == 1 && coin6 == 1)); + +int(0..1) fin1, fin2, fin3, fin4, fin5, fin6; +int(0..1) coin1, coin2, coin3, coin4, coin5, coin6; + +process Tourist1() +{ + process Flip() { palt { :1: {= coin1 = 0, coin_flips++ =} :1: {= coin1 = 1, coin_flips++ =} }; Write() } + process Write() { + alt { + :: when(coin1 == 0 && counter > 0) {= counter-- =}; Check() + :: when(coin1 == 1 && counter < range) {= counter++, coin1 = 0 =}; Check() + } + } + process Check() { + alt { + :: when(counter <= left) {= coin1 = 0, fin1 = 1 =}; Finished() + :: when(counter >= right) {= coin1 = 1, fin1 = 1 =}; Finished() + :: when(counter > left && counter < right) Tourist1() + } + } + process Finished() { done; Finished() } + + Flip() +} + +process Tourist2() +{ + process Flip() { palt { :1: {= coin2 = 0, coin_flips++ =} :1: {= coin2 = 1, coin_flips++ =} }; Write() } + process Write() { + alt { + :: when(coin2 == 0 && counter > 0) {= counter-- =}; Check() + :: when(coin2 == 1 && counter < range) {= counter++, coin2 = 0 =}; Check() + } + } + process Check() { + alt { + :: when(counter <= left) {= coin2 = 0, fin2 = 1 =}; Finished() + :: when(counter >= right) {= coin2 = 1, fin2 = 1 =}; Finished() + :: when(counter > left && counter < right) Tourist2() + } + } + process Finished() { done; Finished() } + + Flip() +} + +process Tourist3() +{ + process Flip() { palt { :1: {= coin3 = 0, coin_flips++ =} :1: {= coin3 = 1, coin_flips++ =} }; Write() } + process Write() { + alt { + :: when(coin3 == 0 && counter > 0) {= counter-- =}; Check() + :: when(coin3 == 1 && counter < range) {= counter++, coin3 = 0 =}; Check() + } + } + process Check() { + alt { + :: when(counter <= left) {= coin3 = 0, fin3 = 1 =}; Finished() + :: when(counter >= right) {= coin3 = 1, fin3 = 1 =}; Finished() + :: when(counter > left && counter < right) Tourist3() + } + } + process Finished() { done; Finished() } + + Flip() +} + +process Tourist4() +{ + process Flip() { palt { :1: {= coin4 = 0, coin_flips++ =} :1: {= coin4 = 1, coin_flips++ =} }; Write() } + process Write() { + alt { + :: when(coin4 == 0 && counter > 0) {= counter-- =}; Check() + :: when(coin4 == 1 && counter < range) {= counter++, coin4 = 0 =}; Check() + } + } + process Check() { + alt { + :: when(counter <= left) {= coin4 = 0, fin4 = 1 =}; Finished() + :: when(counter >= right) {= coin4 = 1, fin4 = 1 =}; Finished() + :: when(counter > left && counter < right) Tourist4() + } + } + process Finished() { done; Finished() } + + Flip() +} + +process Tourist5() +{ + process Flip() { palt { :1: {= coin5 = 0, coin_flips++ =} :1: {= coin5 = 1, coin_flips++ =} }; Write() } + process Write() { + alt { + :: when(coin5 == 0 && counter > 0) {= counter-- =}; Check() + :: when(coin5 == 1 && counter < range) {= counter++, coin5 = 0 =}; Check() + } + } + process Check() { + alt { + :: when(counter <= left) {= coin5 = 0, fin5 = 1 =}; Finished() + :: when(counter >= right) {= coin5 = 1, fin5 = 1 =}; Finished() + :: when(counter > left && counter < right) Tourist5() + } + } + process Finished() { done; Finished() } + + Flip() +} + +process Tourist6() +{ + process Flip() { palt { :1: {= coin6 = 0, coin_flips++ =} :1: {= coin6 = 1, coin_flips++ =} }; Write() } + process Write() { + alt { + :: when(coin6 == 0 && counter > 0) {= counter-- =}; Check() + :: when(coin6 == 1 && counter < range) {= counter++, coin6 = 0 =}; Check() + } + } + process Check() { + alt { + :: when(counter <= left) {= coin6 = 0, fin6 = 1 =}; Finished() + :: when(counter >= right) {= coin6 = 1, fin6 = 1 =}; Finished() + :: when(counter > left && counter < right) Tourist6() + } + } + process Finished() { done; Finished() } + + Flip() +} + +par { +:: Tourist1() +:: Tourist2() +:: Tourist3() +:: Tourist4() +:: Tourist5() +:: Tourist6() +} diff --git a/examples/jani-examples/consensus-6.modest.txt b/examples/jani-examples/consensus-6.modest.txt new file mode 100755 index 000000000..3ff5c0821 --- /dev/null +++ b/examples/jani-examples/consensus-6.modest.txt @@ -0,0 +1,27 @@ +Peak memory usage: 531 MB +Analysis results for consensus-6.modest + ++ State space exploration + States: 2345194 + Transitions: 9418584 + Branches: 13891248 + Time: 8.2 s + Rate: 287507 states/s + ++ C1 + Result: True + Time for min. prob. 0 states: 1.5 s + Time for min. prob. 1 states: 0.2 s + Time: 1.7 s + Min. probability: 1 + ++ C2 + Probability: 0.395776147642961 + Time for min. prob. 0 states: 2.0 s + Time for min. prob. 1 states: 0.1 s + Time: 126.8 s + + + Value iteration + Final error: 9.96634356860147E-07 + Iterations: 2137 + Time: 124.7 s diff --git a/examples/jani-examples/dice.jani b/examples/jani-examples/dice.jani new file mode 100755 index 000000000..e9e377e15 --- /dev/null +++ b/examples/jani-examples/dice.jani @@ -0,0 +1,354 @@ +{ + "jani-version": 1, + "name": "dice", + "type" : "mdp", + "actions" : [], + "variables" : [ + { + "name": "thrownSix", + "type": "bool", + "initial-value": false + }, + { + "name": "terminated", + "type": "bool", + "initial-value": false + } + ], + "rewards" : [ + { + "name" : "step" + } + ], + "properties" : [ + { + "name" : "ProbThrowSix", + "reach" : "thrownSix", + "type": "probability-max-query" + }, + { + "name" : "StepsUntilReach", + "reach" : "terminated", + "reward": "step", + "type": "expected-reachability-reward-max-query" + } + ], + "automata" : [ + { + "name" : "dice", + "variables" : [ + { + "name" : "d", + "type" : { + "kind": "bounded", + "base": "int", + "lower-bound" : 0, + "upper-bound" : 6 + }, + "initial-value" : 0 + } + ], + "locations" : [ + { + "name" : "s0" + }, + { + "name" : "s1" + }, + { + "name" : "s2" + }, + { + "name" : "s3" + }, + { + "name" : "s4" + }, + { + "name" : "s5" + }, + { + "name" : "s6" + }, + { + "name" : "s7" + } + ], + "initial-location" : "s0", + "edges" : [ + { + "location" : "s0", + "guard" : true, + "destinations" : [ + { + "probability" : 0.5, + "location" : "s1", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + }, + { + "probability" : 0.5, + "location" : "s2", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + }, + { + "location" : "s1", + "guard" : true, + "destinations" : [ + { + "probability" : 0.5, + "location" : "s3", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + }, + { + "probability" : 0.5, + "location" : "s4", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + }, + { + "location" : "s2", + "guard" : true, + "destinations" : [ + { + "probability" : 0.5, + "location" : "s5", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + }, + { + "probability" : 0.5, + "location" : "s6", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + }, + { + "location" : "s3", + "guard" : true, + "destinations" : [ + { + "probability" : 0.5, + "location" : "s1", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + }, + { + "probability" : 0.5, + "location" : "s7", + "assignments" : [ + { + "ref" : "d", + "value" : 1 + }, + { + "ref" : "terminated", + "value" : true + } + ], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + }, + { + "location" : "s4", + "guard" : true, + "destinations" : [ + { + "probability" : 0.5, + "location" : "s7", + "assignments" : [ + { + "ref" : "d", + "value" : 2 + }, + { + "ref" : "terminated", + "value" : true + } + ], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + }, + { + "probability" : 0.5, + "location" : "s7", + "assignments" : [ + { + "ref" : "d", + "value" : 3 + }, + { + "ref" : "terminated", + "value" : true + } + ], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + }, + { + "location" : "s5", + "guard" : true, + "destinations" : [ + { + "probability" : 0.5, + "location" : "s7", + "assignments" : [ + { + "ref" : "d", + "value" : 4 + }, + { + "ref" : "terminated", + "value" : true + } + ], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + }, + { + "probability" : 0.5, + "location" : "s7", + "assignments" : [ + { + "ref" : "d", + "value" : 5 + }, + { + "ref" : "terminated", + "value" : true + } + ], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + }, + { + "location" : "s6", + "guard" : true, + "destinations" : [ + { + "probability" : 0.5, + "location" : "s2", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + }, + { + "probability" : 0.5, + "location" : "s7", + "assignments" : [ + { + "ref" : "d", + "value" : 6 + }, + { + "ref" : "thrownSix", + "value" : true + }, + { + "ref" : "terminated", + "value" : true + } + ], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + }, + { + "location" : "s7", + "guard" : true, + "destinations" : [ + { + "probability" : 1, + "location" : "s7", + "assignments" : [], + "rewards" : [ + { + "ref" : "step", + "value" : 1 + } + ] + } + ] + } + ] + } + ], + "system" : "dice" +} diff --git a/examples/jani-examples/dice.jani.txt b/examples/jani-examples/dice.jani.txt new file mode 100755 index 000000000..2cf07a5ed --- /dev/null +++ b/examples/jani-examples/dice.jani.txt @@ -0,0 +1,29 @@ +Peak memory usage: 36 MB +Analysis results for dice.jani + ++ State space exploration + States: 8 + Transitions: 8 + Branches: 14 + Time: 0.0 s + Rate: 190 states/s + ++ ProbThrowSix + Probability: 0.166666626930237 + Time: 0.0 s + + + Value iteration + Final error: 7.15255907834985E-07 + Iterations: 11 + Time: 0.0 s + ++ StepsUntilReach + Value: 3.66666650772095 + Time for min. prob. 0 states: 0.0 s + Time for min. prob. 1 states: 0.0 s + Time: 0.0 s + + + Value iteration + Final error: 4.08717619857464E-07 + Iterations: 12 + Time: 0.0 s