Skip to content

Commit

Permalink
interactive property builder can be used from within the model checker
Browse files Browse the repository at this point in the history
  • Loading branch information
@PimLeerkes
PimLeerkes committed Dec 15, 2024
1 parent e5b571b commit 859f5b9
Show file tree
Hide file tree
Showing 6 changed files with 248 additions and 141 deletions.
18 changes: 15 additions & 3 deletions docs/getting_started/04_mdp.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,21 @@
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"outputs": [
{
"ename": "IndentationError",
"evalue": "expected an indented block after 'else' statement on line 65 (property_builder.py, line 67)",
"output_type": "error",
"traceback": [
"Traceback \u001b[0;36m(most recent call last)\u001b[0m:\n",
"\u001b[0m File \u001b[1;32m~/repositories/stormvogel/.venv/lib/python3.12/site-packages/IPython/core/interactiveshell.py:3577\u001b[0m in \u001b[1;35mrun_code\u001b[0m\n exec(code_obj, self.user_global_ns, self.user_ns)\u001b[0m\n",
"\u001b[0;36m Cell \u001b[0;32mIn[1], line 1\u001b[0;36m\n\u001b[0;31m from stormvogel import visualization, mapping, result, show, property_builder\u001b[0;36m\n",
"\u001b[0;36m File \u001b[0;32m~/repositories/stormvogel/stormvogel/property_builder.py:67\u001b[0;36m\u001b[0m\n\u001b[0;31m else:\u001b[0m\n\u001b[0m ^\u001b[0m\n\u001b[0;31mIndentationError\u001b[0m\u001b[0;31m:\u001b[0m expected an indented block after 'else' statement on line 65\n"
]
}
],
"source": [
"from stormvogel import visualization, mapping, result, show\n",
"from stormvogel import visualization, mapping, result, show, property_builder\n",
"import stormpy"
]
},
Expand Down Expand Up @@ -2531,7 +2543,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.6"
"version": "3.12.7"
}
},
"nbformat": 4,
Expand Down
188 changes: 156 additions & 32 deletions docs/getting_started/model.html
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

<iframe
id="modelZVKCIZVJVv"
id="modeltDCjMpduxa"
width="820"
height="620"
frameborder="0"
Expand All @@ -27,37 +27,161 @@
&lt;div id=&quot;mynetwork&quot;&gt;&lt;/div&gt;
&lt;script type=&quot;text/javascript&quot;&gt;
var nodes = new vis.DataSet([{ id: 0, label: `nijmegen`, group: &quot;states&quot; },
{ id: 1, label: `eindhoven`, group: &quot;states&quot; },
{ id: 2, label: `aachen`, group: &quot;states&quot; },
{ id: 3, label: `saw nijmegen
ʘ 3`, group: &quot;states&quot; },
{ id: 4, label: `saw eindhoven
ʘ 4`, group: &quot;states&quot; },
{ id: 5, label: `saw aachen
ʘ 5`, group: &quot;states&quot; },
{ id: 10000000000, label: `walk`, group: &quot;actions&quot; },
{ id: 10000000001, label: `stay put`, group: &quot;actions&quot; },
{ id: 10000000002, label: `walk`, group: &quot;actions&quot; },
{ id: 10000000003, label: `stay put`, group: &quot;actions&quot; },
{ id: 10000000004, label: `walk`, group: &quot;actions&quot; },
{ id: 10000000005, label: `stay put`, group: &quot;actions&quot; },
var nodes = new vis.DataSet([{ id: 0, label: `init
€ rounds: 0.0`, group: &quot;states&quot; },
{ id: 1, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 2, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 3, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 4, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 5, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 6, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 7, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 8, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 9, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 10, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 11, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 12, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 13, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 14, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 15, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 16, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 17, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 18, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 19, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 20, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 21, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 22, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 23, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 24, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 25, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 26, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 27, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 28, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 29, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 30, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 31, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 32, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 33, label: `
€ rounds: 1.0`, group: &quot;states&quot;, hidden: true },
{ id: 34, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 35, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 36, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 37, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 38, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 39, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 40, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 41, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 42, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 43, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 44, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 45, label: `
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 46, label: `deadlock
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 47, label: `deadlock
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
{ id: 48, label: `deadlock
€ rounds: 0.0`, group: &quot;states&quot;, hidden: true },
]);
var edges = new vis.DataSet([{ from: 0, to: 10000000000 },
{ from: 10000000000, to: 3, label: &quot;1&quot; },
{ from: 0, to: 10000000001 },
{ from: 10000000001, to: 0, label: &quot;1&quot; },
{ from: 3, to: 0, label: &quot;1&quot; },
{ from: 1, to: 10000000002 },
{ from: 10000000002, to: 4, label: &quot;1&quot; },
{ from: 1, to: 10000000003 },
{ from: 10000000003, to: 1, label: &quot;1&quot; },
{ from: 4, to: 1, label: &quot;1&quot; },
{ from: 2, to: 10000000004 },
{ from: 10000000004, to: 5, label: &quot;1&quot; },
{ from: 2, to: 10000000005 },
{ from: 10000000005, to: 2, label: &quot;1&quot; },
{ from: 5, to: 2, label: &quot;1&quot; },
var edges = new vis.DataSet([{ from: 0, to: 1, label: &quot;1/8&quot; },
{ from: 0, to: 2, label: &quot;1/8&quot; },
{ from: 0, to: 3, label: &quot;1/8&quot; },
{ from: 0, to: 4, label: &quot;1/8&quot; },
{ from: 0, to: 5, label: &quot;1/8&quot; },
{ from: 0, to: 6, label: &quot;1/8&quot; },
{ from: 0, to: 7, label: &quot;1/8&quot; },
{ from: 0, to: 8, label: &quot;1/8&quot; },
{ from: 1, to: 9, label: &quot;1&quot; },
{ from: 2, to: 10, label: &quot;1&quot; },
{ from: 3, to: 11, label: &quot;1&quot; },
{ from: 4, to: 12, label: &quot;1&quot; },
{ from: 5, to: 13, label: &quot;1&quot; },
{ from: 6, to: 14, label: &quot;1&quot; },
{ from: 7, to: 15, label: &quot;1&quot; },
{ from: 8, to: 16, label: &quot;1&quot; },
{ from: 9, to: 17, label: &quot;1&quot; },
{ from: 10, to: 18, label: &quot;1&quot; },
{ from: 11, to: 19, label: &quot;1&quot; },
{ from: 12, to: 20, label: &quot;1&quot; },
{ from: 13, to: 21, label: &quot;1&quot; },
{ from: 14, to: 22, label: &quot;1&quot; },
{ from: 15, to: 23, label: &quot;1&quot; },
{ from: 16, to: 24, label: &quot;1&quot; },
{ from: 17, to: 25, label: &quot;1&quot; },
{ from: 18, to: 26, label: &quot;1&quot; },
{ from: 19, to: 27, label: &quot;1&quot; },
{ from: 20, to: 26, label: &quot;1&quot; },
{ from: 21, to: 28, label: &quot;1&quot; },
{ from: 22, to: 29, label: &quot;1&quot; },
{ from: 23, to: 30, label: &quot;1&quot; },
{ from: 24, to: 31, label: &quot;1&quot; },
{ from: 25, to: 32, label: &quot;1&quot; },
{ from: 26, to: 33, label: &quot;1&quot; },
{ from: 27, to: 34, label: &quot;1&quot; },
{ from: 28, to: 35, label: &quot;1&quot; },
{ from: 29, to: 36, label: &quot;1&quot; },
{ from: 30, to: 37, label: &quot;1&quot; },
{ from: 31, to: 38, label: &quot;1&quot; },
{ from: 32, to: 39, label: &quot;1&quot; },
{ from: 33, to: 40, label: &quot;1&quot; },
{ from: 34, to: 41, label: &quot;1&quot; },
{ from: 35, to: 42, label: &quot;1&quot; },
{ from: 36, to: 43, label: &quot;1&quot; },
{ from: 37, to: 44, label: &quot;1&quot; },
{ from: 38, to: 45, label: &quot;1&quot; },
{ from: 39, to: 0, label: &quot;1&quot; },
{ from: 40, to: 46, label: &quot;1&quot; },
{ from: 41, to: 47, label: &quot;1&quot; },
{ from: 42, to: 48, label: &quot;1&quot; },
{ from: 43, to: 48, label: &quot;1&quot; },
{ from: 44, to: 47, label: &quot;1&quot; },
{ from: 45, to: 0, label: &quot;1&quot; },
{ from: 46, to: 46, label: &quot;1&quot; },
{ from: 47, to: 47, label: &quot;1&quot; },
{ from: 48, to: 48, label: &quot;1&quot; },
]);
var options = {
&quot;__fake_macros&quot;: {
Expand Down Expand Up @@ -164,7 +288,7 @@
&quot;enable_physics&quot;: true,
&quot;width&quot;: 800,
&quot;height&quot;: 600,
&quot;explore&quot;: false
&quot;explore&quot;: true
},
&quot;saving&quot;: {
&quot;relative_path&quot;: true,
Expand Down
9 changes: 9 additions & 0 deletions stormvogel/model.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -845,6 +845,15 @@ def remove_transitions_between_states(
"This method only works for models that don't support actions."
)

def get_all_state_labels(self):
"""returns the set of all state labels of the model"""
labels = set()
for state in self.states.values():
for label in state.labels:
if label not in labels:
labels.add(label)
return labels

def get_action(self, name: str) -> Action:
"""Gets an existing action."""
if not self.supports_actions():
Expand Down
53 changes: 14 additions & 39 deletions stormvogel/model_checking.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,21 +2,30 @@
import stormvogel.mapping
import stormvogel.result
import stormvogel.model
import stormvogel.property_builder
import examples.monty_hall


def model_checking(
model: stormvogel.model.Model, prop: str, scheduler: bool = True
model: stormvogel.model.Model, prop: str | None = None, scheduler: bool = True
) -> stormvogel.result.Result | None:
"""
Instead of calling this function, the stormpy model checker can be used by first mapping a model to a stormpy model,
then calling the stormpy model checker with it followed by converting the model checker result to a stormvogel result.
This function just performs this procedure automatically.
"""

prop = stormpy.parse_properties(prop)
if prop:
prop = stormpy.parse_properties(prop)
else:
interactive_prop = (
stormvogel.property_builder.build_property_string_interactive(model)
)
prop = stormpy.parse_properties(interactive_prop)

stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(model)

assert prop is not None
if model.supports_actions() and scheduler:
stormpy_result = stormpy.model_checking(
stormpy_model, prop[0], extract_scheduler=True
Expand All @@ -37,41 +46,7 @@ def model_checking(
return stormvogel_result


class PropertyBuilder:
"""
Aimed to let beginner users build property strings
Args:
model: the model that the property string will be used for
"""

model: stormvogel.model.Model
prop: str

def __init__(self, model: stormvogel.model.Model):
self.model = model
self.prop = ""

def get_reachabilty_probability(self, label: str, value: str = "default") -> str:
"""To create a property that asks for the reachability probabilities of the states"""

print(value)

assert len(self.model.get_states_with_label(label)) > 0
if __name__ == "__main__":
mdp = examples.monty_hall.create_monty_hall_mdp()

if value == "default":
string = f'P=? [F "{label}"]'
self.prop = string
return string
elif value == "max":
string = f'Pmax=? [F "{label}"]'
self.prop = string
return string
elif value == "min":
string = f'Pmin=? [F "{label}"]'
self.prop = string
return string
else:
raise RuntimeError(
"Please choose as value either 'max', 'min' or 'default'."
)
print(model_checking(mdp))
Loading

0 comments on commit 859f5b9

Please sign in to comment.