Skip to content

Commit

Permalink
recent changes in storm
Browse files Browse the repository at this point in the history
  • Loading branch information
sjunges committed May 23, 2024
1 parent a23b688 commit f7fb788
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 79 deletions.
76 changes: 0 additions & 76 deletions doc/source/doc/simulator.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,6 @@
{
"cell_type": "markdown",
"metadata": {
<<<<<<< HEAD
=======
"collapsed": true,
>>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761
"pycharm": {
"name": "#%%md\n"
}
Expand All @@ -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
]
},
{
Expand Down Expand Up @@ -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
]
},
{
Expand Down Expand Up @@ -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
]
},
{
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -520,11 +482,7 @@
},
{
"cell_type": "code",
<<<<<<< HEAD
"execution_count": 17,
=======
"execution_count": 25,
>>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761
"metadata": {
"scrolled": true
},
Expand All @@ -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
]
}
],
Expand Down Expand Up @@ -588,11 +540,7 @@
},
{
"cell_type": "code",
<<<<<<< HEAD
"execution_count": 18,
=======
"execution_count": null,
>>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761
"metadata": {},
"outputs": [],
"source": [
Expand All @@ -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
]
}
],
Expand All @@ -643,16 +581,6 @@
"for path in paths:\n",
" print(\" \".join(path))"
]
<<<<<<< HEAD
=======
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
>>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761
}
],
"metadata": {
Expand All @@ -675,9 +603,5 @@
}
},
"nbformat": 4,
<<<<<<< HEAD
"nbformat_minor": 4
=======
"nbformat_minor": 1
>>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761
}
3 changes: 0 additions & 3 deletions lib/stormpy/examples/files/mdp/slipgrid.nm
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,7 @@ rewards
endrewards

// target observation
<<<<<<< HEAD
label "target" = x=3 & y=3;
=======
>>>>>>> 04362becb6b6c29dac38e36872f8c1e24bdc2761
label "goal" = x=N & y=M;


2 changes: 2 additions & 0 deletions src/pomdp/quantitative_analysis.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
#include "quantitative_analysis.h"

#include <storm/adapters/RationalFunctionAdapter.h>
#include <storm/models/sparse/Pomdp.h>
#include <storm-pomdp/api/verification.h>

Expand Down
2 changes: 2 additions & 0 deletions src/pomdp/tracker.cpp
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
#include "tracker.h"
#include "src/helpers.h"

#include <storm/adapters/RationalFunctionAdapter.h>
#include <storm-pomdp/generator/BeliefSupportTracker.h>
#include <storm-pomdp/generator/NondeterministicBeliefTracker.h>

Expand Down

0 comments on commit f7fb788

Please sign in to comment.