From a86e3a708da0274a9514e927730e5686cb86a84b Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sat, 21 Sep 2024 11:08:40 +0200 Subject: [PATCH 01/13] created model_checking function --- docs/getting_started/mdp.ipynb | 129 +++++++++++++++++++++++---------- stormvogel/model_checking.py | 42 +++++++++++ 2 files changed, 133 insertions(+), 38 deletions(-) create mode 100644 stormvogel/model_checking.py diff --git a/docs/getting_started/mdp.ipynb b/docs/getting_started/mdp.ipynb index 1532656..c7c3ec9 100644 --- a/docs/getting_started/mdp.ipynb +++ b/docs/getting_started/mdp.ipynb @@ -2,26 +2,26 @@ "cells": [ { "cell_type": "code", - "execution_count": 14, + "execution_count": 1, "metadata": {}, "outputs": [], "source": [ - "from stormvogel import visualization, mapping, result, show\n", + "from stormvogel import visualization, mapping, result, show, model_checking\n", "import stormpy" ] }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 2, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "" + "" ] }, - "execution_count": 15, + "execution_count": 2, "metadata": {}, "output_type": "execute_result" } @@ -125,7 +125,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 3, "metadata": {}, "outputs": [], "source": [ @@ -135,7 +135,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 4, "metadata": {}, "outputs": [ { @@ -167,16 +167,28 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 16, "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "['__class__', '__delattr__', '__dir__', '__doc__', '__eq__', '__format__', '__ge__', '__getattribute__', '__getstate__', '__gt__', '__hash__', '__init__', '__init_subclass__', '__le__', '__lt__', '__module__', '__ne__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__sizeof__', '__str__', '__subclasshook__', 'name', 'raw_formula']\n", + "R[exp]max=? [F \"elected\"]\n" + ] + } + ], "source": [ - "prop = stormpy.parse_properties(\"Rmax=? [F \\\"elected\\\"]\", leader)" + "prop = stormpy.parse_properties(\"Rmax=? [F \\\"elected\\\"]\", leader)\n", + "\n", + "print(dir(prop[0]))\n", + "print(prop[0].raw_formula)" ] }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 6, "metadata": {}, "outputs": [], "source": [ @@ -185,7 +197,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -202,7 +214,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -232,7 +244,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -254,39 +266,40 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 10, "metadata": { "scrolled": true }, - "outputs": [], + "outputs": [ + { + "ename": "TypeError", + "evalue": "parse_properties_without_context(): incompatible function arguments. The following argument types are supported:\n 1. (formula_string: str, property_filter: Optional[Set[str]] = None) -> List[stormpy.core.Property]\n\nInvoked with: []", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mTypeError\u001b[0m Traceback (most recent call last)", + "Cell \u001b[0;32mIn[10], line 4\u001b[0m\n\u001b[1;32m 1\u001b[0m stormvogel_model \u001b[38;5;241m=\u001b[39m mapping\u001b[38;5;241m.\u001b[39mstormpy_to_stormvogel(leader_model)\n\u001b[1;32m 3\u001b[0m \u001b[38;5;66;03m#a stormvogel result can also be obtained directly:\u001b[39;00m\n\u001b[0;32m----> 4\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m \u001b[43mmodel_checking\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mmodel_checking\u001b[49m\u001b[43m(\u001b[49m\u001b[43mstormvogel_model\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mprop\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43;01mTrue\u001b[39;49;00m\u001b[43m)\u001b[49m\n\u001b[1;32m 6\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m result\u001b[38;5;241m.\u001b[39mconvert_model_checking_result(stormvogel_model, stormpy_result)\n", + "File \u001b[0;32m~/repositories/stormvogel/.venv/lib/python3.12/site-packages/stormvogel/model_checking.py:18\u001b[0m, in \u001b[0;36mmodel_checking\u001b[0;34m(model, prop, scheduler)\u001b[0m\n\u001b[1;32m 9\u001b[0m \u001b[38;5;250m\u001b[39m\u001b[38;5;124;03m\"\"\"\u001b[39;00m\n\u001b[1;32m 10\u001b[0m \u001b[38;5;124;03mFunction to provide a model checking functionality in stormvogel that uses the stormpy model checker behind the scenes.\u001b[39;00m\n\u001b[1;32m 11\u001b[0m \u001b[38;5;124;03mTakes a stormvogel model and a property string as input. Additionally it can be specified wheter the result should contain a scheduler or not.\u001b[39;00m\n\u001b[0;32m (...)\u001b[0m\n\u001b[1;32m 14\u001b[0m \u001b[38;5;124;03mfollowed by converting the model checker result to a stormvogel result. This function just performs this procedure automatically.\u001b[39;00m\n\u001b[1;32m 15\u001b[0m \u001b[38;5;124;03m\"\"\"\u001b[39;00m\n\u001b[1;32m 17\u001b[0m stormpy_model \u001b[38;5;241m=\u001b[39m stormvogel\u001b[38;5;241m.\u001b[39mmapping\u001b[38;5;241m.\u001b[39mstormvogel_to_stormpy(model)\n\u001b[0;32m---> 18\u001b[0m parsed_prop \u001b[38;5;241m=\u001b[39m \u001b[43mstormpy\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mparse_properties_without_context\u001b[49m\u001b[43m(\u001b[49m\u001b[43mprop\u001b[49m\u001b[43m)\u001b[49m \n\u001b[1;32m 19\u001b[0m stormpy_result \u001b[38;5;241m=\u001b[39m stormpy\u001b[38;5;241m.\u001b[39mmodel_checking(stormpy_model, parsed_prop, extract_scheduler\u001b[38;5;241m=\u001b[39mscheduler)\n\u001b[1;32m 20\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m stormvogel\u001b[38;5;241m.\u001b[39mresult\u001b[38;5;241m.\u001b[39mconvert_model_checking_result(stormvogel_model, stormpy_result)\n", + "\u001b[0;31mTypeError\u001b[0m: parse_properties_without_context(): incompatible function arguments. The following argument types are supported:\n 1. (formula_string: str, property_filter: Optional[Set[str]] = None) -> List[stormpy.core.Property]\n\nInvoked with: []" + ] + } + ], "source": [ "stormvogel_model = mapping.stormpy_to_stormvogel(leader_model)\n", "\n", + "#a stormvogel result can also be obtained directly:\n", + "#stormvogel_result = model_checking.model_checking(stormvogel_model, prop[0], True)\n", + "\n", "stormvogel_result = result.convert_model_checking_result(stormvogel_model, stormpy_result)" ] }, { "cell_type": "code", - "execution_count": 24, + "execution_count": null, "metadata": { "scrolled": true }, - "outputs": [ - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "bccaeb3962e24a84a838417dd4210d04", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "Output(outputs=({'output_type': 'display_data', 'data': {'text/plain': '', '\u2026" - ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], + "outputs": [], "source": [ "import stormvogel.layout\n", "\n", @@ -295,9 +308,21 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 11, "metadata": {}, - "outputs": [], + "outputs": [ + { + "ename": "NameError", + "evalue": "name 'stormvogel_result' is not defined", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mNameError\u001b[0m Traceback (most recent call last)", + "Cell \u001b[0;32mIn[11], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m induced_dtmc \u001b[38;5;241m=\u001b[39m \u001b[43mstormvogel_result\u001b[49m\u001b[38;5;241m.\u001b[39mgenerate_induced_dtmc()\n", + "\u001b[0;31mNameError\u001b[0m: name 'stormvogel_result' is not defined" + ] + } + ], "source": [ "induced_dtmc = stormvogel_result.generate_induced_dtmc()" ] @@ -310,12 +335,26 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "bccaeb3962e24a84a838417dd4210d04", + "model_id": "a44b9b958747405b84ab6467441ca86a", "version_major": 2, "version_minor": 0 }, "text/plain": [ - "Output(outputs=({'output_type': 'display_data', 'data': {'text/plain': '', '\u2026" + "Output()" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "ec5f0ce2baf24964b07078b37cf7e46f", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(), Output()))" ] }, "metadata": {}, @@ -340,6 +379,20 @@ "outputs": [], "source": [] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null, @@ -364,7 +417,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.4" + "version": "3.12.5" } }, "nbformat": 4, diff --git a/stormvogel/model_checking.py b/stormvogel/model_checking.py new file mode 100644 index 0000000..5d8cadd --- /dev/null +++ b/stormvogel/model_checking.py @@ -0,0 +1,42 @@ +import stormpy +import stormvogel.mapping +import stormvogel.result +import stormvogel.model + + +def model_checking( + model: stormvogel.model.Model, prop: str | stormpy.Property, scheduler: bool = False +) -> 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. + """ + + # TODO parse properties + + stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(model) + # parsed_prop = stormpy.parse_properties_without_context(prop) + stormpy_result = stormpy.model_checking( + stormpy_model, prop, extract_scheduler=scheduler + ) + assert stormvogel_model is not None + stormvogel_result = stormvogel.result.convert_model_checking_result( + stormvogel_model, stormpy_result + ) + + return stormvogel_result + + +if __name__ == "__main__": + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + formula_str = "P=? [F s=7 & d=2]" + properties = stormpy.parse_properties(formula_str, prism_program) + model = stormpy.build_model(prism_program, properties) + + stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(model) + + assert stormvogel_model is not None + stormvogel_results = model_checking(stormvogel_model, properties[0]) + print(stormvogel_results) From d8f5b608e70b1d6c316b078d2c0dc75b1f4b93d7 Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sat, 21 Sep 2024 11:36:05 +0200 Subject: [PATCH 02/13] now both strings and stormpy properties can be used --- stormvogel/model_checking.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/stormvogel/model_checking.py b/stormvogel/model_checking.py index 5d8cadd..b30321f 100644 --- a/stormvogel/model_checking.py +++ b/stormvogel/model_checking.py @@ -13,10 +13,11 @@ def model_checking( This function just performs this procedure automatically. """ - # TODO parse properties + # We can choose between provoding properties as a string or as a stormpy.Property object + if isinstance(prop, str): + prop = stormpy.parse_properties_without_context(prop) # TODO make this work stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(model) - # parsed_prop = stormpy.parse_properties_without_context(prop) stormpy_result = stormpy.model_checking( stormpy_model, prop, extract_scheduler=scheduler ) @@ -40,3 +41,6 @@ def model_checking( assert stormvogel_model is not None stormvogel_results = model_checking(stormvogel_model, properties[0]) print(stormvogel_results) + + # stormvogel_results = model_checking(stormvogel_model, formula_str) + # print(stormvogel_results) From 9fb70c0ccd622294a2ad17f4f5971cd4a952cc8c Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sun, 8 Dec 2024 15:08:17 +0100 Subject: [PATCH 03/13] parsing properties works --- stormvogel/model_checking.py | 31 ++++++++++++------------------- 1 file changed, 12 insertions(+), 19 deletions(-) diff --git a/stormvogel/model_checking.py b/stormvogel/model_checking.py index b30321f..a6974a1 100644 --- a/stormvogel/model_checking.py +++ b/stormvogel/model_checking.py @@ -5,7 +5,7 @@ def model_checking( - model: stormvogel.model.Model, prop: str | stormpy.Property, scheduler: bool = False + model: stormvogel.model.Model, prop: str, scheduler: bool = False ) -> 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, @@ -13,34 +13,27 @@ def model_checking( This function just performs this procedure automatically. """ - # We can choose between provoding properties as a string or as a stormpy.Property object - if isinstance(prop, str): - prop = stormpy.parse_properties_without_context(prop) # TODO make this work + prop = stormpy.parse_properties(prop) stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(model) stormpy_result = stormpy.model_checking( - stormpy_model, prop, extract_scheduler=scheduler + stormpy_model, prop[0], extract_scheduler=scheduler ) - assert stormvogel_model is not None + assert model is not None stormvogel_result = stormvogel.result.convert_model_checking_result( - stormvogel_model, stormpy_result + model, stormpy_result ) return stormvogel_result if __name__ == "__main__": - path = stormpy.examples.files.prism_dtmc_die - prism_program = stormpy.parse_prism_program(path) - formula_str = "P=? [F s=7 & d=2]" - properties = stormpy.parse_properties(formula_str, prism_program) - model = stormpy.build_model(prism_program, properties) - - stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(model) + dtmc = stormvogel.model.new_dtmc("Die") + init = dtmc.get_initial_state() + init.set_transitions( + [(1 / 6, dtmc.new_state(f"rolled{i}", {"rolled": i})) for i in range(6)] + ) + dtmc.add_self_loops() - assert stormvogel_model is not None - stormvogel_results = model_checking(stormvogel_model, properties[0]) + stormvogel_results = model_checking(dtmc, 'Pmin=? [F "rolled1"]') print(stormvogel_results) - - # stormvogel_results = model_checking(stormvogel_model, formula_str) - # print(stormvogel_results) From 2bb6c35d0e28d63d76c6304e23a811144155e5e6 Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sat, 14 Dec 2024 14:37:30 +0100 Subject: [PATCH 04/13] works with schedulers + created first test --- stormvogel/model_checking.py | 19 +++++++----------- stormvogel/result.py | 38 +++++++++++++++++------------------- tests/test_model_checking.py | 29 +++++++++++++++++++++++++++ 3 files changed, 54 insertions(+), 32 deletions(-) create mode 100644 tests/test_model_checking.py diff --git a/stormvogel/model_checking.py b/stormvogel/model_checking.py index a6974a1..f73cbc9 100644 --- a/stormvogel/model_checking.py +++ b/stormvogel/model_checking.py @@ -20,20 +20,15 @@ def model_checking( stormpy_model, prop[0], extract_scheduler=scheduler ) assert model is not None - stormvogel_result = stormvogel.result.convert_model_checking_result( - model, stormpy_result - ) - return stormvogel_result + # to get the correct action labels, we need to convert the model back to stormvogel instead of + # using the initial one for now. (otherwise schedulers won't work) + stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(stormpy_model) + assert stormvogel_model is not None -if __name__ == "__main__": - dtmc = stormvogel.model.new_dtmc("Die") - init = dtmc.get_initial_state() - init.set_transitions( - [(1 / 6, dtmc.new_state(f"rolled{i}", {"rolled": i})) for i in range(6)] + stormvogel_result = stormvogel.result.convert_model_checking_result( + stormvogel_model, stormpy_result ) - dtmc.add_self_loops() - stormvogel_results = model_checking(dtmc, 'Pmin=? [F "rolled1"]') - print(stormvogel_results) + return stormvogel_result diff --git a/stormvogel/result.py b/stormvogel/result.py index 04de6be..1658f3e 100644 --- a/stormvogel/result.py +++ b/stormvogel/result.py @@ -42,6 +42,11 @@ def __str__(self) -> str: add = "" return add + "taken actions: " + str(self.taken_actions) + def __eq__(self, other) -> bool: + if isinstance(other, Scheduler): + return self.taken_actions == other.taken_actions + return False + class Result: """Result object represents the model checking results for a given model @@ -110,15 +115,22 @@ def generate_induced_dtmc(self) -> stormvogel.model.Model | None: raise RuntimeError("This result does not have a scheduler") def __str__(self) -> str: - s = {} - if self.scheduler is not None: - for index, action in enumerate(self.scheduler.taken_actions.values()): - s[index] = str(list(action.labels)) - add = "" if self.model.name is not None: add = "model: " + str(self.model.name) + "\n" - return add + "values: \n " + str(self.values) + "\n" + "scheduler: \n " + str(s) + return ( + add + + "values: \n " + + str(self.values) + + "\n" + + "scheduler: \n " + + str(self.scheduler) + ) + + def __eq__(self, other) -> bool: + if isinstance(other, Result): + return self.values == other.values and self.scheduler == other.scheduler + return False def convert_model_checking_result( @@ -148,17 +160,3 @@ def convert_model_checking_result( stormvogel_result.add_scheduler(stormpy_result.scheduler) return stormvogel_result - - -if __name__ == "__main__": - path = stormpy.examples.files.prism_dtmc_die - prism_program = stormpy.parse_prism_program(path) - formula_str = "P=? [F s=7 & d=2]" - properties = stormpy.parse_properties(formula_str, prism_program) - - model = stormpy.build_model(prism_program, properties) - result = stormpy.model_checking(model, properties[0]) - print(type(result)) - stormvogel_model = stormvogel.map.stormpy_to_stormvogel(model) - if stormvogel_model is not None: - convert_model_checking_result(stormvogel_model, result) diff --git a/tests/test_model_checking.py b/tests/test_model_checking.py new file mode 100644 index 0000000..8654616 --- /dev/null +++ b/tests/test_model_checking.py @@ -0,0 +1,29 @@ +import stormvogel.model_checking +import examples.monty_hall +import stormpy + + +def test_mdp_model_checking(): + # we get our result using the stormvogel model checker function indirectly + mdp = examples.monty_hall.create_monty_hall_mdp() + prop = 'Pmin=? [F "done"]' + result = stormvogel.model_checking.model_checking(mdp, prop, True) + + # and directly + prop = stormpy.parse_properties(prop) + + stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(mdp) + stormpy_result = stormpy.model_checking( + stormpy_model, prop[0], extract_scheduler=True + ) + assert mdp is not None + + # to get the correct action labels, we need to convert the model back to stormvogel instead of + # using the initial one for now. (otherwise schedulers won't work) + stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(stormpy_model) + + stormvogel_result = stormvogel.result.convert_model_checking_result( + stormvogel_model, stormpy_result + ) + + assert result == stormvogel_result From 8d0c93dd539afb0b2738c7e88e7dd8126076d6b8 Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sat, 14 Dec 2024 14:56:12 +0100 Subject: [PATCH 05/13] small changes and added one more test --- stormvogel/model_checking.py | 13 ++++++++----- tests/test_model_checking.py | 24 ++++++++++++++++++++---- 2 files changed, 28 insertions(+), 9 deletions(-) diff --git a/stormvogel/model_checking.py b/stormvogel/model_checking.py index f73cbc9..94abbe4 100644 --- a/stormvogel/model_checking.py +++ b/stormvogel/model_checking.py @@ -5,7 +5,7 @@ def model_checking( - model: stormvogel.model.Model, prop: str, scheduler: bool = False + model: stormvogel.model.Model, prop: str, 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, @@ -16,10 +16,13 @@ def model_checking( prop = stormpy.parse_properties(prop) stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(model) - stormpy_result = stormpy.model_checking( - stormpy_model, prop[0], extract_scheduler=scheduler - ) - assert model is not None + + if model.supports_actions() and scheduler: + stormpy_result = stormpy.model_checking( + stormpy_model, prop[0], extract_scheduler=True + ) + else: + stormpy_result = stormpy.model_checking(stormpy_model, prop[0]) # to get the correct action labels, we need to convert the model back to stormvogel instead of # using the initial one for now. (otherwise schedulers won't work) diff --git a/tests/test_model_checking.py b/tests/test_model_checking.py index 8654616..c2a58d8 100644 --- a/tests/test_model_checking.py +++ b/tests/test_model_checking.py @@ -1,9 +1,12 @@ import stormvogel.model_checking import examples.monty_hall +import examples.die import stormpy -def test_mdp_model_checking(): +def test_model_checking(): + # TODO this test is maybe too trivial? + # we get our result using the stormvogel model checker function indirectly mdp = examples.monty_hall.create_monty_hall_mdp() prop = 'Pmin=? [F "done"]' @@ -16,10 +19,23 @@ def test_mdp_model_checking(): stormpy_result = stormpy.model_checking( stormpy_model, prop[0], extract_scheduler=True ) - assert mdp is not None - # to get the correct action labels, we need to convert the model back to stormvogel instead of - # using the initial one for now. (otherwise schedulers won't work) + stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(stormpy_model) + + stormvogel_result = stormvogel.result.convert_model_checking_result( + stormvogel_model, stormpy_result + ) + + # now we do it for a dtmc: + dtmc = examples.die.create_die_dtmc() + prop = 'Pmin=? [F "rolled1"]' + result = stormvogel.model_checking.model_checking(dtmc, prop, True) + + # indirectly: + prop = stormpy.parse_properties(prop) + stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(dtmc) + stormpy_result = stormpy.model_checking(stormpy_model, prop[0]) + stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(stormpy_model) stormvogel_result = stormvogel.result.convert_model_checking_result( From 4412aa5831d2a99a7bfee2a168c973f122b39bde Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sat, 14 Dec 2024 15:06:53 +0100 Subject: [PATCH 06/13] remove unnecessary notebook cell --- docs/getting_started/mdp.ipynb | 138 +++++++++++++++------------------ 1 file changed, 61 insertions(+), 77 deletions(-) diff --git a/docs/getting_started/mdp.ipynb b/docs/getting_started/mdp.ipynb index c7c3ec9..0690df0 100644 --- a/docs/getting_started/mdp.ipynb +++ b/docs/getting_started/mdp.ipynb @@ -18,7 +18,7 @@ { "data": { "text/plain": [ - "" + "" ] }, "execution_count": 2, @@ -167,7 +167,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -266,40 +266,64 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 15, "metadata": { "scrolled": true }, "outputs": [ { - "ename": "TypeError", - "evalue": "parse_properties_without_context(): incompatible function arguments. The following argument types are supported:\n 1. (formula_string: str, property_filter: Optional[Set[str]] = None) -> List[stormpy.core.Property]\n\nInvoked with: []", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mTypeError\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[10], line 4\u001b[0m\n\u001b[1;32m 1\u001b[0m stormvogel_model \u001b[38;5;241m=\u001b[39m mapping\u001b[38;5;241m.\u001b[39mstormpy_to_stormvogel(leader_model)\n\u001b[1;32m 3\u001b[0m \u001b[38;5;66;03m#a stormvogel result can also be obtained directly:\u001b[39;00m\n\u001b[0;32m----> 4\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m \u001b[43mmodel_checking\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mmodel_checking\u001b[49m\u001b[43m(\u001b[49m\u001b[43mstormvogel_model\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mprop\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43;01mTrue\u001b[39;49;00m\u001b[43m)\u001b[49m\n\u001b[1;32m 6\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m result\u001b[38;5;241m.\u001b[39mconvert_model_checking_result(stormvogel_model, stormpy_result)\n", - "File \u001b[0;32m~/repositories/stormvogel/.venv/lib/python3.12/site-packages/stormvogel/model_checking.py:18\u001b[0m, in \u001b[0;36mmodel_checking\u001b[0;34m(model, prop, scheduler)\u001b[0m\n\u001b[1;32m 9\u001b[0m \u001b[38;5;250m\u001b[39m\u001b[38;5;124;03m\"\"\"\u001b[39;00m\n\u001b[1;32m 10\u001b[0m \u001b[38;5;124;03mFunction to provide a model checking functionality in stormvogel that uses the stormpy model checker behind the scenes.\u001b[39;00m\n\u001b[1;32m 11\u001b[0m \u001b[38;5;124;03mTakes a stormvogel model and a property string as input. Additionally it can be specified wheter the result should contain a scheduler or not.\u001b[39;00m\n\u001b[0;32m (...)\u001b[0m\n\u001b[1;32m 14\u001b[0m \u001b[38;5;124;03mfollowed by converting the model checker result to a stormvogel result. This function just performs this procedure automatically.\u001b[39;00m\n\u001b[1;32m 15\u001b[0m \u001b[38;5;124;03m\"\"\"\u001b[39;00m\n\u001b[1;32m 17\u001b[0m stormpy_model \u001b[38;5;241m=\u001b[39m stormvogel\u001b[38;5;241m.\u001b[39mmapping\u001b[38;5;241m.\u001b[39mstormvogel_to_stormpy(model)\n\u001b[0;32m---> 18\u001b[0m parsed_prop \u001b[38;5;241m=\u001b[39m \u001b[43mstormpy\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mparse_properties_without_context\u001b[49m\u001b[43m(\u001b[49m\u001b[43mprop\u001b[49m\u001b[43m)\u001b[49m \n\u001b[1;32m 19\u001b[0m stormpy_result \u001b[38;5;241m=\u001b[39m stormpy\u001b[38;5;241m.\u001b[39mmodel_checking(stormpy_model, parsed_prop, extract_scheduler\u001b[38;5;241m=\u001b[39mscheduler)\n\u001b[1;32m 20\u001b[0m stormvogel_result \u001b[38;5;241m=\u001b[39m stormvogel\u001b[38;5;241m.\u001b[39mresult\u001b[38;5;241m.\u001b[39mconvert_model_checking_result(stormvogel_model, stormpy_result)\n", - "\u001b[0;31mTypeError\u001b[0m: parse_properties_without_context(): incompatible function arguments. The following argument types are supported:\n 1. (formula_string: str, property_filter: Optional[Set[str]] = None) -> List[stormpy.core.Property]\n\nInvoked with: []" - ] + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "423136e0bf054647a4c0a03d7445cfa8", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "Output()" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "443fe89c24aa451bb549ece263673661", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(), Output()))" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], - "source": [ - "stormvogel_model = mapping.stormpy_to_stormvogel(leader_model)\n", - "\n", - "#a stormvogel result can also be obtained directly:\n", - "#stormvogel_result = model_checking.model_checking(stormvogel_model, prop[0], True)\n", - "\n", - "stormvogel_result = result.convert_model_checking_result(stormvogel_model, stormpy_result)" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "scrolled": true - }, - "outputs": [], "source": [ "import stormvogel.layout\n", "\n", @@ -308,34 +332,22 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 16, "metadata": {}, - "outputs": [ - { - "ename": "NameError", - "evalue": "name 'stormvogel_result' is not defined", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mNameError\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[11], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m induced_dtmc \u001b[38;5;241m=\u001b[39m \u001b[43mstormvogel_result\u001b[49m\u001b[38;5;241m.\u001b[39mgenerate_induced_dtmc()\n", - "\u001b[0;31mNameError\u001b[0m: name 'stormvogel_result' is not defined" - ] - } - ], + "outputs": [], "source": [ "induced_dtmc = stormvogel_result.generate_induced_dtmc()" ] }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 17, "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "a44b9b958747405b84ab6467441ca86a", + "model_id": "a56ece4593504c95b575e61387666219", "version_major": 2, "version_minor": 0 }, @@ -349,7 +361,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "ec5f0ce2baf24964b07078b37cf7e46f", + "model_id": "0bb6d1006f5c4805906414ae77c05328", "version_major": 2, "version_minor": 0 }, @@ -365,34 +377,6 @@ "vis2 = show.show(induced_dtmc, layout=stormvogel.layout.EXPLORE())" ] }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, { "cell_type": "code", "execution_count": null, @@ -403,9 +387,9 @@ ], "metadata": { "kernelspec": { - "display_name": "Python (stormvogel)", + "display_name": "Python 3 (ipykernel)", "language": "python", - "name": "stormvogel-env" + "name": "python3" }, "language_info": { "codemirror_mode": { @@ -417,7 +401,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.5" + "version": "3.12.7" } }, "nbformat": 4, From c604f1ab60498cc34d4a258ce79acec5bbc434ba Mon Sep 17 00:00:00 2001 From: PimLeerkes <83347609+PimLeerkes@users.noreply.github.com> Date: Sat, 14 Dec 2024 15:18:42 +0100 Subject: [PATCH 07/13] Update 04_mdp.ipynb From e5b571b9cba904940728697968cbf8f06166fb51 Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sat, 14 Dec 2024 17:25:36 +0100 Subject: [PATCH 08/13] some property string builder ideas --- stormvogel/model_checking.py | 40 +++++++++++++++++++ stormvogel/property_builder.py | 72 ++++++++++++++++++++++++++++++++++ tests/test_model_checking.py | 4 +- tests/test_property_builder.py | 12 ++++++ 4 files changed, 126 insertions(+), 2 deletions(-) create mode 100644 stormvogel/property_builder.py create mode 100644 tests/test_property_builder.py diff --git a/stormvogel/model_checking.py b/stormvogel/model_checking.py index 94abbe4..38df935 100644 --- a/stormvogel/model_checking.py +++ b/stormvogel/model_checking.py @@ -35,3 +35,43 @@ 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 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'." + ) diff --git a/stormvogel/property_builder.py b/stormvogel/property_builder.py new file mode 100644 index 0000000..0dd3af1 --- /dev/null +++ b/stormvogel/property_builder.py @@ -0,0 +1,72 @@ +import stormvogel.model + + +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 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'." + ) + + +def build_property_string_interactive(): + prop = "" + print("Welcome to the stormvogel property string builder.") + if input("Check propabilities (p) or rewards (r): ") == "p": + prop += "P" + if input("Does the model support actions (y) or (n)? ") == "y": + if ( + input("Do you want the maximum (max) or minimum (min) probability? ") + == "max" + ): + prop += "max=?" + else: + prop += "min=?" + else: + prop += "=?" + + label = input( + "For what state label do you want to know the reachability probability? " + ) + prop += f' [F "{label}"]' + else: + prop += "R" + + print("The resulting property string is: ", prop) + return prop + + +if __name__ == "__main__": + build_property_string_interactive() diff --git a/tests/test_model_checking.py b/tests/test_model_checking.py index c2a58d8..97955b1 100644 --- a/tests/test_model_checking.py +++ b/tests/test_model_checking.py @@ -9,7 +9,7 @@ def test_model_checking(): # we get our result using the stormvogel model checker function indirectly mdp = examples.monty_hall.create_monty_hall_mdp() - prop = 'Pmin=? [F "done"]' + prop = 'Pmax=? [F "done"]' result = stormvogel.model_checking.model_checking(mdp, prop, True) # and directly @@ -28,7 +28,7 @@ def test_model_checking(): # now we do it for a dtmc: dtmc = examples.die.create_die_dtmc() - prop = 'Pmin=? [F "rolled1"]' + prop = 'P=? [F "rolled1"]' result = stormvogel.model_checking.model_checking(dtmc, prop, True) # indirectly: diff --git a/tests/test_property_builder.py b/tests/test_property_builder.py new file mode 100644 index 0000000..82a767e --- /dev/null +++ b/tests/test_property_builder.py @@ -0,0 +1,12 @@ +import examples.die +import stormvogel.property_builder + + +def test_property_string_builder(): + # we want to create this string 'Pmin=? [F "rolled1"]': + + dtmc = examples.die.create_die_dtmc() + prop_builder = stormvogel.model_checking.PropertyBuilder(dtmc) + prop = prop_builder.get_reachabilty_probability("rolled1") + + assert prop == 'P=? [F "rolled1"]' From 859f5b9efb69622a336d8cd4710f204ff24e4489 Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sun, 15 Dec 2024 13:13:25 +0100 Subject: [PATCH 09/13] interactive property builder can be used from within the model checker --- docs/getting_started/04_mdp.ipynb | 18 ++- docs/getting_started/model.html | 188 +++++++++++++++++++++++++----- stormvogel/model.py | 9 ++ stormvogel/model_checking.py | 53 +++------ stormvogel/property_builder.py | 109 +++++++++-------- tests/test_property_builder.py | 12 -- 6 files changed, 248 insertions(+), 141 deletions(-) delete mode 100644 tests/test_property_builder.py diff --git a/docs/getting_started/04_mdp.ipynb b/docs/getting_started/04_mdp.ipynb index 1e6014a..ba4443c 100644 --- a/docs/getting_started/04_mdp.ipynb +++ b/docs/getting_started/04_mdp.ipynb @@ -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" ] }, @@ -2531,7 +2543,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.6" + "version": "3.12.7" } }, "nbformat": 4, diff --git a/docs/getting_started/model.html b/docs/getting_started/model.html index 511a1da..b146e37 100644 --- a/docs/getting_started/model.html +++ b/docs/getting_started/model.html @@ -1,6 +1,6 @@