From 04362becb6b6c29dac38e36872f8c1e24bdc2761 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 19 May 2022 14:30:25 +0200 Subject: [PATCH 01/11] first version of documentation for simulators --- doc/source/doc/simulator.ipynb | 612 +++++++++++++++++++++ lib/stormpy/examples/files.py | 2 + lib/stormpy/examples/files/mdp/maze_2.nm | 2 +- lib/stormpy/examples/files/mdp/slipgrid.nm | 29 + lib/stormpy/simulator.py | 2 +- 5 files changed, 645 insertions(+), 2 deletions(-) create mode 100644 doc/source/doc/simulator.ipynb create mode 100644 lib/stormpy/examples/files/mdp/slipgrid.nm diff --git a/doc/source/doc/simulator.ipynb b/doc/source/doc/simulator.ipynb new file mode 100644 index 0000000000..ab9c9961f8 --- /dev/null +++ b/doc/source/doc/simulator.ipynb @@ -0,0 +1,612 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": { + "collapsed": true, + "pycharm": { + "name": "#%%md\n" + } + }, + "source": [ + "# Working with Simulators\n", + "\n", + "The simulators in stormpy are meant to mimic access to unknown models,\n", + "but they can also be used to explore the model.\n", + "\n", + "All simulators implement the abstract class stormpy.simulator.Simulator. \n", + "\n", + "The different simulators are different in the model representation they use in the background and in the representation of the states and actions exposed to the user. We will go through some options by example!\n" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "import stormpy\n", + "import stormpy.examples\n", + "import stormpy.examples.files\n", + "import stormpy.simulator" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Model-based simulation\n", + "\n", + "We first start with an explicit model-based simulation. This means that we have a model of the DTMC in memory. This is fast and convenient if the model is available, but limits the size of models that we support.\n", + "\n", + "### DTMCs\n", + "We first discuss the interface for DTMCs, without any nondeterminism.\n", + "\n", + "#### Explicit state-representations\n", + "After importing some parts of stormpy as above, we start with creating a model, in this case a DTMC:" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": { + "scrolled": true + }, + "outputs": [], + "source": [ + "path = stormpy.examples.files.prism_dtmc_die\n", + "prism_program = stormpy.parse_prism_program(path)\n", + "model = stormpy.build_model(prism_program)\n", + "\n", + "simulator = stormpy.simulator.create_simulator(model, seed=42)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let us simulate a path." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(0, [0.0], {'init'})" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.restart()" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(2, [1.0], set())" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.step()" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(5, [1.0], set())" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.step()" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(11, [1.0], {'done', 'five'})" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.step()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We start the simulator by restarting. We then do 3 steps. Every step returns a triple (state, reward, labels). In particular, the simulation above reflects a path s0, s2, s5, s11. Taking the transitions inbetween yields the reward as shown above. While states s2 and s5 are not labelled, state s0 is labelled with `init` and state s11 is labelled with `done` and `five`. Indeed we can check this information on the model that we used for the simulator:\n" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{'done', 'five'}" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "model.labeling.get_labels_of_state(11)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We can continue sampling." + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(11, [0.0], {'done', 'five'})" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.step()" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(11, [0.0], {'done', 'five'})" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.step()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Indeed, we are not leaving the state, in this case, we can never leave the state as state s11 is absorbing. The simulator detects and exposes this information via `simulator.is_done()`" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.is_done()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We can sample more paths, yielding (potentially) different final states:" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "{7: 21, 9: 16, 10: 18, 11: 17, 12: 16, 8: 12}" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "simulator.restart()\n", + "final_outcomes = dict()\n", + "for n in range(100):\n", + " while not simulator.is_done():\n", + " observation, reward, labels = simulator.step()\n", + " if observation not in final_outcomes:\n", + " final_outcomes[observation] = 1\n", + " else:\n", + " final_outcomes[observation] += 1\n", + " simulator.restart()\n", + "final_outcomes" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Program-level representations" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We can run the same simulator but represent states symbolically, referring to the high-level description of the state rather than on its internal index. The advantage of this is that the process becomes independent of the underlying representation of the model. We first need to build the model with the required annotations." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [], + "source": [ + "options = stormpy.BuilderOptions()\n", + "options.set_build_state_valuations()\n", + "model = stormpy.build_sparse_model_with_options(prism_program, options)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Then, we can create simulator that uses program-level state observations." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [], + "source": [ + "simulator = stormpy.simulator.create_simulator(model, seed=42)\n", + "simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL)" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "'{\\n \"d\": 0,\\n \"s\": 0\\n}'" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "state, reward, label = simulator.restart()\n", + "str(state)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Indeed, the state is now an object that describes the state in terms of the variables of prism program, in this case variables \"s\" and \"d\". \n", + "\n", + "We can use the simulator as before, e.g.," + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "['coin_flips']\n", + "{\n", + " \"d\": 5,\n", + " \"s\": 7\n", + "}: 18, {\n", + " \"d\": 4,\n", + " \"s\": 7\n", + "}: 19, {\n", + " \"d\": 2,\n", + " \"s\": 7\n", + "}: 13, {\n", + " \"d\": 6,\n", + " \"s\": 7\n", + "}: 16, {\n", + " \"d\": 3,\n", + " \"s\": 7\n", + "}: 14, {\n", + " \"d\": 1,\n", + " \"s\": 7\n", + "}: 20\n" + ] + } + ], + "source": [ + "simulator.restart()\n", + "final_outcomes = dict()\n", + "print(simulator.get_reward_names())\n", + "for n in range(100):\n", + " while not simulator.is_done():\n", + " observation, reward, labels = simulator.step()\n", + " if observation not in final_outcomes:\n", + " final_outcomes[observation] = 1\n", + " else:\n", + " final_outcomes[observation] += 1\n", + " simulator.restart() \n", + "print(\", \".join([f\"{str(k)}: {v}\" for k,v in final_outcomes.items()]))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### MDPs" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Explicit representations" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "As above, we can represent states both explicitly or symbolically. We only discuss the explicit representation here. With nondeterminism, we now must resolve this nondeterminism externally. That is, the step argument now takes an argument, which we may pick randomly or in a more intelligent manner." + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "0 --act=1--> 2 --act=2--> 2 --act=2--> 5 --act=2--> 9 --act=0--> 12 --act=1--> 12 --act=0--> 9 --act=1--> 5 --act=2--> 5 --act=0--> 8 --act=3--> 8 --act=3--> 12 --act=1--> 14 --act=1--> 14 --act=2--> 14 --act=1--> 15 --act=0--> 15 --act=0--> 14 --act=1--> 14 --act=0--> 12\n", + "------\n", + "0 --act=0--> 0 --act=0--> 0 --act=1--> 2 --act=0--> 2 --act=0--> 2 --act=2--> 5 --act=2--> 5 --act=0--> 8 --act=0--> 5 --act=2--> 9 --act=1--> 9 --act=0--> 12 --act=0--> 9 --act=1--> 9 --act=1--> 5 --act=0--> 5 --act=1--> 2 --act=2--> 2 --act=0--> 2 --act=1--> 2\n", + "------\n", + "0 --act=1--> 2 --act=1--> 2 --act=2--> 2 --act=0--> 2 --act=0--> 2 --act=0--> 4 --act=3--> 8 --act=2--> 4 --act=1--> 7 --act=1--> 7 --act=2--> 7 --act=3--> 11 --act=2--> 7 --act=1--> 10 --act=0--> 10 --act=1--> 6 --act=1--> 10 --act=0--> 7 --act=0--> 7 --act=1--> 10\n", + "------\n" + ] + } + ], + "source": [ + "import random\n", + "path = stormpy.examples.files.prism_mdp_slipgrid\n", + "prism_program = stormpy.parse_prism_program(path)\n", + "\n", + "model = stormpy.build_model(prism_program)\n", + "simulator = stormpy.simulator.create_simulator(model, seed=42)\n", + "# 5 paths of at most 20 steps.\n", + "paths = []\n", + "for m in range(3):\n", + " path = []\n", + " state, reward, labels = simulator.restart()\n", + " path = [f\"{state}\"]\n", + " for n in range(20):\n", + " actions = simulator.available_actions()\n", + " select_action = random.randint(0,len(actions)-1)\n", + " path.append(f\"--act={actions[select_action]}-->\")\n", + " state, reward, labels = simulator.step(actions[select_action])\n", + " path.append(f\"{state}\")\n", + " if simulator.is_done():\n", + " break\n", + " paths.append(path)\n", + "for path in paths:\n", + " print(\" \".join(path))\n", + " print(\"------\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "In the example above, the actions are internal numbers. Often, a program gives semantically meaningful names, such as moving `north`, `east`, `west` and `south` in a grid with program variables reflecting the `x` and `y` location." + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": { + "scrolled": true + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(1,1) --south--> (2,1) --south--> (2,1) --west--> (2,2) --north--> (1,2) --east--> (1,1) --south--> (1,1) --south--> (2,1) --west--> (2,1) --west--> (2,1) --west--> (2,2) --east--> (2,1) --west--> (2,2) --north--> (2,2) --north--> (1,2) --south--> (2,2) --east--> (2,2) --east--> (2,2) --south--> (2,2) --west--> (2,2) --south--> (3,2)\n", + "(1,1) --south--> (1,1) --west--> (1,1) --south--> (2,1) --north--> (1,1) --west--> (1,1) --west--> (1,2) --south--> (1,2) --south--> (2,2) --south--> (3,2) --west--> (3,3) --south--> (4,3) --east--> (4,2) --north--> (3,2) --north--> (3,2) --south--> (4,2) --north--> (3,2) --east--> (3,1) --north--> (2,1) --north--> (1,1) --south--> (2,1)\n", + "(1,1) --west--> (1,2) --east--> (1,2) --south--> (1,2) --south--> (1,2) --west--> (1,2) --south--> (2,2) --south--> (3,2) --north--> (2,2) --north--> (1,2) --west--> (1,2) --east--> (1,2) --east--> (1,1) --west--> (1,1) --south--> (2,1) --south--> (3,1) --north--> (2,1) --west--> (2,2) --north--> (1,2) --west--> (1,3) --east--> (1,3)\n" + ] + } + ], + "source": [ + "options = stormpy.BuilderOptions()\n", + "options.set_build_choice_labels()\n", + "options.set_build_state_valuations()\n", + "model = stormpy.build_sparse_model_with_options(prism_program, options)\n", + "simulator = stormpy.simulator.create_simulator(model, seed=42)\n", + "simulator.set_action_mode(stormpy.simulator.SimulatorActionMode.GLOBAL_NAMES)\n", + "simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL)\n", + "# 3 paths of at most 20 steps.\n", + "paths = []\n", + "for m in range(3):\n", + " path = []\n", + " state, reward, labels = simulator.restart()\n", + " path = [f\"({state['x']},{state['y']})\"]\n", + " for n in range(20):\n", + " actions = simulator.available_actions()\n", + " select_action = random.randint(0,len(actions)-1)\n", + " path.append(f\"--{actions[select_action]}-->\")\n", + " state, reward, labels = simulator.step(actions[select_action])\n", + " path.append(f\"({state['x']},{state['y']})\")\n", + " if simulator.is_done():\n", + " break\n", + " paths.append(path)\n", + "for path in paths:\n", + " print(\" \".join(path))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Program-level simulator" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We can also use a program-level simulator, which does not require putting the model into memory." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "simulator = stormpy.simulator.create_simulator(prism_program, seed=42)" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(1,1) --south--> (1,1) --west--> (1,1) --west--> (1,2) --east--> (1,1) --west--> (1,2) --west--> (1,2) --west--> (1,2) --east--> (1,1) --south--> (1,1) --south--> (2,1) --south--> (3,1) --north--> (3,1) --west--> (3,1) --south--> (3,1) --west--> (3,1) --south--> (3,1) --south--> (4,1) --west--> (4,2) --east--> (4,1) --north--> (3,1)\n", + "(1,1) --west--> (1,1) --south--> (2,1) --west--> (2,2) --east--> (2,1) --west--> (2,2) --east--> (2,1) --north--> (2,1) --west--> (2,2) --north--> (1,2) --west--> (1,2) --west--> (1,3) --east--> (1,3) --west--> (1,4) --south--> (2,4) --north--> (1,4) --south--> (2,4) --north--> (1,4) --south--> (1,4) --south--> (1,4) --east--> (1,4)\n", + "(1,1) --south--> (2,1) --west--> (2,2) --east--> (2,1) --north--> (2,1) --north--> (2,1) --north--> (1,1) --west--> (1,2) --south--> (2,2) --west--> (2,3) --east--> (2,2) --east--> (2,1) --north--> (2,1) --west--> (2,2) --north--> (1,2) --west--> (1,2) --south--> (2,2) --west--> (2,2) --north--> (1,2) --east--> (1,2) --west--> (1,3)\n" + ] + } + ], + "source": [ + "# 3 paths of at most 20 steps.\n", + "paths = []\n", + "for m in range(3):\n", + " path = []\n", + " state, reward, labels = simulator.restart()\n", + " path = [f\"({state['x']},{state['y']})\"]\n", + " for n in range(20):\n", + " actions = simulator.available_actions()\n", + " select_action = random.randint(0,len(actions)-1)\n", + " path.append(f\"--{actions[select_action]}-->\")\n", + " state, reward, labels = simulator.step(actions[select_action])\n", + " path.append(f\"({state['x']},{state['y']})\")\n", + " if simulator.is_done():\n", + " break\n", + " paths.append(path)\n", + "for path in paths:\n", + " print(\" \".join(path))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "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.9.4" + } + }, + "nbformat": 4, + "nbformat_minor": 1 +} diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 7368dae316..d7e8167fbf 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -37,6 +37,8 @@ def _path(folder, file): """Prism example for parametric two dice""" prism_mdp_maze = _path("mdp", "maze_2.nm") """Prism example for the maze MDP""" +prism_mdp_slipgrid = _path("mdp", "slipgrid.nm") +"""Prism example for a slippery grid with fixed dimensions""" drn_pomdp_maze = _path("pomdp", "maze.drn") """DRN example for the maze POMDP""" prism_pomdp_maze = _path("pomdp", "maze_2.prism") diff --git a/lib/stormpy/examples/files/mdp/maze_2.nm b/lib/stormpy/examples/files/mdp/maze_2.nm index 215cac5c2a..3a8c4e4fde 100644 --- a/lib/stormpy/examples/files/mdp/maze_2.nm +++ b/lib/stormpy/examples/files/mdp/maze_2.nm @@ -1,6 +1,6 @@ -// maze example (POMDP) +// maze example (POMDP) as an MDP // slightly extends that presented in // Littman, Cassandra and Kaelbling // Learning policies for partially observable environments: Scaling up diff --git a/lib/stormpy/examples/files/mdp/slipgrid.nm b/lib/stormpy/examples/files/mdp/slipgrid.nm new file mode 100644 index 0000000000..b9d00a8824 --- /dev/null +++ b/lib/stormpy/examples/files/mdp/slipgrid.nm @@ -0,0 +1,29 @@ +mdp + +const double p = 0.4; +const int N = 4; +const int M = 4; + +module grid + x : [1..N] init 1; + y : [1..M] init 1; + [north] x > 1 -> 1-p: (x'=x-1) + p: (x'=x); + [south] x < N -> 1-p: (x'=x+1) + p: (x'=x); + [east] y > 1 -> 1-p: (y'=y-1) + p: (x'=x); + [west] y < M -> 1-p: (y'=y+1) + p: (x'=x); +endmodule + +// reward structure (number of steps to reach the target) +rewards + + [east] true : 1; + [west] true : 1; + [north] true : 1; + [south] true : 1; + +endrewards + +// target observation +label "goal" = x=N & y=M; + + diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py index 4d88ab0143..e6b6e0e206 100644 --- a/lib/stormpy/simulator.py +++ b/lib/stormpy/simulator.py @@ -13,7 +13,7 @@ class SimulatorActionMode(Enum): class Simulator: """ - Base class for simulators. + Abstract base class for simulators. """ def __init__(self, seed=None): self._seed = seed From c20112ac77ec55955fce7ab34111e061559de915 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 2 Jan 2024 21:22:28 +0100 Subject: [PATCH 02/11] some ADD support, improved valuation support, towards access for results of dd-based model checking --- src/core/result.cpp | 1 + src/storage/dd.cpp | 9 +++++++++ src/storage/expressions.cpp | 2 ++ src/storage/valuation.cpp | 5 ++++- 4 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/core/result.cpp b/src/core/result.cpp index 5757ee528f..8a633a21ee 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -90,6 +90,7 @@ void define_result(py::module& m) { ; py::class_, std::shared_ptr>>(m, "SymbolicQuantitativeCheckResult", "Symbolic quantitative model checking result", quantitativeCheckResult) .def("clone", [](storm::modelchecker::SymbolicQuantitativeCheckResult const& dd) {return dd.clone()->asSymbolicQuantitativeCheckResult(); }) + .def("get_values", &storm::modelchecker::SymbolicQuantitativeCheckResult::getValueVector); ; py::class_, std::shared_ptr>>(m, "HybridQuantitativeCheckResult", "Hybrid quantitative model checking result", quantitativeCheckResult) .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") diff --git a/src/storage/dd.cpp b/src/storage/dd.cpp index 9540aea5f2..dffd9aa790 100644 --- a/src/storage/dd.cpp +++ b/src/storage/dd.cpp @@ -3,6 +3,7 @@ #include "storm/storage/dd/DdMetaVariable.h" #include "storm/storage/dd/Dd.h" #include "storm/storage/dd/Bdd.h" +#include "storm/storage/dd/Add.h" #include "src/helpers.h" template @@ -26,6 +27,14 @@ void define_dd(py::module& m, std::string const& libstring) { py::class_> bdd(m, (std::string("Bdd_") + libstring).c_str(), "Bdd", dd); bdd.def("to_expression", &storm::dd::Bdd::toExpression, py::arg("expression_manager")); + + py::class_> add(m, (std::string("Add_") + libstring + "_Double").c_str(), "Add", dd); + add.def("__iter__", [](const storm::dd::Add &s) { return py::make_iterator(s.begin(), s.end()); }, + py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */); + + py::class_> addIterator(m, (std::string("AddIterator_") + libstring + "_Double").c_str(), "AddIterator"); + addIterator.def("get", [](const storm::dd::AddIterator &it) { return *it; } ); + } diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index 54c87224f8..6c36736952 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -34,6 +34,8 @@ void define_expressions(py::module& m) { py::class_>(m, "Variable", "Represents a variable") .def_property_readonly("name", &storm::expressions::Variable::getName, "Variable name") .def_property_readonly("manager", &storm::expressions::Variable::getManager, "Variable manager") + .def_property_readonly("index", &storm::expressions::Variable::getIndex, "Variable index") + .def_property_readonly("offset", &storm::expressions::Variable::getOffset, "Variable offset (used e.g., in dds)") .def("has_boolean_type", &storm::expressions::Variable::hasBooleanType, "Check if the variable is of boolean type") .def("has_integer_type", &storm::expressions::Variable::hasIntegerType, "Check if the variable is of integer type") .def("has_rational_type", &storm::expressions::Variable::hasRationalType, "Check if the variable is of rational type") diff --git a/src/storage/valuation.cpp b/src/storage/valuation.cpp index c55a67d689..e235f54f4a 100644 --- a/src/storage/valuation.cpp +++ b/src/storage/valuation.cpp @@ -41,8 +41,11 @@ void define_statevaluation(py::module& m) { } void define_simplevaluation(py::module& m) { - py::class_ sval(m, "SimpleValuation"); + py::class_ val(m, "Valuation"); + val.def_property_readonly("expression_manager", &storm::expressions::Valuation::getManager); + py::class_ sval(m, "SimpleValuation", val); sval.def("to_json", &storm::expressions::SimpleValuation::toJson, "Convert to JSON"); + sval.def("to_string", &storm::expressions::SimpleValuation::toString, py::arg("pretty")=true, "to string"); sval.def("get_boolean_value", &storm::expressions::SimpleValuation::getBooleanValue, py::arg("variable"), "Get Boolean Value for expression variable"); sval.def("get_integer_value", &storm::expressions::SimpleValuation::getIntegerValue, py::arg("variable"), "Get Integer Value for expression variable"); From a23b688449d8794e0f0e14e54dbf9bebcd361ddf Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 22 May 2024 22:55:06 +0200 Subject: [PATCH 03/11] rational function inclusion to reflect changes in main storm --- src/logic/formulae.cpp | 1 + src/storage/model.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index c0ad27dc29..a92f28d1e0 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -3,6 +3,7 @@ #include "storm/logic/CloneVisitor.h" #include "storm/logic/LabelSubstitutionVisitor.h" #include "storm/storage/expressions/Variable.h" +#include "storm/adapters/RationalNumberAdapter.h" void define_formulae(py::module& m) { diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 5f0f4777ea..e5bd5bab12 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -1,6 +1,7 @@ #include "model.h" #include "state.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/ModelBase.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" From f7fb78833e3803b41fe311cf1d30310fd200649e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 May 2024 17:03:17 +0200 Subject: [PATCH 04/11] recent changes in storm --- doc/source/doc/simulator.ipynb | 76 ---------------------- lib/stormpy/examples/files/mdp/slipgrid.nm | 3 - src/pomdp/quantitative_analysis.cpp | 2 + src/pomdp/tracker.cpp | 2 + 4 files changed, 4 insertions(+), 79 deletions(-) diff --git a/doc/source/doc/simulator.ipynb b/doc/source/doc/simulator.ipynb index ce64f17f00..8de0ed56b5 100644 --- a/doc/source/doc/simulator.ipynb +++ b/doc/source/doc/simulator.ipynb @@ -3,10 +3,6 @@ { "cell_type": "markdown", "metadata": { -<<<<<<< HEAD -======= - "collapsed": true, ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "pycharm": { "name": "#%%md\n" } @@ -17,15 +13,9 @@ "The simulators in stormpy are meant to mimic access to unknown models,\n", "but they can also be used to explore the model.\n", "\n", -<<<<<<< HEAD "All simulators implement the abstract class `stormpy.simulator.Simulator`. \n", "\n", "The simulators differ in the model representation they use in the background and in the representation of the states and actions exposed to the user. We will go through some options by example!\n" -======= - "All simulators implement the abstract class stormpy.simulator.Simulator. \n", - "\n", - "The different simulators are different in the model representation they use in the background and in the representation of the states and actions exposed to the user. We will go through some options by example!\n" ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 ] }, { @@ -235,11 +225,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ -<<<<<<< HEAD "Indeed, we are not leaving the state. In this case, we can never leave the state as state s11 is absorbing. The simulator detects and exposes this information via `simulator.is_done()`" -======= - "Indeed, we are not leaving the state, in this case, we can never leave the state as state s11 is absorbing. The simulator detects and exposes this information via `simulator.is_done()`" ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 ] }, { @@ -328,11 +314,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ -<<<<<<< HEAD "Then, we create simulator that uses program-level state observations." -======= - "Then, we can create simulator that uses program-level state observations." ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 ] }, { @@ -445,53 +427,33 @@ }, { "cell_type": "code", -<<<<<<< HEAD "execution_count": 16, "metadata": { "tags": [] }, -======= - "execution_count": 18, - "metadata": {}, ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ -<<<<<<< HEAD "0 --act=1--> 2 --act=0--> 2 --act=0--> 4 --act=2--> 1 --act=1--> 3 --act=1--> 3 --act=2--> 7 --act=2--> 3 --act=0--> 1 --act=2--> 4 --act=1--> 4 --act=2--> 4 --act=3--> 8 --act=0--> 5 --act=0--> 8 --act=3--> 12 --act=0--> 12 --act=0--> 9 --act=0--> 9 --act=1--> 5\n", "------\n", "0 --act=1--> 0 --act=0--> 0 --act=1--> 2 --act=1--> 0 --act=0--> 0 --act=0--> 1 --act=0--> 0 --act=1--> 2 --act=2--> 5 --act=0--> 8 --act=1--> 11 --act=2--> 7 --act=2--> 3 --act=2--> 7 --act=2--> 3 --act=2--> 3 --act=1--> 3 --act=2--> 3 --act=0--> 1 --act=1--> 3\n", "------\n", "0 --act=0--> 1 --act=2--> 4 --act=3--> 4 --act=3--> 4 --act=1--> 4 --act=1--> 7 --act=1--> 10 --act=2--> 10 --act=1--> 6 --act=0--> 3 --act=2--> 7 --act=0--> 4 --act=0--> 2 --act=0--> 4 --act=3--> 8 --act=0--> 5 --act=2--> 9 --act=1--> 5 --act=2--> 9 --act=1--> 9\n", -======= - "0 --act=1--> 2 --act=2--> 2 --act=2--> 5 --act=2--> 9 --act=0--> 12 --act=1--> 12 --act=0--> 9 --act=1--> 5 --act=2--> 5 --act=0--> 8 --act=3--> 8 --act=3--> 12 --act=1--> 14 --act=1--> 14 --act=2--> 14 --act=1--> 15 --act=0--> 15 --act=0--> 14 --act=1--> 14 --act=0--> 12\n", - "------\n", - "0 --act=0--> 0 --act=0--> 0 --act=1--> 2 --act=0--> 2 --act=0--> 2 --act=2--> 5 --act=2--> 5 --act=0--> 8 --act=0--> 5 --act=2--> 9 --act=1--> 9 --act=0--> 12 --act=0--> 9 --act=1--> 9 --act=1--> 5 --act=0--> 5 --act=1--> 2 --act=2--> 2 --act=0--> 2 --act=1--> 2\n", - "------\n", - "0 --act=1--> 2 --act=1--> 2 --act=2--> 2 --act=0--> 2 --act=0--> 2 --act=0--> 4 --act=3--> 8 --act=2--> 4 --act=1--> 7 --act=1--> 7 --act=2--> 7 --act=3--> 11 --act=2--> 7 --act=1--> 10 --act=0--> 10 --act=1--> 6 --act=1--> 10 --act=0--> 7 --act=0--> 7 --act=1--> 10\n", ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "------\n" ] } ], "source": [ "import random\n", -<<<<<<< HEAD "random.seed(23)\n", -======= ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "path = stormpy.examples.files.prism_mdp_slipgrid\n", "prism_program = stormpy.parse_prism_program(path)\n", "\n", "model = stormpy.build_model(prism_program)\n", "simulator = stormpy.simulator.create_simulator(model, seed=42)\n", -<<<<<<< HEAD "# 3 paths of at most 20 steps.\n", -======= - "# 5 paths of at most 20 steps.\n", ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "paths = []\n", "for m in range(3):\n", " path = []\n", @@ -520,11 +482,7 @@ }, { "cell_type": "code", -<<<<<<< HEAD "execution_count": 17, -======= - "execution_count": 25, ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "metadata": { "scrolled": true }, @@ -533,15 +491,9 @@ "name": "stdout", "output_type": "stream", "text": [ -<<<<<<< HEAD "(1,1) --west--> (1,2) --south--> (1,2) --east--> (1,2) --east--> (1,1) --west--> (1,2) --east--> (1,1) --south--> (2,1) --south--> (2,1) --north--> (1,1) --south--> (2,1) --west--> (2,1) --north--> (2,1) --west--> (2,2) --west--> (2,2) --south--> (3,2) --east--> (3,2) --south--> (4,2) --west--> (4,2) --west--> (4,2) --north--> (3,2)\n", "(1,1) --west--> (1,1) --south--> (1,1) --west--> (1,2) --south--> (1,2) --south--> (1,2) --west--> (1,3) --east--> (1,2) --east--> (1,2) --south--> (2,2) --south--> (3,2) --south--> (4,2) --west--> (4,3) --north--> (3,3) --south--> (4,3) --west--> (4,4) --north--> (3,4) --east--> (3,3) --west--> (3,3) --north--> (2,3) --east--> (2,3)\n", "(1,1) --south--> (2,1) --south--> (3,1) --south--> (3,1) --north--> (2,1) --north--> (1,1) --south--> (2,1) --south--> (3,1) --south--> (3,1) --west--> (3,2) --south--> (3,2) --west--> (3,3) --east--> (3,2) --south--> (3,2) --north--> (3,2) --north--> (3,2) --south--> (3,2) --south--> (4,2) --east--> (4,1) --north--> (4,1) --west--> (4,2)\n" -======= - "(1,1) --south--> (2,1) --south--> (2,1) --west--> (2,2) --north--> (1,2) --east--> (1,1) --south--> (1,1) --south--> (2,1) --west--> (2,1) --west--> (2,1) --west--> (2,2) --east--> (2,1) --west--> (2,2) --north--> (2,2) --north--> (1,2) --south--> (2,2) --east--> (2,2) --east--> (2,2) --south--> (2,2) --west--> (2,2) --south--> (3,2)\n", - "(1,1) --south--> (1,1) --west--> (1,1) --south--> (2,1) --north--> (1,1) --west--> (1,1) --west--> (1,2) --south--> (1,2) --south--> (2,2) --south--> (3,2) --west--> (3,3) --south--> (4,3) --east--> (4,2) --north--> (3,2) --north--> (3,2) --south--> (4,2) --north--> (3,2) --east--> (3,1) --north--> (2,1) --north--> (1,1) --south--> (2,1)\n", - "(1,1) --west--> (1,2) --east--> (1,2) --south--> (1,2) --south--> (1,2) --west--> (1,2) --south--> (2,2) --south--> (3,2) --north--> (2,2) --north--> (1,2) --west--> (1,2) --east--> (1,2) --east--> (1,1) --west--> (1,1) --south--> (2,1) --south--> (3,1) --north--> (2,1) --west--> (2,2) --north--> (1,2) --west--> (1,3) --east--> (1,3)\n" ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 ] } ], @@ -588,11 +540,7 @@ }, { "cell_type": "code", -<<<<<<< HEAD "execution_count": 18, -======= - "execution_count": null, ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "metadata": {}, "outputs": [], "source": [ @@ -601,26 +549,16 @@ }, { "cell_type": "code", -<<<<<<< HEAD "execution_count": 19, -======= - "execution_count": 27, ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ -<<<<<<< HEAD "(1,1) --0--> (2,1) --0--> (1,1) --1--> (1,2) --1--> (1,1) --1--> (1,2) --0--> (2,2) --3--> (2,3) --0--> (1,3) --2--> (1,3) --2--> (1,4) --0--> (2,4) --2--> (2,3) --2--> (2,2) --3--> (2,2) --3--> (2,3) --2--> (2,2) --0--> (2,2) --2--> (2,2) --0--> (1,2) --0--> (2,2)\n", "(1,1) --0--> (2,1) --1--> (2,1) --2--> (2,2) --3--> (2,2) --1--> (2,2) --1--> (3,2) --0--> (2,2) --2--> (2,1) --2--> (2,2) --0--> (2,2) --1--> (3,2) --3--> (3,3) --3--> (3,3) --2--> (3,2) --0--> (2,2) --2--> (2,2) --3--> (2,2) --0--> (1,2) --0--> (2,2) --3--> (2,3)\n", "(1,1) --0--> (2,1) --2--> (2,2) --0--> (1,2) --0--> (2,2) --3--> (2,2) --3--> (2,3) --0--> (1,3) --1--> (1,3) --2--> (1,4) --1--> (1,4) --1--> (1,3) --2--> (1,4) --0--> (2,4) --2--> (2,3) --2--> (2,2) --2--> (2,2) --0--> (1,2) --0--> (2,2) --0--> (2,2) --3--> (2,3)\n" -======= - "(1,1) --south--> (1,1) --west--> (1,1) --west--> (1,2) --east--> (1,1) --west--> (1,2) --west--> (1,2) --west--> (1,2) --east--> (1,1) --south--> (1,1) --south--> (2,1) --south--> (3,1) --north--> (3,1) --west--> (3,1) --south--> (3,1) --west--> (3,1) --south--> (3,1) --south--> (4,1) --west--> (4,2) --east--> (4,1) --north--> (3,1)\n", - "(1,1) --west--> (1,1) --south--> (2,1) --west--> (2,2) --east--> (2,1) --west--> (2,2) --east--> (2,1) --north--> (2,1) --west--> (2,2) --north--> (1,2) --west--> (1,2) --west--> (1,3) --east--> (1,3) --west--> (1,4) --south--> (2,4) --north--> (1,4) --south--> (2,4) --north--> (1,4) --south--> (1,4) --south--> (1,4) --east--> (1,4)\n", - "(1,1) --south--> (2,1) --west--> (2,2) --east--> (2,1) --north--> (2,1) --north--> (2,1) --north--> (1,1) --west--> (1,2) --south--> (2,2) --west--> (2,3) --east--> (2,2) --east--> (2,1) --north--> (2,1) --west--> (2,2) --north--> (1,2) --west--> (1,2) --south--> (2,2) --west--> (2,2) --north--> (1,2) --east--> (1,2) --west--> (1,3)\n" ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 ] } ], @@ -643,16 +581,6 @@ "for path in paths:\n", " print(\" \".join(path))" ] -<<<<<<< HEAD -======= - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 } ], "metadata": { @@ -675,9 +603,5 @@ } }, "nbformat": 4, -<<<<<<< HEAD "nbformat_minor": 4 -======= - "nbformat_minor": 1 ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 } diff --git a/lib/stormpy/examples/files/mdp/slipgrid.nm b/lib/stormpy/examples/files/mdp/slipgrid.nm index e73354b42b..ebd3f26286 100644 --- a/lib/stormpy/examples/files/mdp/slipgrid.nm +++ b/lib/stormpy/examples/files/mdp/slipgrid.nm @@ -24,10 +24,7 @@ rewards endrewards // target observation -<<<<<<< HEAD label "target" = x=3 & y=3; -======= ->>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761 label "goal" = x=N & y=M; diff --git a/src/pomdp/quantitative_analysis.cpp b/src/pomdp/quantitative_analysis.cpp index 87b2906678..eec6cb5ff8 100644 --- a/src/pomdp/quantitative_analysis.cpp +++ b/src/pomdp/quantitative_analysis.cpp @@ -1,4 +1,6 @@ #include "quantitative_analysis.h" + +#include #include #include diff --git a/src/pomdp/tracker.cpp b/src/pomdp/tracker.cpp index 3e072dbefe..11740e2b98 100644 --- a/src/pomdp/tracker.cpp +++ b/src/pomdp/tracker.cpp @@ -1,5 +1,7 @@ #include "tracker.h" #include "src/helpers.h" + +#include #include #include From 0e5d223704c13e3bd09f613215c81a12a1ccb3dc Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 25 Sep 2024 20:40:16 +0200 Subject: [PATCH 05/11] relreach v1 --- examples/analysis/05-analysis.py | 23 ++++ lib/stormpy/examples/files.py | 3 + .../examples/files/mdp/maze_2_multigoal.nm | 128 ++++++++++++++++++ src/core/multiobjective.cpp | 53 ++++++++ src/core/multiobjective.h | 5 + src/mod_core.cpp | 2 + 6 files changed, 214 insertions(+) create mode 100644 lib/stormpy/examples/files/mdp/maze_2_multigoal.nm create mode 100644 src/core/multiobjective.cpp create mode 100644 src/core/multiobjective.h diff --git a/examples/analysis/05-analysis.py b/examples/analysis/05-analysis.py index e69de29bb2..db1fc997a5 100644 --- a/examples/analysis/05-analysis.py +++ b/examples/analysis/05-analysis.py @@ -0,0 +1,23 @@ +import stormpy + +import stormpy.examples +import stormpy.examples.files + + +def example_analysis_05(): + path = stormpy.examples.files.prism_mdp_maze_multigoal + prism_program = stormpy.parse_prism_program(path) + + formula_str = "multi(Pmax=? [F \"goalalt1\"], Pmax=? [F \"goalalt2\"])" + properties = stormpy.parse_properties(formula_str, prism_program) + + options = stormpy.BuilderOptions([p.raw_formula for p in properties]) + options.set_build_state_valuations() + model = stormpy.build_sparse_model_with_options(prism_program, options) + env = stormpy.Environment() + lower_bound, upper_bound = stormpy.compute_rel_reach_helper(env, model, properties[0].raw_formula) + print(lower_bound) + print(upper_bound) + +if __name__ == '__main__': + example_analysis_05() diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 8b75d02479..a94144ffef 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -36,6 +36,8 @@ def _path(folder, file): prism_pmdp_coin_two_dice = _path("pmdp", "two_dice.nm") """Prism example for parametric two dice""" prism_mdp_maze = _path("mdp", "maze_2.nm") +"""""" +prism_mdp_maze_multigoal = _path("mdp", "maze_2_multigoal.nm") """Prism example for the maze MDP""" prism_mdp_slipgrid = _path("mdp", "slipgrid.nm") """Prism example for the maze MDP towards sketching""" @@ -55,3 +57,4 @@ def _path(folder, file): """GSPN example (PNPRO format)""" gspn_pnml_simple = _path("gspn", "gspn_simple.pnml") """GSPN example (PNML format)""" + diff --git a/lib/stormpy/examples/files/mdp/maze_2_multigoal.nm b/lib/stormpy/examples/files/mdp/maze_2_multigoal.nm new file mode 100644 index 0000000000..305ac06d16 --- /dev/null +++ b/lib/stormpy/examples/files/mdp/maze_2_multigoal.nm @@ -0,0 +1,128 @@ + + +// maze example (POMDP) as an MDP +// slightly extends that presented in +// Littman, Cassandra and Kaelbling +// Learning policies for partially observable environments: Scaling up +// Technical Report CS, Brown University +// gxn 29/01/16 +// Made into a MDP for documentation of stormpy. + +// state space (value of variable "s") + +// 0 1 2 3 4 +// 5 6 7 +// 8 9 10 +// 11 13 12 + +// 13 is the target + +mdp + + +module maze + + s : [-1..13]; + + // initialisation + [] s=-1 -> 1/11 : (s'=0) + + 1/11 : (s'=1) + + 1/11 : (s'=2) + + 1/11 : (s'=3) + + 1/11 : (s'=4) + + 1/11 : (s'=5) + + 1/11 : (s'=6) + + 1/11 : (s'=7) + + 1/11 : (s'=8) + + 1/11 : (s'=9) + + 1/11 : (s'=10); + + // moving around the maze + + [east] s=0 -> (s'=1); + [west] s=0 -> (s'=0); + [north] s=0 -> (s'=0); + [south] s=0 -> (s'=5); + + [east] s=1 -> (s'=2); + [west] s=1 -> (s'=0); + [north] s=1 -> (s'=1); + [south] s=1 -> (s'=1); + + [east] s=2 -> (s'=3); + [west] s=2 -> (s'=1); + [north] s=2 -> (s'=2); + [south] s=2 -> (s'=6); + + [east] s=3 -> (s'=4); + [west] s=3 -> (s'=2); + [north] s=3 -> (s'=3); + [south] s=3 -> (s'=3); + + [east] s=4 -> (s'=4); + [west] s=4 -> (s'=3); + [north] s=4 -> (s'=4); + [south] s=4 -> (s'=7); + + [east] s=5 -> (s'=5); + [west] s=5 -> (s'=5); + [north] s=5 -> (s'=0); + [south] s=5 -> (s'=8); + + [east] s=6 -> (s'=6); + [west] s=6 -> (s'=6); + [north] s=6 -> (s'=2); + [south] s=6 -> (s'=9); + + [east] s=7 -> (s'=7); + [west] s=7 -> (s'=7); + [north] s=7 -> (s'=4); + [south] s=7 -> (s'=10); + + [east] s=8 -> (s'=8); + [west] s=8 -> (s'=8); + [north] s=8 -> (s'=5); + [south] s=8 -> (s'=11); + + [east] s=9 -> (s'=9); + [west] s=9 -> (s'=9); + [north] s=9 -> (s'=6); + [south] s=9 -> (s'=13); + + [east] s=10 -> (s'=10); + [west] s=10 -> (s'=10); + [north] s=10 -> (s'=7); + [south] s=10 -> (s'=12); + + [east] s=11 -> (s'=11); + [west] s=11 -> (s'=11); + [north] s=11 -> (s'=8); + [south] s=11 -> (s'=11); + + [east] s=12 -> (s'=12); + [west] s=12 -> (s'=12); + [north] s=12 -> (s'=10); + [south] s=12 -> (s'=12); + + // loop when we reach the target + [done] s=13 -> true; + +endmodule + +// reward structure (number of steps to reach the target) +rewards + + [east] true : 1; + [west] true : 1; + [north] true : 1; + [south] true : 1; + +endrewards + +// target observation +label "goal" = s=13; +label "goalalt1" = s=11; +label "goalalt2" = s=12; + + + diff --git a/src/core/multiobjective.cpp b/src/core/multiobjective.cpp new file mode 100644 index 0000000000..8081a655bb --- /dev/null +++ b/src/core/multiobjective.cpp @@ -0,0 +1,53 @@ +#include "multiobjective.h" + +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" + +#include "storm/environment/Environment.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" +#include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h" +#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h" +#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h" +#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" +#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" +#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" +#include "storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/InvalidEnvironmentException.h" + + +std::pair _checkForRelReach(storm::Environment const& env, storm::models::sparse::Mdp const& model, + storm::logic::MultiObjectiveFormula const& formula) { + // This internal check for RelReach requires some cleanup before it makes sense to merge this. + // STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, + // "Multi-objective Model checking on model with multiple initial states is not supported."); + std::vector weightVector = {1.0,-1.0}; + // Preprocess the model + auto preprocessorResult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, model, formula); + auto checker = storm::modelchecker::multiobjective::StandardMdpPcaaWeightVectorChecker(preprocessorResult); + checker.check(env, weightVector); + double underApprox = checker.getUnderApproximationOfInitialStateResults().at(0); + double overApprox = checker.getOverApproximationOfInitialStateResults().at(0); +// +// /*! +// * Retrieves a scheduler that induces the current values +// * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. +// * Also note that (currently) the scheduler only supports unbounded objectives. +// */ +// virtual storm::storage::Scheduler computeScheduler() const override; + return {underApprox, overApprox}; +} + + +// Define python bindings +void define_multiobjective(py::module& m) { + m.def("compute_rel_reach_helper", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula")); +} \ No newline at end of file diff --git a/src/core/multiobjective.h b/src/core/multiobjective.h new file mode 100644 index 0000000000..f355c182bb --- /dev/null +++ b/src/core/multiobjective.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_multiobjective(py::module& m); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index f2d060aeb5..e86a16b47e 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -3,6 +3,7 @@ #include "core/core.h" #include "core/result.h" #include "core/modelchecking.h" +#include "core/multiobjective.h" #include "core/bisimulation.h" #include "core/input.h" #include "core/analysis.h" @@ -29,6 +30,7 @@ PYBIND11_MODULE(core, m) { define_export(m); define_result(m); define_modelchecking(m); + define_multiobjective(m); define_counterexamples(m); define_bisimulation(m); define_input(m); From 4e292530c985d4b3a2ecfe08b680866cf2eb0272 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 14 Jan 2025 00:02:35 +0100 Subject: [PATCH 06/11] update multiobjective with fix and exact --- examples/analysis/05-analysis.py | 12 ++++++++++-- src/core/multiobjective.cpp | 16 ++++++++++------ 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/examples/analysis/05-analysis.py b/examples/analysis/05-analysis.py index db1fc997a5..4a33811934 100644 --- a/examples/analysis/05-analysis.py +++ b/examples/analysis/05-analysis.py @@ -5,6 +5,7 @@ def example_analysis_05(): + exact = True path = stormpy.examples.files.prism_mdp_maze_multigoal prism_program = stormpy.parse_prism_program(path) @@ -13,9 +14,16 @@ def example_analysis_05(): options = stormpy.BuilderOptions([p.raw_formula for p in properties]) options.set_build_state_valuations() - model = stormpy.build_sparse_model_with_options(prism_program, options) env = stormpy.Environment() - lower_bound, upper_bound = stormpy.compute_rel_reach_helper(env, model, properties[0].raw_formula) + + if exact: + env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.eigen) + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.policy_iteration + model = stormpy.build_sparse_exact_model_with_options(prism_program, options) + lower_bound, upper_bound = stormpy.compute_rel_reach_helper_exact(env, model, properties[0].raw_formula) + else: + model = stormpy.build_sparse_model_with_options(prism_program, options) + lower_bound, upper_bound = stormpy.compute_rel_reach_helper(env, model, properties[0].raw_formula) print(lower_bound) print(upper_bound) diff --git a/src/core/multiobjective.cpp b/src/core/multiobjective.cpp index 8081a655bb..1cfa9b586f 100644 --- a/src/core/multiobjective.cpp +++ b/src/core/multiobjective.cpp @@ -2,6 +2,7 @@ #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/environment/Environment.h" #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h" @@ -24,18 +25,20 @@ #include "storm/exceptions/InvalidEnvironmentException.h" -std::pair _checkForRelReach(storm::Environment const& env, storm::models::sparse::Mdp const& model, +template +std::pair _checkForRelReach(storm::Environment const& env, storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula) { // This internal check for RelReach requires some cleanup before it makes sense to merge this. // STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, // "Multi-objective Model checking on model with multiple initial states is not supported."); - std::vector weightVector = {1.0,-1.0}; + std::vector weightVector = {storm::utility::one(),-storm::utility::one()}; // Preprocess the model - auto preprocessorResult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, model, formula); + auto preprocessorResult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, model, formula); auto checker = storm::modelchecker::multiobjective::StandardMdpPcaaWeightVectorChecker(preprocessorResult); checker.check(env, weightVector); - double underApprox = checker.getUnderApproximationOfInitialStateResults().at(0); - double overApprox = checker.getOverApproximationOfInitialStateResults().at(0); + ValueType underApprox = checker.getUnderApproximationOfInitialStateResults().at(0) - checker.getOverApproximationOfInitialStateResults().at(1); + ValueType overApprox = checker.getOverApproximationOfInitialStateResults().at(0) - checker.getUnderApproximationOfInitialStateResults().at(1); + // // /*! // * Retrieves a scheduler that induces the current values @@ -49,5 +52,6 @@ std::pair _checkForRelReach(storm::Environment const& env, storm // Define python bindings void define_multiobjective(py::module& m) { - m.def("compute_rel_reach_helper", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula")); + m.def("compute_rel_reach_helper", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula")); + m.def("compute_rel_reach_helper_exact", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula")); } \ No newline at end of file From 4e8c0a64d756c360b326323e31d1b92530150583 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 14 Jan 2025 22:17:30 +0100 Subject: [PATCH 07/11] force exact added --- src/core/environment.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/environment.cpp b/src/core/environment.cpp index 9fa4f06af5..e89007057c 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -43,6 +43,7 @@ void define_environment(py::module& m) { py::class_(m, "SolverEnvironment", "Environment for solvers") .def("set_force_sound", &storm::SolverEnvironment::setForceSoundness, "force soundness", py::arg("new_value") = true) + .def("set_force_exact", &storm::SolverEnvironment::setForceExact, "force exact solving", py::arg("new_value") = true) .def("set_linear_equation_solver_type", &storm::SolverEnvironment::setLinearEquationSolverType, "set solver type to use", py::arg("new_value"), py::arg("set_from_default") = false) .def_property_readonly("minmax_solver_environment", [](storm::SolverEnvironment& senv) -> auto& { return senv.minMax(); }) .def_property_readonly("native_solver_environment", [](storm::SolverEnvironment& senv) -> auto& {return senv.native(); }) From e344a5499f5836fb25ad0edd8705626548bd247d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 15 Mar 2025 22:03:07 +0100 Subject: [PATCH 08/11] update for relreach --- src/core/multiobjective.cpp | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) diff --git a/src/core/multiobjective.cpp b/src/core/multiobjective.cpp index 1cfa9b586f..9efd24e408 100644 --- a/src/core/multiobjective.cpp +++ b/src/core/multiobjective.cpp @@ -17,6 +17,7 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/settings/SettingsManager.h" +#include "storm/storage/SparseMatrix.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/utility/Stopwatch.h" #include "storm/utility/macros.h" @@ -25,9 +26,9 @@ #include "storm/exceptions/InvalidEnvironmentException.h" -template -std::pair _checkForRelReach(storm::Environment const& env, storm::models::sparse::Mdp const& model, - storm::logic::MultiObjectiveFormula const& formula) { +template +std::tuple> _checkForRelReach(storm::Environment const& env, storm::models::sparse::Mdp const& model, + storm::logic::MultiObjectiveFormula const& formula, bool computeScheduler) { // This internal check for RelReach requires some cleanup before it makes sense to merge this. // STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, // "Multi-objective Model checking on model with multiple initial states is not supported."); @@ -38,20 +39,15 @@ std::pair _checkForRelReach(storm::Environment const& env, checker.check(env, weightVector); ValueType underApprox = checker.getUnderApproximationOfInitialStateResults().at(0) - checker.getOverApproximationOfInitialStateResults().at(1); ValueType overApprox = checker.getOverApproximationOfInitialStateResults().at(0) - checker.getUnderApproximationOfInitialStateResults().at(1); - -// -// /*! -// * Retrieves a scheduler that induces the current values -// * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. -// * Also note that (currently) the scheduler only supports unbounded objectives. -// */ -// virtual storm::storage::Scheduler computeScheduler() const override; - return {underApprox, overApprox}; + if (computeScheduler) { + return {underApprox, overApprox, checker.computeScheduler()}; + } else { + return {underApprox, overApprox, storm::storage::Scheduler(0)}; + } } - // Define python bindings void define_multiobjective(py::module& m) { - m.def("compute_rel_reach_helper", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula")); - m.def("compute_rel_reach_helper_exact", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula")); + m.def("compute_rel_reach_helper", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); + m.def("compute_rel_reach_helper_exact", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); } \ No newline at end of file From b098c78110ef12bf90d5d987f17a4d8f48bd9902 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 26 Feb 2026 12:37:51 +0100 Subject: [PATCH 09/11] Adaption to changes in DirectEncodingExporter --- examples/pomdp/01-pomdps.py | 2 +- lib/stormpy/__init__.py | 4 ++-- src/core/core.cpp | 24 ++++++++++++------------ 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/examples/pomdp/01-pomdps.py b/examples/pomdp/01-pomdps.py index e1a7082569..87c1210351 100644 --- a/examples/pomdp/01-pomdps.py +++ b/examples/pomdp/01-pomdps.py @@ -67,7 +67,7 @@ def example_pomdps_01(): export_pmc = False # Set to True to export the pMC as drn. if export_pmc: - export_options = stormpy.DirectEncodingOptions() + export_options = stormpy.DirectEncodingExporterOptions() export_options.allow_placeholders = False stormpy.export_to_drn(pmc, "test.out", export_options) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index f50287bcb1..1b66b0bf86 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -712,12 +712,12 @@ def parse_properties(properties, context=None, filters=None): raise stormpy.exceptions.StormError("Unclear context. Please pass a symbolic model description") -def export_to_drn(model, file, options=DirectEncodingOptions()): +def export_to_drn(model, file, options=DirectEncodingExporterOptions()): """ Export a model to DRN format :param model: The model :param file: A path - :param options: DirectEncodingOptions + :param options: DirectEncodingExporterOptions :return: """ if model.supports_parameters: diff --git a/src/core/core.cpp b/src/core/core.cpp index 00e4494e77..b93e53f1b2 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -192,21 +192,21 @@ void define_optimality_type(py::module& m) { // Thin wrapper for exporting model template -void exportDRN(std::shared_ptr> model, std::string const& file, storm::io::DirectEncodingOptions options) { - std::ofstream stream; - storm::io::openFile(file, stream); - storm::io::explicitExportSparseModel(stream, model, {}, options); - storm::io::closeFile(stream); +void exportDRN(std::shared_ptr> model, std::string const& file, storm::io::DirectEncodingExporterOptions options) { + storm::api::exportSparseModelAsDrn(model, file, options); } void define_export(py::module& m) { - py::class_ opts(m, "DirectEncodingOptions"); - opts.def(py::init<>()); - opts.def_readwrite("allow_placeholders", &storm::io::DirectEncodingOptions::allowPlaceholders); + py::class_(m, "DirectEncodingExporterOptions") + .def(py::init<>()) + .def_readwrite("allow_placeholders", &storm::io::DirectEncodingExporterOptions::allowPlaceholders) + .def_readwrite("outputPrecision", &storm::io::DirectEncodingExporterOptions::outputPrecision) + ; + // Export - m.def("_export_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingOptions()); - m.def("_export_to_drn_interval", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingOptions()); - m.def("_export_exact_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingOptions()); - m.def("_export_parametric_to_drn", &exportDRN, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingOptions()); + m.def("_export_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); + m.def("_export_to_drn_interval", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); + m.def("_export_exact_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); + m.def("_export_parametric_to_drn", &exportDRN, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); } From f150926cc620b7ccfb21fcf1d2488da3d6c75c75 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 9 Mar 2026 22:22:37 +0100 Subject: [PATCH 10/11] intermediate-commit --- src/core/multiobjective.cpp | 75 +++++++++++++------------------ src/core/multiobjective.h | 3 +- src/mod_core.cpp | 3 +- src/storage/memorystructure.cpp | 2 + tests/core/test_multiobjective.py | 31 ++++++++++++- 5 files changed, 66 insertions(+), 48 deletions(-) diff --git a/src/core/multiobjective.cpp b/src/core/multiobjective.cpp index 9efd24e408..8736d7d39d 100644 --- a/src/core/multiobjective.cpp +++ b/src/core/multiobjective.cpp @@ -1,53 +1,38 @@ #include "multiobjective.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" - -#include "storm/adapters/RationalNumberAdapter.h" -#include "storm/environment/Environment.h" -#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" -#include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h" -#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h" -#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" -#include "storm/modelchecker/multiobjective/pcaa/StandardMdpPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h" -#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/settings/SettingsManager.h" -#include "storm/storage/SparseMatrix.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/utility/Stopwatch.h" #include "storm/utility/macros.h" - -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/exceptions/InvalidEnvironmentException.h" - - -template -std::tuple> _checkForRelReach(storm::Environment const& env, storm::models::sparse::Mdp const& model, - storm::logic::MultiObjectiveFormula const& formula, bool computeScheduler) { - // This internal check for RelReach requires some cleanup before it makes sense to merge this. - // STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, - // "Multi-objective Model checking on model with multiple initial states is not supported."); - std::vector weightVector = {storm::utility::one(),-storm::utility::one()}; - // Preprocess the model - auto preprocessorResult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, model, formula); - auto checker = storm::modelchecker::multiobjective::StandardMdpPcaaWeightVectorChecker(preprocessorResult); - checker.check(env, weightVector); - ValueType underApprox = checker.getUnderApproximationOfInitialStateResults().at(0) - checker.getOverApproximationOfInitialStateResults().at(1); - ValueType overApprox = checker.getOverApproximationOfInitialStateResults().at(0) - checker.getUnderApproximationOfInitialStateResults().at(1); - if (computeScheduler) { - return {underApprox, overApprox, checker.computeScheduler()}; - } else { - return {underApprox, overApprox, storm::storage::Scheduler(0)}; - } +#include "storm/environment/Environment.h" +// +//// Helper class to avoid that we also need to bind the preprocessing. +template +std::unique_ptr>> makeWeightedObjectiveMDPModelChecker(storm::Environment const& env, storm::models::sparse::Mdp const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, bool produceScheduler) { +// auto const preprocessresult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, originalModel, originalFormula, produceScheduler); +// return storm::modelchecker::multiobjective::createWeightVectorChecker(preprocessresult); } - -// Define python bindings -void define_multiobjective(py::module& m) { - m.def("compute_rel_reach_helper", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); - m.def("compute_rel_reach_helper_exact", &_checkForRelReach, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); -} \ No newline at end of file +// +// +//// Define python bindings +template +void define_multiobjective(py::module& m, std::string const& vtSuffix) { +// m.def(("_weighted_objective_mdp_model_checker_preprocess" + vtSuffix).c_str(), &makeWeightedObjectiveMDPModelChecker, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); +// m.def("_create_weighted_objective_mdp_model_checker") +// +// using PcaaPreprocessorResult = storm::modelchecker::multiobjective::PcaaPreprocessorResult +// using PcaaWeightVectorChecker = storm::modelchecker::multiobjective::PcaaWeightVectorChecker>; +// py::class_< +// py::class_> weightedObjectiveMdpModelChecker(m, ("WeightedObjectiveMdpModelChecker" + vtSuffix).c_str()); +// weightedObjectiveMdpModelChecker.def("check", &PcaaWeightVectorChecker::check, py::arg("env"), py::arg("weight_vector")) +// .def("get_achievable_point", &PcaaWeightVectorChecker::getAchievablePoint) +// .def("get_optimal_weighted_sum", &PcaaWeightVectorChecker::getOptimalWeightedSum, "Note that this sum can be hard to interpret whenever one mixes minimization and maximization objectives.") +// .def("compute_scheduler", &PcaaWeightVectorChecker::computeScheduler, "Note that this is a scheduler on the preprocessed MDP") +// .def("set_weighted_precision", &PcaaWeightVectorChecker::setWeightedPrecision, py::arg("value"), "A smaller value means a higher precision."); +} +// +template void define_multiobjective(py::module&, std::string const&); +template void define_multiobjective(py::module&, std::string const&); \ No newline at end of file diff --git a/src/core/multiobjective.h b/src/core/multiobjective.h index f355c182bb..db4229da2d 100644 --- a/src/core/multiobjective.h +++ b/src/core/multiobjective.h @@ -2,4 +2,5 @@ #include "common.h" -void define_multiobjective(py::module& m); +template +void define_multiobjective(py::module& m, std::string const& vtSuffix); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index 20481304b0..5fc021d6e3 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -33,7 +33,8 @@ PYBIND11_MODULE(_core, m) { define_check_task(m, "ExactCheckTask"); define_check_task(m, "ParametricCheckTask"); define_modelchecking(m); - define_multiobjective(m); + define_multiobjective(m, "Double"); + define_multiobjective(m, "Exact"); define_counterexamples(m); define_bisimulation(m); define_input(m); diff --git a/src/storage/memorystructure.cpp b/src/storage/memorystructure.cpp index d6b1f814d8..d669c149fd 100644 --- a/src/storage/memorystructure.cpp +++ b/src/storage/memorystructure.cpp @@ -15,6 +15,8 @@ void define_memorystructure_untyped(py::module& m) { memoryStructure.def("_product_model_parametric", [](MemoryStructure& ms, storm::models::sparse::Model const& sparseModel) {return ms.product(sparseModel);}); memoryStructure.def_property_readonly("nr_states", &MemoryStructure::getNumberOfStates); memoryStructure.def_property_readonly("state_labeling", &MemoryStructure::getStateLabeling); + + py::class_ memoryProductReverseData(m, "SparseModelMemoryProductReverseData"); } template diff --git a/tests/core/test_multiobjective.py b/tests/core/test_multiobjective.py index 84bc2742c4..2d264d1f11 100644 --- a/tests/core/test_multiobjective.py +++ b/tests/core/test_multiobjective.py @@ -1,10 +1,12 @@ +import math + import stormpy from helpers.helper import get_example_path from configurations import plotting, numpy_avail -class TestModelChecking: +class TestMultiObjectiveModelChecking: def naive_api_double_no_plotting_test(self): program = stormpy.parse_prism_program(get_example_path("mdp", "multiobjective1.nm")) properties = stormpy.parse_properties_for_prism_program('multi(Pmax=? [ F<=3 s=2 ],R{"rew"}max=? [ F s=2 ])', program) @@ -38,3 +40,30 @@ def naive_api_double_with_plotting_test(self): ax.set_xlabel(formula.subformulas[0]) ax.set_ylabel(formula.subformulas[1]) # plt.show() + +class TestWeightedObjectiveModelChecking: + def test_maze_double(self): + path = stormpy.examples.files.prism_mdp_maze_multigoal + prism_program = stormpy.parse_prism_program(path) + + formula_str = "multi(Rmin=? [F \"goalalt1\"], Pmax=? [F \"goalalt2\"])" + properties = stormpy.parse_properties(formula_str, prism_program) + + options = stormpy.BuilderOptions([p.raw_formula for p in properties]) + options.set_build_state_valuations() + env = stormpy.Environment() + model = stormpy.build_sparse_model_with_options(prism_program, options) + weighted_model_checker = stormpy._core._make_weighted_objective_mdp_model_checker_Double(env, model, properties[0].raw_formula, compute_scheduler=True) + weighted_model_checker.set_weighted_precision(0.0001) + weighted_model_checker.check(env, [0.5, 0.5]) + point = weighted_model_checker.get_achievable_point() + assert len(point) == 2 + assert math.isclose(point[0], 3.454545454545454) + assert math.isclose(point[1], 0.36363636363636365) + value = weighted_model_checker.get_optimal_weighted_sum() + assert math.isclose(value, -1.5454545454545454) + scheduler = weighted_model_checker.compute_scheduler() + assert scheduler.memoryless + assert scheduler.memory_size == 1 + + From e30c72de72882cc8f4da791bcea7274fa51fdef7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 11 Mar 2026 17:41:06 +0100 Subject: [PATCH 11/11] fixes --- src/core/multiobjective.cpp | 29 ++++++++++++----------------- src/storage/memorystructure.cpp | 4 ++++ tests/core/test_multiobjective.py | 13 ++++++------- 3 files changed, 22 insertions(+), 24 deletions(-) diff --git a/src/core/multiobjective.cpp b/src/core/multiobjective.cpp index 8736d7d39d..cf37cba3be 100644 --- a/src/core/multiobjective.cpp +++ b/src/core/multiobjective.cpp @@ -11,27 +11,22 @@ // //// Helper class to avoid that we also need to bind the preprocessing. template -std::unique_ptr>> makeWeightedObjectiveMDPModelChecker(storm::Environment const& env, storm::models::sparse::Mdp const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, bool produceScheduler) { -// auto const preprocessresult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, originalModel, originalFormula, produceScheduler); -// return storm::modelchecker::multiobjective::createWeightVectorChecker(preprocessresult); +std::pair>>, std::optional> makeWeightedObjectiveMDPModelChecker(storm::Environment const& env, storm::models::sparse::Mdp const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, bool produceScheduler) { + auto const preprocessresult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, originalModel, originalFormula, produceScheduler); + return std::make_pair(storm::modelchecker::multiobjective::createWeightVectorChecker(preprocessresult), preprocessresult.memoryIncorporationReverseData); } // -// -//// Define python bindings template void define_multiobjective(py::module& m, std::string const& vtSuffix) { -// m.def(("_weighted_objective_mdp_model_checker_preprocess" + vtSuffix).c_str(), &makeWeightedObjectiveMDPModelChecker, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); -// m.def("_create_weighted_objective_mdp_model_checker") -// -// using PcaaPreprocessorResult = storm::modelchecker::multiobjective::PcaaPreprocessorResult -// using PcaaWeightVectorChecker = storm::modelchecker::multiobjective::PcaaWeightVectorChecker>; -// py::class_< -// py::class_> weightedObjectiveMdpModelChecker(m, ("WeightedObjectiveMdpModelChecker" + vtSuffix).c_str()); -// weightedObjectiveMdpModelChecker.def("check", &PcaaWeightVectorChecker::check, py::arg("env"), py::arg("weight_vector")) -// .def("get_achievable_point", &PcaaWeightVectorChecker::getAchievablePoint) -// .def("get_optimal_weighted_sum", &PcaaWeightVectorChecker::getOptimalWeightedSum, "Note that this sum can be hard to interpret whenever one mixes minimization and maximization objectives.") -// .def("compute_scheduler", &PcaaWeightVectorChecker::computeScheduler, "Note that this is a scheduler on the preprocessed MDP") -// .def("set_weighted_precision", &PcaaWeightVectorChecker::setWeightedPrecision, py::arg("value"), "A smaller value means a higher precision."); + m.def(("_make_weighted_objective_mdp_model_checker_" + vtSuffix).c_str(), &makeWeightedObjectiveMDPModelChecker, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); + + using PcaaWeightVectorChecker = storm::modelchecker::multiobjective::PcaaWeightVectorChecker>; + py::class_> weightedObjectiveMdpModelChecker(m, ("WeightedObjectiveMdpModelChecker" + vtSuffix).c_str()); + weightedObjectiveMdpModelChecker.def("check", &PcaaWeightVectorChecker::check, py::arg("env"), py::arg("weight_vector")) + .def("get_achievable_point", &PcaaWeightVectorChecker::getAchievablePoint) + .def("get_optimal_weighted_sum", &PcaaWeightVectorChecker::getOptimalWeightedSum, "Note that this sum can be hard to interpret whenever one includes also minimization objectives.") + .def("compute_scheduler", &PcaaWeightVectorChecker::computeScheduler, "Note that this is a scheduler on the preprocessed MDP.") + .def("set_weighted_precision", &PcaaWeightVectorChecker::setWeightedPrecision, py::arg("value"), "A smaller value means a higher precision."); } // template void define_multiobjective(py::module&, std::string const&); diff --git a/src/storage/memorystructure.cpp b/src/storage/memorystructure.cpp index d669c149fd..a52c866ef5 100644 --- a/src/storage/memorystructure.cpp +++ b/src/storage/memorystructure.cpp @@ -4,6 +4,7 @@ #include #include #include +#include void define_memorystructure_untyped(py::module& m) { @@ -17,6 +18,9 @@ void define_memorystructure_untyped(py::module& m) { memoryStructure.def_property_readonly("state_labeling", &MemoryStructure::getStateLabeling); py::class_ memoryProductReverseData(m, "SparseModelMemoryProductReverseData"); + memoryProductReverseData.def("_reverse_scheduler_double", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, py::arg("product_scheduler")); + memoryProductReverseData.def("_reverse_scheduler_exact", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, py::arg("product_scheduler")); + memoryProductReverseData.def("_reverse_scheduler_parametric", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, py::arg("product_scheduler")); } template diff --git a/tests/core/test_multiobjective.py b/tests/core/test_multiobjective.py index 2d264d1f11..b10c98563c 100644 --- a/tests/core/test_multiobjective.py +++ b/tests/core/test_multiobjective.py @@ -53,17 +53,16 @@ def test_maze_double(self): options.set_build_state_valuations() env = stormpy.Environment() model = stormpy.build_sparse_model_with_options(prism_program, options) - weighted_model_checker = stormpy._core._make_weighted_objective_mdp_model_checker_Double(env, model, properties[0].raw_formula, compute_scheduler=True) + weighted_model_checker, inverter = stormpy._core._make_weighted_objective_mdp_model_checker_Double(env, model, properties[0].raw_formula, compute_scheduler=True) weighted_model_checker.set_weighted_precision(0.0001) weighted_model_checker.check(env, [0.5, 0.5]) point = weighted_model_checker.get_achievable_point() assert len(point) == 2 - assert math.isclose(point[0], 3.454545454545454) - assert math.isclose(point[1], 0.36363636363636365) + assert math.isclose(point[0], 3.8) + assert math.isclose(point[1], 0.4) value = weighted_model_checker.get_optimal_weighted_sum() - assert math.isclose(value, -1.5454545454545454) - scheduler = weighted_model_checker.compute_scheduler() - assert scheduler.memoryless - assert scheduler.memory_size == 1 + assert math.isclose(value, -1.7) + scheduler = inverter._reverse_scheduler_double(weighted_model_checker.compute_scheduler()) + assert scheduler.memory_size == 4