From e5b571b9cba904940728697968cbf8f06166fb51 Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Sat, 14 Dec 2024 17:25:36 +0100 Subject: [PATCH 1/6] 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 2/6] 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 @@