Added scheduler classes. Added method to model classes that applies a scheduler.

Former-commit-id: 73a4be11b2

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -1268,7 +1268,7 @@ namespace storm {
             static storm::storage::VectorSet<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
 #ifdef STORM_HAVE_GUROBI
                 // (0) Check whether the MDP is indeed labeled.
-                if (!labeledMdp.hasChoiceLabels()) {
+                if (!labeledMdp.hasChoiceLabeling()) {
                     throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model.";
                 }
                 

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1447,7 +1447,7 @@ namespace storm {
                 storm::utility::ir::defineUndefinedConstants(program, constantDefinitionString);
 
                 // (0) Check whether the MDP is indeed labeled.
-                if (!labeledMdp.hasChoiceLabels()) {
+                if (!labeledMdp.hasChoiceLabeling()) {
                     throw storm::exceptions::InvalidArgumentException() << "Minimal command set generation is impossible for unlabeled model.";
                 }
                 

src/models/AbstractModel.h

@@ -9,6 +9,7 @@
 #include "src/models/AtomicPropositionsLabeling.h"
 #include "src/storage/BitVector.h"
 #include "src/storage/SparseMatrix.h"
+#include "src/storage/Scheduler.h"
 #include "src/storage/VectorSet.h"
 #include "src/utility/Hash.h"
 
@@ -403,7 +404,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * Retrieves whether this model has a labeling for the choices.
          * @return True if this model has a labeling.
          */
-        bool hasChoiceLabels() const {
+        bool hasChoiceLabeling() const {
             return choiceLabeling;
         }
 
@@ -459,6 +460,15 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		 * @return void
 		 */
 		virtual void setStateIdBasedChoiceLabeling() = 0;
+    
+        /*
+         * Applies the given scheduler to the model.
+         *
+         * @param scheduler The scheduler to apply.
+         * @return The model resulting from applying the scheduler to the model.
+         */
+        virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const = 0;
+    
 protected:
         /*!
          * Exports the model to the dot-format and prints the result to the given stream.

src/models/AbstractNondeterministicModel.h

@@ -1,10 +1,11 @@
 #ifndef STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_
 #define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_
 
-#include "AbstractModel.h"
-
 #include <memory>
 
+#include "AbstractModel.h"
+#include "src/storage/Scheduler.h"
+
 namespace storm {
     namespace models {
         
@@ -235,7 +236,7 @@ namespace storm {
     
                 this->choiceLabeling.reset(newChoiceLabeling);
             }
-                        
+        
         private:
             /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
             std::vector<uint_fast64_t> nondeterministicChoiceIndices;

src/models/Ctmc.h

@@ -86,6 +86,17 @@ public:
 	virtual std::size_t getHash() const override {
 		return AbstractDeterministicModel<T>::getHash();
 	}
+    
+    virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
+    std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
+    for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
+        nondeterministicChoiceIndices[state] = state;
+    }
+    nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
+    storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler);
+    
+    return std::shared_ptr<AbstractModel<T>>(new Ctmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() :  boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>()));
+}
 };
 
 } // namespace models

src/models/Ctmdp.h

@@ -115,6 +115,18 @@ public:
 		return AbstractNondeterministicModel<T>::getHash();
 	}
 
+    virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
+        storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler);
+    
+        // Construct the new nondeterministic choice indices for the resulting matrix.
+        std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
+        for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
+            nondeterministicChoiceIndices[state] = state;
+        }
+        nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
+        return std::shared_ptr<AbstractModel<T>>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() :  boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>()));
+    }
+    
 private:
 
 	/*!

src/models/Dtmc.h

@@ -19,6 +19,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/settings/Settings.h"
 #include "src/utility/vector.h"
+#include "src/utility/matrix.h"
 
 namespace storm {
 
@@ -276,7 +277,7 @@ public:
 		}
 
 		boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> newChoiceLabels;
-		if(this->hasChoiceLabels()) {
+		if(this->hasChoiceLabeling()) {
 
 			// Get the choice label sets and move the needed values to the front.
 			std::vector<storm::storage::VectorSet<uint_fast64_t>> newChoice(this->getChoiceLabeling());
@@ -299,6 +300,17 @@ public:
 
 	}
 
+    virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
+        std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
+        for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
+            nondeterministicChoiceIndices[state] = state;
+        }
+        nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
+        storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler);
+    
+        return std::shared_ptr<AbstractModel<T>>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() :  boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>()));
+    }
+
 private:
 	/*!
 	 *	@brief Perform some sanity checks.

src/models/Mdp.h

@@ -18,6 +18,7 @@
 #include "src/settings/Settings.h"
 #include "src/models/AbstractNondeterministicModel.h"
 #include "src/utility/set.h"
+#include "src/utility/matrix.h"
 
 namespace storm {
 
@@ -136,7 +137,7 @@ public:
      */
     Mdp<T> restrictChoiceLabels(storm::storage::VectorSet<uint_fast64_t> const& enabledChoiceLabels) const {
         // Only perform this operation if the given model has choice labels.
-        if (!this->hasChoiceLabels()) {
+        if (!this->hasChoiceLabeling()) {
             throw storm::exceptions::InvalidArgumentException() << "Restriction to label set is impossible for unlabeled model.";
         }
         
@@ -192,6 +193,18 @@ public:
 		return AbstractNondeterministicModel<T>::getHash();
 	}
     
+    virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
+        storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler);
+    
+        // Construct the new nondeterministic choice indices for the resulting matrix.
+        std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
+        for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
+            nondeterministicChoiceIndices[state] = state;
+        }
+        nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
+        return std::shared_ptr<AbstractModel<T>>(new Mdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() :  boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>()));
+    }
+    
 private:
 
 	/*!

src/storage/PartialScheduler.cpp

@@ -0,0 +1,24 @@
+#include "src/storage/PartialScheduler.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace storage {
+        
+        void PartialScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) {
+            choices[state] = choice;
+        }
+        
+        bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const {
+            return choices.find(state) != choices.end();
+        }
+        
+        uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const {
+            auto stateChoicePair = choices.find(state);
+            
+            if (stateChoicePair == choices.end()) {
+                throw storm::exceptions::InvalidArgumentException() << "Scheduler does not define a choice for state " << state;
+            }
+        }
+        
+    } // namespace storage
+} // namespace storm

src/storage/PartialScheduler.h

@@ -0,0 +1,24 @@
+#ifndef STORM_STORAGE_PARTIALSCHEDULER_H_
+#define STORM_STORAGE_PARTIALSCHEDULER_H_
+
+#include "src/storage/Scheduler.h"
+
+namespace storm {
+    namespace storage {
+        
+        class PartialScheduler : public Scheduler {
+        public:
+            void setChoice(uint_fast64_t state, uint_fast64_t choice) override;
+            
+            bool isChoiceDefined(uint_fast64_t state) const override;
+            
+            uint_fast64_t getChoice(uint_fast64_t state) const override;
+            
+        private:
+            // A mapping from all states that have defined choices to their respective choices.
+            std::unsorted_map<uint_fast64_t, uint_fast64_t> choices;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PARTIALSCHEDULER_H_ */

src/storage/Scheduler.h

@@ -0,0 +1,36 @@
+#ifndef STORM_STORAGE_SCHEDULER_H_
+#define STORM_STORAGE_SCHEDULER_H_
+
+namespace storm {
+    namespace storage {
+        
+        /*
+         * This class is the abstract base class of all scheduler classes. Scheduler classes define which action is chosen in a particular state of a non-deterministic model.
+         */
+        class Scheduler {
+        public:
+            /*
+             * Sets the choice defined by the scheduler for the given state.
+             *
+             * @param state The state for which to set the choice.
+             * @param choice The choice to set for the given state.
+             */
+            virtual void setChoice(uint_fast64_t state, uint_fast64_t choice) = 0;
+            
+            /*
+             * Retrieves whether this scheduler defines a choice for the given state.
+             *
+             * @param state The state for which to check whether the scheduler defines a choice.
+             * @return True if the scheduler defines a choice for the given state.
+             */
+            virtual bool isChoiceDefined(uint_fast64_t state) const = 0;
+            
+            /*!
+             * Retrieves the choice for the given state under the assumption that the scheduler defines a proper choice for the state.
+             */
+            virtual uint_fast64_t getChoice(uint_fast64_t state) const = 0;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_SCHEDULER_H_ */

src/storage/TotalScheduler.cpp

@@ -0,0 +1,21 @@
+#include "src/storage/TotalScheduler.h"
+
+namespace storm {
+    namespace storage {
+        TotalScheduler::TotalScheduler(uint_fast64_t numberOfStates) : choices(numberOfStates) {
+            // Intentionally left empty.
+        }
+        
+        void setChoice(uint_fast64_t state, uint_fast64_t choice) override {
+            choices[state] = choice;
+        }
+        
+        bool isChoiceDefined(uint_fast64_t state) const override {
+            return true;
+        }
+        
+        uint_fast64_t getChoice(uint_fast64_t state) const override {
+            return choices[state];
+        }
+    }
+}

src/storage/TotalScheduler.h

@@ -0,0 +1,26 @@
+#ifndef STORM_STORAGE_TOTALSCHEDULER_H_
+#define STORM_STORAGE_TOTALSCHEDULER_H_
+
+#include "src/storage/Scheduler.h"
+
+namespace storm {
+    namespace storage {
+        
+        class TotalScheduler : public Scheduler {
+        public:
+            TotalScheduler(uint_fast64_t numberOfStates);
+            
+            void setChoice(uint_fast64_t state, uint_fast64_t choice) override;
+            
+            bool isChoiceDefined(uint_fast64_t state) const override;
+            
+            uint_fast64_t getChoice(uint_fast64_t state) const override;
+            
+        private:
+            // A vector that stores the choice for each state.
+            std::vector<uint_fast64_t> choices;
+        };
+    } // namespace storage
+} // namespace storm
+
+#endif /* STORM_STORAGE_TOTALSCHEDULER_H_ */

src/utility/matrix.h

@@ -0,0 +1,52 @@
+#ifndef STORM_UTILITY_MATRIX_H_
+#define STORM_UTILITY_MATRIX_H_
+
+#include "src/storage/SparseMatrix.h"
+#include "src/storage/Scheduler.h"
+#include "src/exceptions/InvalidStateException.h"
+
+namespace storm {
+    namespace utility {
+        namespace matrix {
+            
+            /*!
+             * Applies the given scheduler to the given transition matrix. This means that all choices that are not taken by the scheduler are
+             * dropped from the transition matrix. If a state has no choice enabled, it is equipped with a self-loop instead.
+             *
+             * @param transitionMatrix The transition matrix of the original system.
+             * @param nondeterministicChoiceIndices A vector indicating at which rows the choices for the states begin.
+             * @param scheduler The scheduler to apply to the system.
+             * @return A transition matrix that corresponds to all transitions of the given system that are selected by the given scheduler.
+             */
+            template <typename T>
+            storm::storage::SparseMatrix<T> applyScheduler(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::Scheduler const& scheduler) {
+                storm::storage::SparseMatrix<T> result(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount());
+                
+                for (uint_fast64_t state = 0; state < nondeterministicChoiceIndices.size() - 1; ++state) {
+                    if (scheduler.isChoiceDefined(state)) {
+                        // Check whether the choice is valid for this state.
+                        uint_fast64_t choice = nondeterministicChoiceIndices[state] + scheduler.getChoice(state);
+                        if (choice >= nondeterministicChoiceIndices[state + 1]) {
+                            throw storm::exceptions::InvalidStateException() << "Scheduler defines illegal choice " << choice << " for state " << state << ".";
+                        }
+                        
+                        // If a valid choice for this state is defined, we copy over the corresponding entries.
+                        typename storm::storage::SparseMatrix<T>::Rows selectedRow = transitionMatrix.getRow(choice);
+                        for (auto entry : selectedRow) {
+                            result.insertNextValue(state, entry.column(), entry.value());
+                        }
+                    } else {
+                        // If no valid choice for the state is defined, we insert a self-loop.
+                        result.insertNextValue(state, state, storm::utility::constGetOne<T>());
+                    }
+                }
+                
+                // Finalize the matrix creation and return result.
+                result.finalize();
+                return result;
+            }
+        }
+    }
+}
+
+#endif /* STORM_UTILITY_MATRIX_H_ */