Merge pull request #173 from moves-rwth/137-state-builder

137 state builder
moves-rwth · Dec 22, 2024 · bfdd07c · bfdd07c
2 parents a6d8cac + 081efbe
commit bfdd07c
Show file tree

Hide file tree

Showing 5 changed files with 434 additions and 23 deletions.
diff --git a/docs/getting_started/04_mdp.ipynb b/docs/getting_started/04_mdp.ipynb
@@ -9,7 +9,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 2,
+      "execution_count": 1,
       "metadata": {},
       "outputs": [],
       "source": [
@@ -19,16 +19,16 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 3,
+      "execution_count": 2,
       "metadata": {},
       "outputs": [
         {
           "data": {
             "text/plain": [
-              "<stormpy.storage.storage.PrismProgram at 0x7f70bcd3d530>"
+              "<stormpy.storage.storage.PrismProgram at 0x7f6c38d21f70>"
             ]
           },
-          "execution_count": 3,
+          "execution_count": 2,
           "metadata": {},
           "output_type": "execute_result"
         }
@@ -132,7 +132,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 4,
+      "execution_count": 3,
       "metadata": {},
       "outputs": [],
       "source": [
@@ -142,7 +142,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 5,
+      "execution_count": 4,
       "metadata": {},
       "outputs": [
         {
@@ -174,7 +174,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 6,
+      "execution_count": 5,
       "metadata": {},
       "outputs": [],
       "source": [
@@ -183,7 +183,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 7,
+      "execution_count": 6,
       "metadata": {},
       "outputs": [],
       "source": [
@@ -192,7 +192,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 8,
+      "execution_count": 7,
       "metadata": {},
       "outputs": [
         {
@@ -209,7 +209,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 9,
+      "execution_count": 8,
       "metadata": {},
       "outputs": [
         {
@@ -239,7 +239,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 10,
+      "execution_count": 9,
       "metadata": {},
       "outputs": [
         {
@@ -261,7 +261,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 11,
+      "execution_count": 10,
       "metadata": {
         "scrolled": true
       },
@@ -274,7 +274,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 12,
+      "execution_count": 11,
       "metadata": {
         "scrolled": true
       },
@@ -284,7 +284,7 @@
             "text/html": [
               "\n",
               "          <iframe\n",
-              "                id=\"modelclDGBmFPaZ\"\n",
+              "                id=\"modelZzRAPaKtcw\"\n",
               "                width=\"820\"\n",
               "                height=\"620\"\n",
               "                frameborder=\"0\"\n",
@@ -2141,7 +2141,7 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 13,
+      "execution_count": 12,
       "metadata": {},
       "outputs": [],
       "source": [
@@ -2150,15 +2150,17 @@
     },
     {
       "cell_type": "code",
-      "execution_count": 14,
-      "metadata": {},
+      "execution_count": 13,
+      "metadata": {
+        "scrolled": true
+      },
       "outputs": [
         {
           "data": {
             "text/html": [
               "\n",
               "          <iframe\n",
-              "                id=\"modelhYRVZOxBne\"\n",
+              "                id=\"modeleXgJiypsxN\"\n",
               "                width=\"820\"\n",
               "                height=\"620\"\n",
               "                frameborder=\"0\"\n",
@@ -2514,6 +2516,48 @@
         "vis2 = show.show(induced_dtmc, layout=stormvogel.layout.EXPLORE(), show_editor=False, save_and_embed=True)"
       ]
     },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": []
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": []
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": []
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": []
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": []
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": []
+    },
     {
       "cell_type": "code",
       "execution_count": null,

diff --git a/docs/getting_started/model.html b/docs/getting_started/model.html
@@ -1,6 +1,6 @@
 
           <iframe
-                id="modelhYRVZOxBne"
+                id="modeleXgJiypsxN"
                 width="820"
                 height="620"
                 frameborder="0"

diff --git a/stormvogel/model.py b/stormvogel/model.py
@@ -205,7 +205,7 @@ class Action:
         labels: The labels of this action. Corresponds to Storm labels.
     """
 
-    name: str
+    name: str  # TODO name is stormpy choice label or we don't need a name at all?
     labels: frozenset[str]
 
     def __str__(self):
@@ -862,6 +862,8 @@ def get_action(self, name: str) -> Action:
             )
         assert self.actions is not None
         if name not in self.actions:
+            print(name)
+            print(self.actions)
             raise RuntimeError(
                 f"Tried to get action {name} but that action does not exist"
             )
@@ -883,15 +885,16 @@ def new_state(
         self,
         labels: list[str] | str | None = None,
         features: dict[str, int] | None = None,
+        name: str | None = None,
     ) -> State:
         """Creates a new state and returns it."""
         state_id = self.__free_state_id()
         if isinstance(labels, list):
-            state = State(labels, features or {}, state_id, self)
+            state = State(labels, features or {}, state_id, self, name=name)
         elif isinstance(labels, str):
-            state = State([labels], features or {}, state_id, self)
+            state = State([labels], features or {}, state_id, self, name=name)
         elif labels is None:
-            state = State([], features or {}, state_id, self)
+            state = State([], features or {}, state_id, self, name=name)
 
         self.states[state_id] = state