From fb7ae1578dff9033cd29e1adf10c6aa593e40d0e Mon Sep 17 00:00:00 2001 From: PimLeerkes Date: Thu, 31 Oct 2024 18:02:13 +0100 Subject: [PATCH] temporary examples package problem fix --- Untitled.ipynb | 43 ++++++ docs/getting_started/die.ipynb | 40 +++--- docs/getting_started/mdp.ipynb | 80 +++++++++-- docs/getting_started/simulator.ipynb | 198 ++++++++++++++++++++++++--- poetry.lock | 2 +- pyproject.toml | 7 +- stormvogel/simulator.py | 83 ----------- 7 files changed, 309 insertions(+), 144 deletions(-) create mode 100644 Untitled.ipynb diff --git a/Untitled.ipynb b/Untitled.ipynb new file mode 100644 index 0000000..dba60c4 --- /dev/null +++ b/Untitled.ipynb @@ -0,0 +1,43 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "id": "c4d32ada-47ed-412e-95dd-3f16880fa568", + "metadata": {}, + "outputs": [], + "source": [ + "import examples" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "1935eab3-9731-4cd3-9fde-cbd22a25eea3", + "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/docs/getting_started/die.ipynb b/docs/getting_started/die.ipynb index 0844265..301ff3a 100644 --- a/docs/getting_started/die.ipynb +++ b/docs/getting_started/die.ipynb @@ -11,13 +11,27 @@ "cell_type": "code", "execution_count": 1, "metadata": {}, - "outputs": [], + "outputs": [ + { + "ename": "ModuleNotFoundError", + "evalue": "No module named 'examples'", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mModuleNotFoundError\u001b[0m Traceback (most recent call last)", + "Cell \u001b[0;32mIn[1], line 7\u001b[0m\n\u001b[1;32m 4\u001b[0m \u001b[38;5;28;01mimport\u001b[39;00m \u001b[38;5;21;01mstormvogel\u001b[39;00m\u001b[38;5;21;01m.\u001b[39;00m\u001b[38;5;21;01mmapping\u001b[39;00m\n\u001b[1;32m 5\u001b[0m \u001b[38;5;28;01mimport\u001b[39;00m \u001b[38;5;21;01mstormpy\u001b[39;00m\n\u001b[0;32m----> 7\u001b[0m \u001b[38;5;28;01mimport\u001b[39;00m \u001b[38;5;21;01mexamples\u001b[39;00m\u001b[38;5;21;01m.\u001b[39;00m\u001b[38;5;21;01mdie\u001b[39;00m\n", + "\u001b[0;31mModuleNotFoundError\u001b[0m: No module named 'examples'" + ] + } + ], "source": [ "import stormvogel.model\n", "import stormvogel.visualization\n", "import stormvogel.show\n", "import stormvogel.mapping\n", - "import stormpy" + "import stormpy\n", + "\n", + "import examples.die" ] }, { @@ -29,7 +43,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 3, "metadata": { "scrolled": true }, @@ -37,7 +51,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "6aa5be91a6a041c39340ffa6390225b5", + "model_id": "d1eded56d0fa4392b74b8b8fad251b65", "version_major": 2, "version_minor": 0 }, @@ -48,22 +62,10 @@ "metadata": {}, "output_type": "display_data" }, - { - "data": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "7c32b09fa7ad42ddb62483aa1b038354", + "model_id": "67aac6234dfa4131b012378ba3e0e8ce", "version_major": 2, "version_minor": 0 }, @@ -123,9 +125,9 @@ ], "metadata": { "kernelspec": { - "display_name": "Python (stormvogel)", + "display_name": "stormvogel", "language": "python", - "name": "stormvogel-env" + "name": "stormvogel" }, "language_info": { "codemirror_mode": { diff --git a/docs/getting_started/mdp.ipynb b/docs/getting_started/mdp.ipynb index a999f02..0dd3467 100644 --- a/docs/getting_started/mdp.ipynb +++ b/docs/getting_started/mdp.ipynb @@ -18,7 +18,7 @@ { "data": { "text/plain": [ - "" + "" ] }, "execution_count": 2, @@ -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,7 +167,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 5, "metadata": {}, "outputs": [], "source": [ @@ -176,7 +176,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 6, "metadata": {}, "outputs": [], "source": [ @@ -185,7 +185,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -202,7 +202,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -232,7 +232,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -254,7 +254,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 10, "metadata": { "scrolled": true }, @@ -267,7 +267,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 11, "metadata": { "scrolled": true }, @@ -275,12 +275,50 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "bccaeb3962e24a84a838417dd4210d04", + "model_id": "997d4600f467461ea1373a3ada686982", "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": { + "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": "f45b2ef528d34e9fadcd1202511779a3", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(), Output()))" ] }, "metadata": {}, @@ -310,12 +348,26 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "bccaeb3962e24a84a838417dd4210d04", + "model_id": "28051486259a4ca8852934d34a5b64ce", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "Output()" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "913f91028e9443b6822c19813374c072", "version_major": 2, "version_minor": 0 }, "text/plain": [ - "Output(outputs=({'output_type': 'display_data', 'data': {'text/plain': '', '\u2026" + "HBox(children=(Output(), Output()))" ] }, "metadata": {}, diff --git a/docs/getting_started/simulator.ipynb b/docs/getting_started/simulator.ipynb index 0a4df45..8d27f49 100644 --- a/docs/getting_started/simulator.ipynb +++ b/docs/getting_started/simulator.ipynb @@ -2,19 +2,90 @@ "cells": [ { "cell_type": "code", - "execution_count": 1, + "execution_count": 14, "id": "a8ddc37c-66d2-43e4-8162-6be19a1d70a1", "metadata": {}, "outputs": [], "source": [ - "import stormvogel.simulator\n", - "import stormvogel.model\n", - "import examples.monty_hall" + "from stormvogel import visualization, show, simulator, model" ] }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 15, + "id": "cab40f99-3460-4497-8b9f-3d669eee1e11", + "metadata": {}, + "outputs": [], + "source": [ + "# We create the monty hall mdp\n", + "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()" + ] + }, + { + "cell_type": "code", + "execution_count": 16, "id": "eb0fadc0-7bb6-4c1d-ae3e-9e16527726ab", "metadata": {}, "outputs": [ @@ -29,50 +100,135 @@ "State 1 with labels ['carchosen'] and features {}\n", "State 2 with labels ['open'] and features {}\n", "State 3 with labels ['goatrevealed'] and features {}\n", - "State 4 with labels ['done'] and features {}\n", + "State 4 with labels ['target', 'done'] and features {}\n", "\n", "Transitions:\n" ] } ], "source": [ - "#we take for example the monty hall mdp model:\n", - "mdp = examples.monty_hall.create_monty_hall_mdp()\n", + "#we want to simulate this model. That is, we start at the initial state and then\n", + "#we walk through the model according to transition probabilities.\n", + "#When we do this, we get a partial model as a result that contains everything we discovered\n", + "#during this walk.\n", "\n", - "#we cam then simulate the model with the simulator to create a partial model:\n", - "partial_model = stormvogel.simulator.simulate(mdp, runs=1, steps=4, seed=123456)\n", + "#we can choose how many steps we take:\n", + "steps = 4\n", "\n", + "#and we can specify a seed if we want:\n", + "seed = 123456\n", + "\n", + "#then we run the simulator:\n", + "partial_model = stormvogel.simulator.simulate(mdp, steps=steps, seed=seed)\n", "print(partial_model)" ] }, { "cell_type": "code", - "execution_count": 6, - "id": "34d0c293-d090-4e3d-9e80-4351f5fcba62", - "metadata": {}, + "execution_count": 17, + "id": "59ac1e34-866c-42c4-b19b-c2a15c830e2e", + "metadata": { + "scrolled": true + }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "initial state --(action: empty)--> state: 2 --(action: open2)--> state: 9 --(action: empty)--> state: 20 --(action: stay)--> state: 39\n" + "ModelType.MDP with name None\n", + "\n", + "States:\n", + "State 0 with labels ['init'] and features {}\n", + "State 1 with labels ['carchosen'] and features {}\n", + "State 2 with labels ['open'] and features {}\n", + "State 3 with labels ['goatrevealed'] and features {}\n", + "State 4 with labels ['done'] and features {}\n", + "\n", + "Transitions:\n" ] } ], "source": [ - "#we can also simulate a path:\n", - "path = stormvogel.simulator.simulate_path(mdp, steps=4, seed=123456)\n", + "#it still chooses random actions but we can prevent this by providing a scheduler:\n", + "taken_actions = {}\n", + "for id, state in mdp.states.items():\n", + " taken_actions[id] = state.available_actions()[0]\n", + "scheduler = stormvogel.result.Scheduler(mdp, taken_actions)\n", "\n", - "print(path)" + "partial_model = stormvogel.simulator.simulate(mdp, steps=steps, scheduler=scheduler, seed=seed)\n", + "print(partial_model)" ] }, { "cell_type": "code", - "execution_count": null, - "id": "6b03bb18-4c65-4544-9f2b-fd58682a829d", + "execution_count": 20, + "id": "22871288-755c-463f-9150-f207c2f5c211", "metadata": {}, - "outputs": [], - "source": [] + "outputs": [ + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "f92e1a66e2034c70832b36e2bd7fe70f", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "Output()" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "b413c4c87cb34895b0a4551b4e49ed16", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + "HBox(children=(Output(), Output()))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "#we can also visualize the partial model that we get from the simulator:\n", + "show.show(partial_model)" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "id": "34d0c293-d090-4e3d-9e80-4351f5fcba62", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "initial state --(action: empty)--> state: 2 --(action: open0)--> state: 7 --(action: empty)--> state: 17 --(action: stay)--> state: 33\n" + ] + } + ], + "source": [ + "#we can also use another simulator function that returns a path instead of a partial model:\n", + "path = stormvogel.simulator.simulate_path(mdp, steps=4, scheduler=scheduler, seed=123456)\n", + "\n", + "print(path)" + ] } ], "metadata": { diff --git a/poetry.lock b/poetry.lock index 3082d79..c53feeb 100644 --- a/poetry.lock +++ b/poetry.lock @@ -3436,4 +3436,4 @@ files = [ [metadata] lock-version = "2.0" python-versions = "^3.11" -content-hash = "65bbdf4a8a22412ec0f95ebe412b3ec8a4821be723e154dfa0a80c8dc73ccc46" +content-hash = "c7ce7fa5e4ee787e2296e46d57bce7e48c2fd7f8a8b848f6b3a06de03989023f" diff --git a/pyproject.toml b/pyproject.toml index a3241c1..f265a76 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -10,11 +10,6 @@ authors = ["The stormvogel team"] license = "GPLv3" readme = "README.md" -packages = [ - { include = "stormvogel" }, - { include = "examples" } -] - [tool.poetry.dependencies] python = "^3.11" ipywidgets = "^8.1.3" @@ -28,6 +23,7 @@ matplotlib = "^3.9.2" anyio = "^4.6.0" nbmake = "^1.5.4" mock = "^5.1.0" +jupyter = "^1.1.1" [tool.poetry.group.test.dependencies] pytest = "^8.2.2" @@ -43,7 +39,6 @@ jupyterlab = "^4.2.2" sphinx = "^7.3.7" furo = "^2024.5.6" nbsphinx = "^0.9.4" -jupyter = "^1.0.0" [tool.ruff] src = ["stormvogel", "examples"] diff --git a/stormvogel/simulator.py b/stormvogel/simulator.py index 2dab3f6..34d7400 100644 --- a/stormvogel/simulator.py +++ b/stormvogel/simulator.py @@ -5,11 +5,6 @@ import stormvogel.model import stormpy.examples.files import stormpy.examples -import examples.die -import examples.monty_hall -import examples.monty_hall_pomdp -import examples.nuclear_fusion_ctmc -import examples.simple_ma import random @@ -283,81 +278,3 @@ def get_range_index(stateid: int): break return partial_model - - -if __name__ == "__main__": - """ - # we first test it with a dtmc - dtmc = examples.die.create_die_dtmc() - rewardmodel = dtmc.add_rewards("rewardmodel") - for stateid in dtmc.states.keys(): - rewardmodel.rewards[stateid] = 1 - - rewardmodel2 = dtmc.add_rewards("rewardmodel2") - for stateid in dtmc.states.keys(): - rewardmodel2.rewards[stateid] = 2 - - partial_model = simulate(dtmc, 1, 10) - print(partial_model) - path = simulate_path(dtmc, 5) - print(path) - """ - """ - # then we test it with an mdp - mdp = examples.monty_hall.create_monty_hall_mdp() - rewardmodel = mdp.add_rewards("rewardmodel") - for i in range(67): - rewardmodel.rewards[i] = i - rewardmodel2 = mdp.add_rewards("rewardmodel2") - for i in range(67): - rewardmodel2.rewards[i] = i - - taken_actions = {} - for id, state in mdp.states.items(): - taken_actions[id] = state.available_actions()[0] - scheduler = stormvogel.result.Scheduler(mdp, taken_actions) - - partial_model = simulate(mdp, 10, 1, scheduler) - path = simulate_path(mdp, 5) - print(partial_model) - assert partial_model is not None - print(path) - print(partial_model.rewards) - """ - - # then we test it with a pomdp - pomdp = examples.monty_hall_pomdp.create_monty_hall_pomdp() - - taken_actions = {} - for id, state in pomdp.states.items(): - taken_actions[id] = state.available_actions()[0] - scheduler = stormvogel.result.Scheduler(pomdp, taken_actions) - - partial_model = simulate(pomdp, 10, 10, scheduler) - path = simulate_path(pomdp, 5) - print(partial_model) - print(path) - - """ - # then we test it with a ctmc - ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc() - partial_model = simulate(ctmc, 10, 10) - path = simulate_path(ctmc, 5) - print(partial_model) - print(path) - - # TODO Markov automatas - - - ma = examples.simple_ma.create_simple_ma() - - taken_actions = {} - for id, state in ma.states.items(): - taken_actions[id] = state.available_actions()[0] - scheduler = stormvogel.result.Scheduler(ma, taken_actions) - - partial_model = simulate(ma, 10, 10, scheduler) - #path = simulate_path(ma, 5) - print(partial_model) - #print(path) - """