From 1ef92dee9e3f883db1d3ca9a8c6581863ca15980 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sun, 12 Apr 2020 21:52:00 -0700
Subject: [PATCH] backbone for a simulator on top of explicit state models

---
 .../DiscreteTimeSparseModelSimulator.cpp      | 50 +++++++++++++++++++
 .../DiscreteTimeSparseModelSimulator.h        | 30 +++++++++++
 src/storm/utility/random.cpp                  | 24 +++++++++
 src/storm/utility/random.h                    | 29 +++++++++++
 4 files changed, 133 insertions(+)
 create mode 100644 src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp
 create mode 100644 src/storm/simulator/DiscreteTimeSparseModelSimulator.h
 create mode 100644 src/storm/utility/random.cpp
 create mode 100644 src/storm/utility/random.h

diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp
new file mode 100644
index 000000000..d8fd4a82a
--- /dev/null
+++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp
@@ -0,0 +1,50 @@
+#include "storm/simulator/DiscreteTimeSparseModelSimulator.h"
+#include "storm/models/sparse/Model.h"
+
+namespace storm {
+    namespace simulator {
+        template<typename ValueType, typename RewardModelType>
+        DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), currentState(*model.getInitialStates().begin()) {
+            STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits()==1, "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index.");
+
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        void DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::setSeed(uint64_t seed) {
+            generator = storm::utility::RandomProbabilityGenerator<double>(seed);
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        bool DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::step(uint64_t action) {
+            // TODO lots of optimization potential.
+            //  E.g., do not sample random numbers if there is only a single transition
+            ValueType probability = generator.random();
+            STORM_LOG_ASSERT(action < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions");
+            uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + action;
+            ValueType sum = storm::utility::zero<ValueType>();
+            for (auto const& entry : model.getTransitionMatrix().getRow(row)) {
+                sum += entry.getValue();
+                if (sum >= probability) {
+                    currentState = entry.getColumn();
+                    return true;
+                }
+            }
+            return false;
+            STORM_LOG_ASSERT(false, "This position should never be reached");
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        uint64_t DiscreteTimeSparseModelSimulator<ValueType, RewardModelType>::getCurrentState() const {
+            return currentState;
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        bool DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::resetToInitial() {
+            currentState = *model.getInitialStates().begin();
+            return true;
+        }
+
+
+        template class DiscreteTimeSparseModelSimulator<double>;
+    }
+}
\ No newline at end of file
diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.h b/src/storm/simulator/DiscreteTimeSparseModelSimulator.h
new file mode 100644
index 000000000..1637bffec
--- /dev/null
+++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.h
@@ -0,0 +1,30 @@
+#include <cstdint>
+#include "storm/models/sparse/Model.h"
+#include "storm/utility/random.h"
+
+namespace storm {
+    namespace simulator {
+
+        /**
+         * This class is a low-level interface to quickly sample from Discrete-Time Models
+         * stored explicitly as a SparseModel.
+         * Additional information about state, actions, should be obtained via the model itself.
+         *
+         * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such informations yourself.
+         * @tparam ModelType
+         */
+        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+        class DiscreteTimeSparseModelSimulator {
+        public:
+            DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> const& model);
+            void setSeed(uint64_t);
+            bool step(uint64_t action);
+            uint64_t getCurrentState() const;
+            bool resetToInitial();
+        protected:
+            uint64_t currentState;
+            storm::models::sparse::Model<ValueType, RewardModelType> const& model;
+            storm::utility::RandomProbabilityGenerator<ValueType> generator;
+        };
+    }
+}
\ No newline at end of file
diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp
new file mode 100644
index 000000000..6f3464cdb
--- /dev/null
+++ b/src/storm/utility/random.cpp
@@ -0,0 +1,24 @@
+#include "storm/utility/random.h"
+
+namespace storm {
+    namespace utility {
+        RandomProbabilityGenerator<double>::RandomProbabilityGenerator()
+        : distribution(0.0, 1.0)
+        {
+            std::random_device rd;
+            engine = std::mt19937(rd());
+        }
+
+        RandomProbabilityGenerator<double>::RandomProbabilityGenerator(uint64_t seed)
+        : engine(seed), distribution(0.0, 1.0)
+        {
+
+        }
+
+        double RandomProbabilityGenerator<double>::random() {
+            return distribution(engine);
+        }
+
+
+    }
+}
\ No newline at end of file
diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h
new file mode 100644
index 000000000..ef5b359df
--- /dev/null
+++ b/src/storm/utility/random.h
@@ -0,0 +1,29 @@
+#include <random>
+
+namespace storm {
+    namespace utility {
+        template<typename ValueType>
+        class RandomProbabilityGenerator {
+        public:
+            RandomProbabilityGenerator();
+            RandomProbabilityGenerator(uint64_t seed);
+            ValueType random() const;
+
+        };
+
+        template<>
+        class RandomProbabilityGenerator<double> {
+        public:
+            RandomProbabilityGenerator();
+            RandomProbabilityGenerator(uint64_t seed);
+            double random();
+        private:
+            std::uniform_real_distribution<double> distribution;
+            std::mt19937 engine;
+
+        };
+
+
+
+    }
+}
\ No newline at end of file