From 04362becb6b6c29dac38e36872f8c1e24bdc2761 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 19 May 2022 14:30:25 +0200 Subject: [PATCH 1/6] 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 000000000..ab9c9961f --- /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 7368dae31..d7e8167fb 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 215cac5c2..3a8c4e4fd 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 000000000..b9d00a882 --- /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 4d88ab014..e6b6e0e20 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 2/6] 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 5757ee528..8a633a21e 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 9540aea5f..dffd9aa79 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 54c87224f..6c3673695 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 c55a67d68..e235f54f4 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 3/6] 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 c0ad27dc2..a92f28d1e 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 5f0f4777e..e5bd5bab1 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 4/6] 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 ce64f17f0..8de0ed56b 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 e73354b42..ebd3f2628 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 87b290667..eec6cb5ff 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 3e072dbef..11740e2b9 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 314f66dd70eb59891a7aba6721be05609ee0e15b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 12 Nov 2024 14:18:43 +0100 Subject: [PATCH 5/6] update on observation trace unfolder bindings --- lib/stormpy/pomdp/__init__.py | 9 ++++++--- src/pomdp/transformations.cpp | 17 ++++++++++++----- 2 files changed, 18 insertions(+), 8 deletions(-) diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index d490e77b4..389565c0a 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -64,15 +64,18 @@ def create_nondeterminstic_belief_tracker(model, reduction_timeout, track_timeou return pomdp.NondeterministicBeliefTrackerDoubleSparse(model, opts) -def create_observation_trace_unfolder(model, risk_assessment, expr_manager): +def create_observation_trace_unfolder(model, risk_assessment, expr_manager, rejection_sampling = True): """ :param model: :param risk_assessment: :param expr_manager: + :param rejection_sampling: :return: """ + options = pomdp.ObservationTraceUnfolderOptions() + options.rejection_sampling = rejection_sampling if model.is_exact: - return pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager) + return pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager, options) else: - return pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager) \ No newline at end of file + return pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager, options) \ No newline at end of file diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index 07fa32abc..5428f626e 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -32,9 +32,11 @@ std::shared_ptr> apply_unk } template -std::shared_ptr> unfold_trace(storm::models::sparse::Pomdp const& pomdp, std::shared_ptr& exprManager, std::vector const& observationTrace, std::vector const& riskDef ) { - storm::pomdp::ObservationTraceUnfolder transformer(pomdp, exprManager); - return transformer.transform(observationTrace, riskDef); +std::shared_ptr> unfold_trace(storm::models::sparse::Pomdp const& pomdp, std::shared_ptr& exprManager, std::vector const& observationTrace, std::vector const& riskDef, bool rejectionSampling=true) { + storm::pomdp::ObservationTraceUnfolderOptions options = storm::pomdp::ObservationTraceUnfolderOptions(); + options.rejectionSampling = rejectionSampling; + storm::pomdp::ObservationTraceUnfolder transformer(pomdp, riskDef, exprManager, options); + return transformer.transform(observationTrace); } // STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL @@ -47,6 +49,11 @@ void define_transformations_nt(py::module &m) { .value("full", storm::transformer::PomdpFscApplicationMode::FULL) ; + py::class_ unfolderOptions(m, "ObservationTraceUnfolderOptions", "Options for the ObservationTraceUnfolder"); + unfolderOptions.def(py::init<>()); + unfolderOptions.def_readwrite("rejection_sampling", &storm::pomdp::ObservationTraceUnfolderOptions::rejectionSampling); + + } template @@ -55,10 +62,10 @@ void define_transformations(py::module& m, std::string const& vtSuffix) { m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false, py::arg("keep_state_valuations")=false); m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false); m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); - //m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace, "Unfold observed trace", py::arg("pomdp"), py::arg("expression_manager"),py::arg("observation_trace"), py::arg("risk_definition")); py::class_> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(), "Unfolds observation traces in models"); - unfolder.def(py::init const&, std::vector const&, std::shared_ptr&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager")); + unfolder.def(py::init const&, std::vector const&, std::shared_ptr&, storm::pomdp::ObservationTraceUnfolderOptions const&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager"), py::arg("options")); + unfolder.def("is_rejection_sampling_set", &storm::pomdp::ObservationTraceUnfolder::isRejectionSamplingSet); unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder::transform, py::arg("trace")); unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder::extend, py::arg("new_observation")); unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder::reset, py::arg("new_observation")); From 3125e2c1af75410b96ec584afd0b22cabdce462e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 16 Dec 2024 10:08:43 +0100 Subject: [PATCH 6/6] improved name for arguments --- src/pomdp/transformations.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index 5428f626e..8ea950f65 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -67,7 +67,7 @@ void define_transformations(py::module& m, std::string const& vtSuffix) { unfolder.def(py::init const&, std::vector const&, std::shared_ptr&, storm::pomdp::ObservationTraceUnfolderOptions const&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager"), py::arg("options")); unfolder.def("is_rejection_sampling_set", &storm::pomdp::ObservationTraceUnfolder::isRejectionSamplingSet); unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder::transform, py::arg("trace")); - unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder::extend, py::arg("new_observation")); + unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder::extend, py::arg("new_observations")); unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder::reset, py::arg("new_observation")); }