Skip to content

Commit

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

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


0 comments on commit 8c6ecc5

Please sign in to comment.