From 38189e700418fbd48773a6adae6deb14ce3eaaf2 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sun, 12 Apr 2020 22:02:39 -0700
Subject: [PATCH] first version of a model simulator

---
 examples/simulator/01-simulator.py | 27 ++++++++++++++
 lib/stormpy/simulator.py           | 58 ++++++++++++++++++++++++++++++
 src/core/simulator.cpp             | 12 +++++++
 src/core/simulator.h               |  5 +++
 src/mod_core.cpp                   |  2 ++
 5 files changed, 104 insertions(+)
 create mode 100644 examples/simulator/01-simulator.py
 create mode 100644 lib/stormpy/simulator.py
 create mode 100644 src/core/simulator.cpp
 create mode 100644 src/core/simulator.h

diff --git a/examples/simulator/01-simulator.py b/examples/simulator/01-simulator.py
new file mode 100644
index 0000000..aa8f1e7
--- /dev/null
+++ b/examples/simulator/01-simulator.py
@@ -0,0 +1,27 @@
+import stormpy
+import stormpy.core
+import stormpy.simulator
+
+import stormpy.examples
+import stormpy.examples.files
+
+
+def example_simulator_01():
+    path = stormpy.examples.files.prism_dtmc_die
+    prism_program = stormpy.parse_prism_program(path)
+
+    model = stormpy.build_model(prism_program)
+    simulator = stormpy.simulator.create_simulator(model, seed=42)
+    final_outcomes = dict()
+    for n in range(1000):
+        for i in range(100):
+            observation = simulator.step()
+        if observation not in final_outcomes:
+            final_outcomes[observation] = 1
+        else:
+            final_outcomes[observation] += 1
+        simulator.restart()
+    print(final_outcomes)
+
+if __name__ == '__main__':
+    example_simulator_01()
diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py
new file mode 100644
index 0000000..7163805
--- /dev/null
+++ b/lib/stormpy/simulator.py
@@ -0,0 +1,58 @@
+import stormpy.core
+
+class Simulator:
+    """
+    Base class for simulators.
+    """
+    def __init__(self, seed=None):
+        self._seed = seed
+
+    def step(self, action=None):
+        raise NotImplementedError("Abstract superclass")
+
+    def restart(self):
+        raise NotImplementedError("Abstract superclass")
+
+
+class SparseSimulator(Simulator):
+    """
+    Simulator on top of sparse models.
+    """
+
+    def __init__(self, model, seed=None):
+        super().__init__(seed)
+        self._model = model
+        self._engine = stormpy.core._DiscreteTimeSparseModelSimulatorDouble(model)
+        if seed is not None:
+            self._engine.set_seed(seed)
+
+    def step(self, action=None):
+        if action is None:
+            if self._model.is_nondeterministic_model:
+                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")
+            check = self._engine.step(action)
+            assert(check)
+        return self._engine.get_current_state()
+
+    def restart(self):
+        self._engine.reset_to_initial_state()
+
+
+def create_simulator(model, seed = None):
+    """
+    Factory method for creating a simulator.
+
+    :param model: Some form of model
+    :param seed: A seed for reproducibility. If None (default), the seed is internally generated.
+    :return: A simulator that can simulate on top of this model
+    """
+    if isinstance(model, stormpy.storage._ModelBase):
+        if model.is_sparse_model:
+            return SparseSimulator(model, seed)
+    else:
+        raise NotImplementedError("Currently, we only support simulators for sparse models.")
diff --git a/src/core/simulator.cpp b/src/core/simulator.cpp
new file mode 100644
index 0000000..263a44d
--- /dev/null
+++ b/src/core/simulator.cpp
@@ -0,0 +1,12 @@
+#include "simulator.h"
+#include <storm/simulator/DiscreteTimeSparseModelSimulator.h>
+
+void define_sparse_model_simulator(py::module& m) {
+    py::class_<storm::simulator::DiscreteTimeSparseModelSimulator<double>> dtsmsd(m, "_DiscreteTimeSparseModelSimulatorDouble", "Simulator for sparse discrete-time models in memory (ValueType = double)");
+    dtsmsd.def(py::init<storm::models::sparse::Model<double> const&>());
+    dtsmsd.def("set_seed", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::setSeed, py::arg("seed"));
+    dtsmsd.def("step", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::step, py::arg("action"));
+    dtsmsd.def("get_current_state", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::getCurrentState);
+    dtsmsd.def("reset_to_initial_state", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::resetToInitial);
+
+}
\ No newline at end of file
diff --git a/src/core/simulator.h b/src/core/simulator.h
new file mode 100644
index 0000000..4edb35b
--- /dev/null
+++ b/src/core/simulator.h
@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_sparse_model_simulator(py::module& m);
\ No newline at end of file
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index 84467ef..f16db4d 100644
--- a/src/mod_core.cpp
+++ b/src/mod_core.cpp
@@ -9,6 +9,7 @@
 #include "core/counterexample.h"
 #include "core/environment.h"
 #include "core/transformation.h"
+#include "core/simulator.h"
 
 PYBIND11_MODULE(core, m) {
     m.doc() = "core";
@@ -33,4 +34,5 @@ PYBIND11_MODULE(core, m) {
     define_input(m);
     define_graph_constraints(m);
     define_transformation(m);
+    define_sparse_model_simulator(m);
 }