From 093664cd69380079d777d834bb20b1748c48ffba Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Tue, 25 Feb 2025 12:06:01 +0100 Subject: [PATCH] made a start on the property builder widget --- docs/getting_started/04_mdp.ipynb | 66 ++--- docs/getting_started/10_model_checking.ipynb | 265 +++++++++++++++++++ stormvogel/layout.py | 7 + stormvogel/layouts/property_string.json | 118 +++++++++ stormvogel/mapping.py | 2 +- stormvogel/model.py | 11 + stormvogel/model_checking.py | 3 +- stormvogel/property_builder.py | 20 +- 8 files changed, 438 insertions(+), 54 deletions(-) create mode 100644 docs/getting_started/10_model_checking.ipynb create mode 100644 stormvogel/layouts/property_string.json diff --git a/docs/getting_started/04_mdp.ipynb b/docs/getting_started/04_mdp.ipynb index b638e2f..5da4d71 100644 --- a/docs/getting_started/04_mdp.ipynb +++ b/docs/getting_started/04_mdp.ipynb @@ -9,7 +9,7 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 14, "metadata": {}, "outputs": [], "source": [ @@ -19,16 +19,16 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "" + "" ] }, - "execution_count": 2, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -132,7 +132,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 16, "metadata": {}, "outputs": [], "source": [ @@ -142,7 +142,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -174,7 +174,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 18, "metadata": {}, "outputs": [], "source": [ @@ -183,7 +183,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 19, "metadata": {}, "outputs": [], "source": [ @@ -192,7 +192,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -209,7 +209,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -239,7 +239,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -261,7 +261,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 23, "metadata": { "scrolled": true }, @@ -274,7 +274,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 24, "metadata": { "scrolled": true }, @@ -282,7 +282,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "da5d1ffd4d864e61818cad4ba5aa84e2", + "model_id": "43744e33c53e49adb37d4f6f1854613b", "version_major": 2, "version_minor": 0 }, @@ -293,44 +293,10 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "application/javascript": [ - "return_id_result('http://127.0.0.1:8892', 'MRUCAmayGSiiBVtFKZLo', 'test message')" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "3d1ee93242b0442ab576e078585fbae1", + "model_id": "63e4fdcb620d4285abe0d4febd0eee22", "version_major": 2, "version_minor": 0 }, @@ -344,7 +310,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "78d3ba8f89064fcd98b5eb5b9eb666ef", + "model_id": "69eacefaf7aa4630881ace29c28e879b", "version_major": 2, "version_minor": 0 }, diff --git a/docs/getting_started/10_model_checking.ipynb b/docs/getting_started/10_model_checking.ipynb new file mode 100644 index 0000000..dd46d34 --- /dev/null +++ b/docs/getting_started/10_model_checking.ipynb @@ -0,0 +1,265 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "id": "f677ad96-491b-410b-b161-1801e8ee526a", + "metadata": {}, + "outputs": [], + "source": [ + "import stormvogel.model\n", + "from stormvogel import show, model_checking, property_builder" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "56e3af45-3e12-43d6-a16a-786da89ef504", + "metadata": { + "scrolled": true + }, + "outputs": [ + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "e7bb279f00df49dbac8fd92b652ad881", + "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": { + "application/javascript": [ + "return_id_result('http://127.0.0.1:8889', 'LmarPXzNfSLOpbrzOBbl', 'test message')" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "96feaffe194f4a77b90237350c43a723", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "Output()" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "79501639bf784551a0883b9ddf15bd26", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(), Output()))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "mdp = stormvogel.model.new_mdp(\"Monty Hall\")\n", + "\n", + "init = mdp.get_initial_state()\n", + "\n", + "# first choose car position\n", + "init.set_transitions(\n", + " [(1 / 3, mdp.new_state(\"carchosen\", {\"car_pos\": i})) for i in range(3)]\n", + ")\n", + "\n", + "# we choose a door in each case\n", + "for s in mdp.get_states_with_label(\"carchosen\"):\n", + " s.set_transitions(\n", + " [\n", + " (\n", + " mdp.action(f\"open{i}\"),\n", + " mdp.new_state(\"open\", s.features | {\"chosen_pos\": i}),\n", + " )\n", + " for i in range(3)\n", + " ]\n", + " )\n", + "\n", + "# the other goat is revealed\n", + "for s in mdp.get_states_with_label(\"open\"):\n", + " car_pos = s.features[\"car_pos\"]\n", + " chosen_pos = s.features[\"chosen_pos\"]\n", + " other_pos = {0, 1, 2} - {car_pos, chosen_pos}\n", + " s.set_transitions(\n", + " [\n", + " (\n", + " 1 / len(other_pos),\n", + " mdp.new_state(\"goatrevealed\", s.features | {\"reveal_pos\": i}),\n", + " )\n", + " for i in other_pos\n", + " ]\n", + " )\n", + "\n", + "# we must choose whether we want to switch\n", + "for s in mdp.get_states_with_label(\"goatrevealed\"):\n", + " car_pos = s.features[\"car_pos\"]\n", + " chosen_pos = s.features[\"chosen_pos\"]\n", + " reveal_pos = s.features[\"reveal_pos\"]\n", + " other_pos = list({0, 1, 2} - {reveal_pos, chosen_pos})[0]\n", + " s.set_transitions(\n", + " [\n", + " (\n", + " mdp.action(\"stay\"),\n", + " mdp.new_state(\n", + " [\"done\"] + ([\"target\"] if chosen_pos == car_pos else []),\n", + " s.features | {\"chosen_pos\": chosen_pos},\n", + " ),\n", + " ),\n", + " (\n", + " mdp.action(\"switch\"),\n", + " mdp.new_state(\n", + " [\"done\"] + ([\"target\"] if other_pos == car_pos else []),\n", + " s.features | {\"chosen_pos\": other_pos},\n", + " ),\n", + " ),\n", + " ]\n", + " )\n", + "\n", + "# we add self loops to all states with no outgoing transitions\n", + "mdp.add_self_loops()\n", + "\n", + "show.show(mdp, show_editor=True)" + ] + }, + { + "cell_type": "markdown", + "id": "a954571f-a723-4145-8cb6-2a94fa986718", + "metadata": {}, + "source": [ + "We can do model checking on this model by only using stormvogel functions directly. Behind the scenes this calls the stormpy model checker." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "4fe1edee-15ab-45ad-8605-f1c646186718", + "metadata": {}, + "outputs": [ + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "c86474e4a728417a855d24ef10d1def9", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(),))" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "property = stormvogel.property_builder.build_property_string(mdp)\n", + "#result = stormvogel.model_checking.model_checking(mdp)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "25cd927d-d4ef-4d93-b1d8-d6efb30d1dce", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "a0a8713d-034f-4225-8203-c8e024027f0f", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "02cf28bf-4644-4511-95ae-1859dabac886", + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "80ab60c3-646d-4224-a5f8-b569586930f4", + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.12.7" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/stormvogel/layout.py b/stormvogel/layout.py index ed71a30..c231651 100644 --- a/stormvogel/layout.py +++ b/stormvogel/layout.py @@ -98,3 +98,10 @@ def EXPLORE(): return Layout( os.path.join(PACKAGE_ROOT_DIR, "layouts/explore.json"), path_relative=False ) + + +def PROPERTY_STRING(): + return Layout( + os.path.join(PACKAGE_ROOT_DIR, "layouts/property_string.json"), + path_relative=False, + ) diff --git a/stormvogel/layouts/property_string.json b/stormvogel/layouts/property_string.json new file mode 100644 index 0000000..c060ecc --- /dev/null +++ b/stormvogel/layouts/property_string.json @@ -0,0 +1,118 @@ +{ + "__fake_macros": { + "__group_macro": { + "borderWidth": 1, + "color": { + "background": "white", + "border": "black", + "highlight": { + "background": "white", + "border": "red" + } + }, + "shape": "ellipse", + "mass": 1, + "font": { + "color": "black", + "size": 14 + } + } + }, + "groups": { + "type": { + "borderWidth": 1, + "color": { + "background": "white", + "border": "black", + "highlight": { + "background": "white", + "border": "red" + } + }, + "shape": "ellipse", + "mass": 1, + "font": { + "color": "black", + "size": 14 + } + }, + "task": { + "borderWidth": 1, + "color": { + "background": "lightblue", + "border": "black", + "highlight": { + "background": "white", + "border": "red" + } + }, + "shape": "box", + "mass": 1, + "font": { + "color": "black", + "size": 14 + } + }, + "scheduled_actions": { + "borderWidth": 1, + "color": { + "background": "pink", + "border": "black", + "highlight": { + "background": "white", + "border": "red" + } + }, + "shape": "box", + "mass": 1, + "font": { + "color": "black", + "size": 14 + }, + "schedColor": false + } + }, + "reload_button": false, + "edges": { + "arrows": "to", + "font": { + "color": "black", + "size": 14 + }, + "color": { + "color": "black" + } + }, + "numbers": { + "fractions": true, + "digits": 5 + }, + "state_properties": { + "show_results": true, + "result_symbol": "\u2606", + "show_rewards": true, + "reward_symbol": "\u20ac", + "show_zero_rewards": true, + "show_observations": true, + "observation_symbol": "\u0298" + }, + "layout": { + "randomSeed": 5 + }, + "misc": { + "enable_physics": true, + "width": 800, + "height": 600, + "explore": false + }, + "saving": { + "relative_path": true, + "filename": "layouts/NAME.json", + "save_button": false, + "load_button": false + }, + "positions": {}, + "width": 800, + "height": 600, + "physics": true +} diff --git a/stormvogel/mapping.py b/stormvogel/mapping.py index b3e30c0..0f7bd71 100644 --- a/stormvogel/mapping.py +++ b/stormvogel/mapping.py @@ -63,7 +63,7 @@ def add_labels(model: stormvogel.model.Model) -> stormpy.storage.StateLabeling: """ assert stormpy is not None - state_labeling = stormpy.storage.StateLabeling(len(model.states)) + state_labeling = stormpy.storage.StateLabeling(len(list(model.states.keys()))) # we first add all the different labels for label in model.get_labels(): diff --git a/stormvogel/model.py b/stormvogel/model.py index 394ed16..740847b 100644 --- a/stormvogel/model.py +++ b/stormvogel/model.py @@ -1065,6 +1065,17 @@ def __eq__(self, other) -> bool: return False +def from_prism(prism_code="stormpy.storage.storage.PrismProgram"): + """Create a model from prism. Requires stormpy.""" + try: + import stormpy + import stormvogel.mapping + + return stormvogel.mapping.stormpy_to_stormvogel(stormpy.build_model(prism_code)) + except ImportError: + RuntimeError("Using PRISM requires stormpy.") + + def new_dtmc(name: str | None = None, create_initial_state: bool = True) -> Model: """Creates a DTMC.""" return Model(name, ModelType.DTMC, create_initial_state) diff --git a/stormvogel/model_checking.py b/stormvogel/model_checking.py index a9a1980..21c3a48 100644 --- a/stormvogel/model_checking.py +++ b/stormvogel/model_checking.py @@ -2,7 +2,6 @@ import stormvogel.result import stormvogel.model import stormvogel.property_builder -import examples.monty_hall try: import stormpy @@ -52,6 +51,8 @@ def model_checking( if __name__ == "__main__": + import examples.monty_hall + mdp = examples.monty_hall.create_monty_hall_mdp() rewardmodel = mdp.add_rewards("rewardmodel") diff --git a/stormvogel/property_builder.py b/stormvogel/property_builder.py index 01141ee..e7cefe0 100644 --- a/stormvogel/property_builder.py +++ b/stormvogel/property_builder.py @@ -1,5 +1,9 @@ import stormvogel.model -import examples.monty_hall +import stormvogel.layout +import stormvogel.layout_editor +import stormvogel.communication_server +import ipywidgets as widgets +import IPython.display as ipd def build_property_string_interactive(model: stormvogel.model.Model) -> str: @@ -101,7 +105,19 @@ def labels() -> str: return prop +def build_property_string(model: stormvogel.model.Model): + """Lets the user build a property string using a widget""" + layout = stormvogel.layout.PROPERTY_STRING() + # do_init_server = stormvogel.communication_server.enable_server + e = stormvogel.layout_editor.LayoutEditor(layout, do_display=False) + e.show() + box = widgets.HBox(children=[e.output]) + ipd.display(box) + + if __name__ == "__main__": + import examples.monty_hall + mdp = examples.monty_hall.create_monty_hall_mdp() - build_property_string_interactive(mdp) + build_property_string(mdp)