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 + +void define_sparse_model_simulator(py::module& m) { + py::class_> dtsmsd(m, "_DiscreteTimeSparseModelSimulatorDouble", "Simulator for sparse discrete-time models in memory (ValueType = double)"); + dtsmsd.def(py::init const&>()); + dtsmsd.def("set_seed", &storm::simulator::DiscreteTimeSparseModelSimulator::setSeed, py::arg("seed")); + dtsmsd.def("step", &storm::simulator::DiscreteTimeSparseModelSimulator::step, py::arg("action")); + dtsmsd.def("get_current_state", &storm::simulator::DiscreteTimeSparseModelSimulator::getCurrentState); + dtsmsd.def("reset_to_initial_state", &storm::simulator::DiscreteTimeSparseModelSimulator::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); }