added option to not automatically set initial state

docs/getting_started/study.html

@@ -1,6 +1,6 @@
 
           <iframe
-                id="studyJItnPUbGyS"
+                id="studyQvPbMkPXdR"
                 width="820"
                 height="620"
                 frameborder="0"

examples/stormpy_dtmc.py

@@ -44,7 +44,7 @@ def example_building_dtmcs_01():
         state_labeling.add_label(label)
 
     # Set label of state 0
-    state_labeling.add_label_to_state("init", 0)
+    state_labeling.add_label_to_state("init", 1)
     # print(state_labeling.get_states("init"))
 
     # Set remaining labels

stormvogel/mapping.py

@@ -324,6 +324,7 @@ def add_states(
         """
         helper function to add the states from the sparsemodel to the model
         """
+        model.new_state()
         for state in sparsemodel.states:
             if state.id == 0:
                 for label in state.labels:
@@ -357,7 +358,7 @@ def map_dtmc(sparsedtmc: stormpy.storage.SparseDtmc) -> stormvogel.model.Model:
         """
 
         # we create the model (it seems names are not stored in sparsedtmcs)
-        model = stormvogel.model.new_dtmc(name=None)
+        model = stormvogel.model.new_dtmc(name=None, create_initial_state=False)
 
         # we add the states
         add_states(model, sparsedtmc)
@@ -388,7 +389,7 @@ def map_mdp(sparsemdp: stormpy.storage.SparseDtmc) -> stormvogel.model.Model:
         """
 
         # we create the model
-        model = stormvogel.model.new_mdp(name=None)
+        model = stormvogel.model.new_mdp(name=None, create_initial_state=False)
 
         # we add the states
         add_states(model, sparsemdp)
@@ -430,7 +431,7 @@ def map_ctmc(sparsectmc: stormpy.storage.SparseCtmc) -> stormvogel.model.Model:
         """
 
         # we create the model (it seems names are not stored in sparsectmcs)
-        model = stormvogel.model.new_ctmc(name=None)
+        model = stormvogel.model.new_ctmc(name=None, create_initial_state=False)
 
         # we add the states
         add_states(model, sparsectmc)
@@ -465,7 +466,7 @@ def map_pomdp(sparsepomdp: stormpy.storage.SparsePomdp) -> stormvogel.model.Mode
         """
 
         # we create the model (it seems names are not stored in sparsepomdps)
-        model = stormvogel.model.new_pomdp(name=None)
+        model = stormvogel.model.new_pomdp(name=None, create_initial_state=False)
 
         # we add the states
         add_states(model, sparsepomdp)
@@ -511,7 +512,7 @@ def map_ma(sparsema: stormpy.storage.SparseMA) -> stormvogel.model.Model:
         """
 
         # we create the model (it seems names are not stored in sparsemas)
-        model = stormvogel.model.new_ma(name=None)
+        model = stormvogel.model.new_ma(name=None, create_initial_state=False)
 
         # we add the states
         add_states(model, sparsema)

stormvogel/model.py

@@ -359,7 +359,9 @@ class Model:
     # In ma's we keep track of markovian states
     markovian_states: list[State] | None
 
-    def __init__(self, name: str | None, model_type: ModelType):
+    def __init__(
+        self, name: str | None, model_type: ModelType, create_initial_state: bool = True
+    ):
         self.name = name
         self.type = model_type
         self.transitions = {}
@@ -391,7 +393,8 @@ def __init__(self, name: str | None, model_type: ModelType):
             self.markovian_states = None
 
         # Add the initial state
-        self.new_state(["init"])
+        if create_initial_state:
+            self.new_state(["init"])
 
     def supports_actions(self):
         """Returns whether this model supports actions."""
@@ -853,31 +856,33 @@ def __eq__(self, other):
         return False
 
 
-def new_dtmc(name: str | None = None):
+def new_dtmc(name: str | None = None, create_initial_state: bool = True):
     """Creates a DTMC."""
-    return Model(name, ModelType.DTMC)
+    return Model(name, ModelType.DTMC, create_initial_state)
 
 
-def new_mdp(name: str | None = None):
+def new_mdp(name: str | None = None, create_initial_state: bool = True):
     """Creates an MDP."""
-    return Model(name, ModelType.MDP)
+    return Model(name, ModelType.MDP, create_initial_state)
 
 
-def new_ctmc(name: str | None = None):
+def new_ctmc(name: str | None = None, create_initial_state: bool = True):
     """Creates a CTMC."""
-    return Model(name, ModelType.CTMC)
+    return Model(name, ModelType.CTMC, create_initial_state)
 
 
-def new_pomdp(name: str | None = None):
+def new_pomdp(name: str | None = None, create_initial_state: bool = True):
     """Creates a POMDP."""
-    return Model(name, ModelType.POMDP)
+    return Model(name, ModelType.POMDP, create_initial_state)
 
 
-def new_ma(name: str | None = None):
+def new_ma(name: str | None = None, create_initial_state: bool = True):
     """Creates a MA."""
-    return Model(name, ModelType.MA)
+    return Model(name, ModelType.MA, create_initial_state)
 
 
-def new_model(modeltype: ModelType, name: str | None = None):
+def new_model(
+    modeltype: ModelType, name: str | None = None, create_initial_state: bool = True
+):
     """More general model creation function"""
-    return Model(name, modeltype)
+    return Model(name, modeltype, create_initial_state)

tests/test_mapping.py

@@ -102,8 +102,6 @@ def test_stormpy_to_stormvogel_and_back_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)
-
     assert sparse_equal(stormpy_dtmc, new_stormpy_dtmc)
 
 
@@ -138,7 +136,6 @@ def test_stormpy_to_stormvogel_and_back_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)
     assert sparse_equal(stormpy_mdp, new_stormpy_mdp)