changed new_action function and map.py name to mapping.py

docs/getting_started/mdp.ipynb

@@ -6,7 +6,7 @@
       "metadata": {},
       "outputs": [],
       "source": [
-        "from stormvogel import visualization, map, result, show\n",
+        "from stormvogel import visualization, mapping, result, show\n",
         "import stormpy"
       ]
     },
@@ -260,7 +260,7 @@
       },
       "outputs": [],
       "source": [
-        "stormvogel_model = map.stormpy_to_stormvogel(leader_model)\n",
+        "stormvogel_model = mapping.stormpy_to_stormvogel(leader_model)\n",
         "\n",
         "stormvogel_result = result.convert_model_checking_result(stormvogel_model, stormpy_result)"
       ]

docs/getting_started/prism.ipynb

@@ -15,7 +15,7 @@
       "metadata": {},
       "outputs": [],
       "source": [
-        "from stormvogel import visualization, map, result, show\n",
+        "from stormvogel import visualization, mapping, result, show\n",
         "import stormpy"
       ]
     },
@@ -235,7 +235,7 @@
       "metadata": {},
       "outputs": [],
       "source": [
-        "stormvogel_model = map.stormpy_to_stormvogel(nand_model)\n",
+        "stormvogel_model = mapping.stormpy_to_stormvogel(nand_model)\n",
         "\n",
         "stormvogel_result = result.convert_model_checking_result(stormvogel_model, stormpy_result)"
       ]

stormvogel/map.py → stormvogel/mapping.py

@@ -384,7 +384,7 @@ def map_mdp(sparsemdp: stormpy.storage.SparseDtmc) -> stormvogel.model.Model:
                     else str(i)
                 )
                 # TODO assign the correct action name and not only an index
-                action = model.new_action_with_labels(str(i), actionlabels)
+                action = model.new_action(str(i), actionlabels)
                 branch = [(x.value(), model.get_state_by_id(x.column)) for x in row]
                 transition[action] = stormvogel.model.Branch(branch)
                 transitions = stormvogel.model.Transition(transition)
@@ -455,7 +455,7 @@ def map_pomdp(sparsepomdp: stormpy.storage.SparsePomdp) -> stormvogel.model.Mode
                     else str(i)
                 )
                 # TODO assign the correct action name and not only an index
-                action = model.new_action_with_labels(str(i), actionlabels)
+                action = model.new_action(str(i), actionlabels)
                 branch = [(x.value(), model.get_state_by_id(x.column)) for x in row]
                 transition[action] = stormvogel.model.Branch(branch)
                 transitions = stormvogel.model.Transition(transition)
@@ -498,7 +498,7 @@ def map_ma(sparsema: stormpy.storage.SparseMA) -> stormvogel.model.Model:
                     else str(i)
                 )
                 # TODO assign the correct action name and not only an index
-                action = model.new_action_with_labels(str(i), actionlabels)
+                action = model.new_action(str(i), actionlabels)
                 branch = [(x.value(), model.get_state_by_id(x.column)) for x in row]
                 transition[action] = stormvogel.model.Branch(branch)
                 transitions = stormvogel.model.Transition(transition)

stormvogel/model.py

@@ -359,7 +359,7 @@ def add_transitions(self, s: State, transitions: Transition | TransitionShorthan
         for choice, branch in transitions.transition.items():
             self.transitions[s.id].transition[choice] = branch
 
-    def new_action(self, name: str) -> Action:
+    def new_action(self, name: str, labels: frozenset[str] | None = None) -> Action:
         """Creates a new action and returns it."""
         if not self.supports_actions():
             raise RuntimeError(
@@ -370,22 +370,10 @@ def new_action(self, name: str) -> Action:
             raise RuntimeError(
                 f"Tried to add action {name} but that action already exists"
             )
-        action = Action(name, frozenset())
-        self.actions[name] = action
-        return action
-
-    def new_action_with_labels(self, name: str, labels: frozenset[str]) -> Action:
-        """Creates a new action with labels and returns it."""
-        if not self.supports_actions():
-            raise RuntimeError(
-                "Called new_action on a model that does not support actions"
-            )
-        assert self.actions is not None
-        if name in self.actions:
-            raise RuntimeError(
-                f"Tried to add action {name} but that action already exists"
-            )
-        action = Action(name, labels)
+        if labels:
+            action = Action(name, labels)
+        else:
+            action = Action(name, frozenset())
         self.actions[name] = action
         return action
 

stormvogel/result.py

@@ -1,5 +1,5 @@
 import stormpy
-import stormvogel.map
+import stormvogel.mapping
 import stormvogel.model
 import stormpy.examples.files
 import stormpy.examples
@@ -98,10 +98,10 @@ def generate_induced_dtmc(self) -> stormvogel.model.Model | None:
             self.model.get_type() == stormvogel.model.ModelType.MDP
             and self.scheduler is not None
         ):
-            stormpy_mdp = stormvogel.map.stormvogel_to_stormpy(self.model)
+            stormpy_mdp = stormvogel.mapping.stormvogel_to_stormpy(self.model)
             if stormpy_mdp is not None:
                 stormpy_dtmc = stormpy_mdp.apply_scheduler(self.stormpy_scheduler)
-                stormvogel_dtmc = stormvogel.map.stormpy_to_stormvogel(stormpy_dtmc)
+                stormvogel_dtmc = stormvogel.mapping.stormpy_to_stormvogel(stormpy_dtmc)
                 return stormvogel_dtmc
             else:
                 print("something went wrong")

tests/saved_test_layout.json

@@ -1,11 +1,14 @@
 {
-  "autoApply": true,
   "__fake_macros": {
     "__group_macro": {
       "borderWidth": 1,
       "color": {
         "background": "white",
-        "border": "black"
+        "border": "black",
+        "highlight": {
+          "background": "white",
+          "border": "red"
+        }
       },
       "shape": "ellipse",
       "mass": 1,
@@ -20,7 +23,11 @@
       "borderWidth": 1,
       "color": {
         "background": "white",
-        "border": "black"
+        "border": "black",
+        "highlight": {
+          "background": "white",
+          "border": "red"
+        }
       },
       "shape": "ellipse",
       "mass": 1,
@@ -33,7 +40,11 @@
       "borderWidth": 1,
       "color": {
         "background": "lightblue",
-        "border": "black"
+        "border": "black",
+        "highlight": {
+          "background": "white",
+          "border": "red"
+        }
       },
       "shape": "box",
       "mass": 1,
@@ -46,17 +57,24 @@
       "borderWidth": 1,
       "color": {
         "background": "pink",
-        "border": "black"
+        "border": "black",
+        "highlight": {
+          "background": "white",
+          "border": "red"
+        }
       },
       "shape": "box",
       "mass": 1,
       "font": {
         "color": "black",
         "size": 14
-      }
+      },
+      "schedColor": false
     }
   },
+  "reload_button": false,
   "edges": {
+    "arrows": "to",
     "font": {
       "color": "black",
       "size": 14
@@ -69,18 +87,30 @@
     "fractions": true,
     "digits": 5
   },
-  "resultSymbol": "\u2606",
-  "schedColor": true,
-  "physics": {
-    "enabled": true
+  "results_and_rewards": {
+    "show_results": true,
+    "resultSymbol": "\u2606",
+    "show_rewards": true
   },
   "layout": {
     "randomSeed": 5
   },
+  "misc": {
+    "enable_physics": true,
+    "width": 800,
+    "height": 600,
+    "explore": false
+  },
   "saving": {
     "relative_path": true,
-    "filename": "layouts/NAME.json"
+    "filename": "layouts/NAME.json",
+    "save_button": false,
+    "load_button": false
   },
+  "positions": {},
+  "width": 800,
+  "height": 600,
+  "physics": true,
   "init": {
     "color": "TEST_COLOR"
   }

tests/test_map.py → tests/test_mapping.py

@@ -1,6 +1,6 @@
 import examples.monty_hall
 import examples.stormpy_mdp
-import stormvogel.map
+import stormvogel.mapping
 import stormvogel.model
 import examples.stormpy_dtmc
 import examples.die
@@ -96,10 +96,10 @@ def test_stormpy_to_stormvogel_and_back_dtmc():
     # we test it for an example stormpy representation of a dtmc
     stormpy_dtmc = examples.stormpy_dtmc.example_building_dtmcs_01()
     # print(stormpy_dtmc.transition_matrix)
-    stormvogel_dtmc = stormvogel.map.stormpy_to_stormvogel(stormpy_dtmc)
+    stormvogel_dtmc = stormvogel.mapping.stormpy_to_stormvogel(stormpy_dtmc)
     # print(stormvogel_dtmc)
     assert stormvogel_dtmc is not None
-    new_stormpy_dtmc = stormvogel.map.stormvogel_to_stormpy(stormvogel_dtmc)
+    new_stormpy_dtmc = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_dtmc)
     # print(new_stormpy_dtmc.transition_matrix)
 
     # TODO also compare other parts than the matrix (e.g. state labels)
@@ -111,9 +111,9 @@ def test_stormvogel_to_stormpy_and_back_dtmc():
     # we test it for the die dtmc
     stormvogel_dtmc = examples.die.create_die_dtmc()
     # print(stormvogel_dtmc)
-    stormpy_dtmc = stormvogel.map.stormvogel_to_stormpy(stormvogel_dtmc)
+    stormpy_dtmc = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_dtmc)
     # print(stormpy_dtmc)
-    new_stormvogel_dtmc = stormvogel.map.stormpy_to_stormvogel(stormpy_dtmc)
+    new_stormvogel_dtmc = stormvogel.mapping.stormpy_to_stormvogel(stormpy_dtmc)
     # print(new_stormvogel_dtmc)
 
     assert new_stormvogel_dtmc == stormvogel_dtmc
@@ -123,10 +123,10 @@ def test_stormpy_to_stormvogel_and_back_mdp():
     # we test it for an example stormpy representation of an mdp
     stormpy_mdp = examples.stormpy_mdp.example_building_mdps_01()
     # print(stormpy_mdp)
-    stormvogel_mdp = stormvogel.map.stormpy_to_stormvogel(stormpy_mdp)
+    stormvogel_mdp = stormvogel.mapping.stormpy_to_stormvogel(stormpy_mdp)
     # print(stormvogel_mdp)
     assert stormvogel_mdp is not None
-    new_stormpy_mdp = stormvogel.map.stormvogel_to_stormpy(stormvogel_mdp)
+    new_stormpy_mdp = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_mdp)
     # print(new_stormpy_mdp)
 
     # TODO also compare other parts than the matrix (e.g. choice labels)
@@ -137,9 +137,9 @@ def test_stormvogel_to_stormpy_and_back_mdp():
     # we test it for monty hall mdp
     stormvogel_mdp = examples.monty_hall.create_monty_hall_mdp()
     # print(stormvogel_mdp)
-    stormpy_mdp = stormvogel.map.stormvogel_to_stormpy(stormvogel_mdp)
+    stormpy_mdp = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_mdp)
     # print(stormpy_mdp)
-    new_stormvogel_mdp = stormvogel.map.stormpy_to_stormvogel(stormpy_mdp)
+    new_stormvogel_mdp = stormvogel.mapping.stormpy_to_stormvogel(stormpy_mdp)
     # print(new_stormvogel_mdp)
 
     assert new_stormvogel_mdp == stormvogel_mdp
@@ -149,9 +149,9 @@ def test_stormvogel_to_stormpy_and_back_ctmc():
     # we create a stormpy representation of an example ctmc
     stormvogel_ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
     # print(stormvogel_ctmc)
-    stormpy_ctmc = stormvogel.map.stormvogel_to_stormpy(stormvogel_ctmc)
+    stormpy_ctmc = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_ctmc)
     # print(stormpy_ctmc)
-    new_stormvogel_ctmc = stormvogel.map.stormpy_to_stormvogel(stormpy_ctmc)
+    new_stormvogel_ctmc = stormvogel.mapping.stormpy_to_stormvogel(stormpy_ctmc)
     # print(new_stormvogel_ctmc)
 
     assert new_stormvogel_ctmc == stormvogel_ctmc
@@ -161,10 +161,10 @@ def test_stormpy_to_stormvogel_and_back_ctmc():
     # we create a stormpy representation of an example ctmc
     stormpy_ctmc = examples.stormpy_ctmc.example_building_ctmcs_01()
     # print(stormpy_ctmc)
-    stormvogel_ctmc = stormvogel.map.stormpy_to_stormvogel(stormpy_ctmc)
+    stormvogel_ctmc = stormvogel.mapping.stormpy_to_stormvogel(stormpy_ctmc)
     # print(stormvogel_ctmc)
     assert stormvogel_ctmc is not None
-    new_stormpy_ctmc = stormvogel.map.stormvogel_to_stormpy(stormvogel_ctmc)
+    new_stormpy_ctmc = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_ctmc)
     # print(new_stormpy_ctmc)
 
     assert sparse_equal(stormpy_ctmc, new_stormpy_ctmc)
@@ -174,9 +174,9 @@ def test_stormvogel_to_stormpy_and_back_pomdp():
     # we create a stormpy representation of an example pomdp
     stormvogel_pomdp = examples.monty_hall_pomdp.create_monty_hall_pomdp()
     # print(stormvogel_pomdp)
-    stormpy_pomdp = stormvogel.map.stormvogel_to_stormpy(stormvogel_pomdp)
+    stormpy_pomdp = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_pomdp)
     # print(stormpy_pomdp)
-    new_stormvogel_pomdp = stormvogel.map.stormpy_to_stormvogel(stormpy_pomdp)
+    new_stormvogel_pomdp = stormvogel.mapping.stormpy_to_stormvogel(stormpy_pomdp)
     # print(new_stormvogel_pomdp)
 
     assert new_stormvogel_pomdp == stormvogel_pomdp
@@ -186,10 +186,10 @@ def test_stormpy_to_stormvogel_and_back_pomdp():
     # we create a stormpy representation of an example pomdp
     stormpy_pomdp = examples.stormpy_pomdp.example_building_pomdps_01()
     # print(stormpy_pomdp)
-    stormvogel_pomdp = stormvogel.map.stormpy_to_stormvogel(stormpy_pomdp)
+    stormvogel_pomdp = stormvogel.mapping.stormpy_to_stormvogel(stormpy_pomdp)
     # print(stormvogel_pomdp)
     assert stormvogel_pomdp is not None
-    new_stormpy_pomdp = stormvogel.map.stormvogel_to_stormpy(stormvogel_pomdp)
+    new_stormpy_pomdp = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_pomdp)
     # print(new_stormpy_pomdp)
 
     assert sparse_equal(stormpy_pomdp, new_stormpy_pomdp)
@@ -199,9 +199,9 @@ def test_stormvogel_to_stormpy_and_back_ma():
     # we create a stormpy representation of an example ma
     stormvogel_ma = examples.simple_ma.create_simple_ma()
     # print(stormvogel_ma)
-    stormpy_ma = stormvogel.map.stormvogel_to_stormpy(stormvogel_ma)
+    stormpy_ma = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_ma)
     # print(stormpy_ma)
-    new_stormvogel_ma = stormvogel.map.stormpy_to_stormvogel(stormpy_ma)
+    new_stormvogel_ma = stormvogel.mapping.stormpy_to_stormvogel(stormpy_ma)
     # print(new_stormvogel_ma)
 
     assert new_stormvogel_ma == stormvogel_ma
@@ -211,10 +211,10 @@ def test_stormpy_to_stormvogel_and_back_ma():
     # we create a stormpy representation of an example ma
     stormpy_ma = examples.stormpy_ma.example_building_mas_01()
     # print(stormpy_ma)
-    stormvogel_ma = stormvogel.map.stormpy_to_stormvogel(stormpy_ma)
+    stormvogel_ma = stormvogel.mapping.stormpy_to_stormvogel(stormpy_ma)
     # print(stormvogel_ma)
     assert stormvogel_ma is not None
-    new_stormpy_ma = stormvogel.map.stormvogel_to_stormpy(stormvogel_ma)
+    new_stormpy_ma = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_ma)
     # print(new_stormpy_ma)
 
     assert sparse_equal(stormpy_ma, new_stormpy_ma)

tests/test_result.py

@@ -12,7 +12,7 @@ def test_convert_model_checker_results_dtmc():
     model = stormpy.build_model(prism_program, properties)
     result = stormpy.model_checking(model, properties[0])
 
-    stormvogel_model = stormvogel.map.stormpy_to_stormvogel(model)
+    stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(model)
     assert stormvogel_model is not None
     stormvogel_result = stormvogel.result.convert_model_checking_result(
         stormvogel_model, result
@@ -44,7 +44,7 @@ def test_convert_model_checker_results_dtmc_qualitative():
     model = stormpy.build_model(prism_program, properties)
     result = stormpy.model_checking(model, properties[0])
 
-    stormvogel_model = stormvogel.map.stormpy_to_stormvogel(model)
+    stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(model)
     assert stormvogel_model is not None
     stormvogel_result = stormvogel.result.convert_model_checking_result(
         stormvogel_model, result
@@ -78,7 +78,7 @@ def test_convert_model_checker_results_mdp():
     model = stormpy.build_model(prism_program, properties)
     result = stormpy.model_checking(model, properties[0], extract_scheduler=True)
 
-    stormvogel_model = stormvogel.map.stormpy_to_stormvogel(model)
+    stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(model)
     assert stormvogel_model is not None
     stormvogel_result = stormvogel.result.convert_model_checking_result(
         stormvogel_model, result
@@ -650,7 +650,7 @@ def test_convert_model_checker_results_mdp_qualitative():
     model = stormpy.build_model(prism_program, properties)
     result = stormpy.model_checking(model, properties[0], extract_scheduler=True)
 
-    stormvogel_model = stormvogel.map.stormpy_to_stormvogel(model)
+    stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(model)
     assert stormvogel_model is not None
     stormvogel_result = stormvogel.result.convert_model_checking_result(
         stormvogel_model, result