simulator support for nondeterministic models

examples/simulator/01-simulator.py

@@ -4,8 +4,9 @@ import stormpy.simulator
 
 import stormpy.examples
 import stormpy.examples.files
-
-
+"""
+Simulator for deterministic models
+"""
 def example_simulator_01():
     path = stormpy.examples.files.prism_dtmc_die
     prism_program = stormpy.parse_prism_program(path)

examples/simulator/02-simulator.py

@@ -0,0 +1,42 @@
+import stormpy
+import stormpy.core
+import stormpy.simulator
+
+import stormpy.examples
+import stormpy.examples.files
+import random
+
+"""
+Simulator for nondeterministic models
+"""
+def example_simulator_01():
+    path = stormpy.examples.files.prism_mdp_maze
+    prism_program = stormpy.parse_prism_program(path)
+
+    model = stormpy.build_model(prism_program)
+    simulator = stormpy.simulator.create_simulator(model, seed=42)
+    # 5 paths of at most 20 steps.
+    paths = []
+    for m in range(5):
+        path = []
+        state = simulator.restart()
+        path = [f"{state}"]
+        for n in range(20):
+            actions = simulator.available_actions()
+            select_action = random.randint(0,len(actions)-1)
+            #print(f"Randomly select action nr: {select_action} from actions {actions}")
+            path.append(f"--act={actions[select_action]}-->")
+            state = simulator.step(actions[select_action])
+            #print(state)
+            path.append(f"{state}")
+            if simulator.is_done():
+                #print("Trapped!")
+                break
+        paths.append(path)
+    for path in paths:
+        print(" ".join(path))
+
+
+
+if __name__ == '__main__':
+    example_simulator_01()

lib/stormpy/simulator.py

@@ -7,6 +7,9 @@ class SimulatorObservationMode(Enum):
     STATE_LEVEL = 0,
     PROGRAM_LEVEL = 1
 
+class SimulatorActionMode(Enum):
+    INDEX_LEVEL = 0
+
 class Simulator:
     """
     Base class for simulators.
@@ -14,6 +17,16 @@ class Simulator:
     def __init__(self, seed=None):
         self._seed = seed
         self._observation_mode = SimulatorObservationMode.STATE_LEVEL
+        self._action_mode = SimulatorActionMode.INDEX_LEVEL
+
+    def available_actions(self):
+        """
+        Returns an iterable over the available actions. The action mode may be used to select how actions are referred to.
+        TODO: Support multiple action modes
+
+        :return:
+        """
+        raise NotImplementedError("Abstract Superclass")
 
     def step(self, action=None):
         """
@@ -62,26 +75,35 @@ class SparseSimulator(Simulator):
             self._engine.set_seed(seed)
         self._state_valuations = None
 
+    def available_actions(self):
+        return range(self.nr_available_actions())
+
+    def nr_available_actions(self):
+        return self._model.get_nr_available_actions(self._engine.get_current_state())
+
+    def _report_observation(self):
+        if self._observation_mode == SimulatorObservationMode.STATE_LEVEL:
+            return self._engine.get_current_state()
+        elif self._observation_mode == SimulatorObservationMode.PROGRAM_LEVEL:
+            return self._state_valuations.get_state(self._engine.get_current_state())
+
     def step(self, action=None):
         if action is None:
-            if self._model.is_nondeterministic_model:
-                raise RuntimeError("Must specify an action in nondeterministic models")
+            if self._model.is_nondeterministic_model and self.nr_available_actions() > 1:
+                raise RuntimeError("Must specify an action in nondeterministic models.")
             check = self._engine.step(0)
             assert check
         else:
-            if action >= self._model.get_nondeterministic_choices():
-                raise RuntimeError(f"Only {self._model.get_nondeterministic_choices()} actions available")
+            if action >= self.nr_available_actions():
+                raise RuntimeError(f"Only {self.nr_available_actions()} actions available")
             check = self._engine.step(action)
             assert check
-        if self._observation_mode == SimulatorObservationMode.STATE_LEVEL:
-            return self._engine.get_current_state()
-        elif self._observation_mode == SimulatorObservationMode.PROGRAM_LEVEL:
-            return self._state_valuations.get_state(self._engine.get_current_state())
+        return self._report_observation()
 
-        assert False, "Observation Mode not recognised."
 
     def restart(self):
         self._engine.reset_to_initial_state()
+        return self._report_observation()
 
     def is_done(self):
         return self._model.is_sink_state(self._engine.get_current_state())