bugfixes for NondeterministicModel, improvements for StateActionPair, graph and initialize

Former-commit-id: 4531d784a1

src/models/sparse/NondeterministicModel.cpp

@@ -40,8 +40,8 @@ namespace storm {
             }
             
             template<typename ValueType>
-            uint_fast64_t getNumberOfChoices(uint_fast64_t state) const {
-                auto indices = this->getNondetermininisticChoiceIndices();
+            uint_fast64_t NondeterministicModel<ValueType>::getNumberOfChoices(uint_fast64_t state) const {
+                auto indices = this->getNondeterministicChoiceIndices();
                 return indices[state+1] - indices[state];
             }
             

src/storage/StateActionPair.h

@@ -36,7 +36,7 @@ namespace storm {
 namespace std {
     template<>
     struct hash<storm::storage::StateActionPair> {
-        size_t operator()(storm::storage::StateActionPair const& sap) {
+        size_t operator()(storm::storage::StateActionPair const& sap) const {
             return (sap.getState() << 3 ^ sap.getAction());
         }
     };

src/storage/StateActionTargetTuple.h

@@ -10,12 +10,16 @@ namespace storm {
             uint_fast64_t state;
             uint_fast64_t action;
             uint_fast64_t target;
-                
+            
         };
             
         inline std::string to_string(StateActionTarget const& sat) {
             return std::to_string(sat.state) + "_" + std::to_string(sat.action) + "_" + std::to_string(sat.target);
         }
+        
+        inline bool operator==(StateActionTarget const& sat1, StateActionTarget const& sat2) {
+            return sat1.state == sat2.state && sat1.action == sat2.action && sat1.target == sat2.target;
+        }
 
     }
 }

src/utility/graph.h

@@ -529,6 +529,23 @@ namespace storm {
                 return currentStates;
             }
             
+            /*!
+             * Computes the sets of states that have probability 1 of satisfying phi until psi under at least
+             * one possible resolution of non-determinism in a non-deterministic model. Stated differently,
+             * this means that these states have probability 1 of satisfying phi until psi if the
+             * scheduler tries to maximize this probability.
+             *
+             * @param model The model whose graph structure to search.
+             * @param backwardTransitions The reversed transition relation of the model.
+             * @param phiStates The set of all states satisfying phi.
+             * @param psiStates The set of all states satisfying psi.
+             * @return A bit vector that represents all states with probability 1.
+             */
+            template <typename T>
+            storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+                return performProb1E(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
+            }
+            
             template <typename T>
             std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
                 std::pair<storm::storage::BitVector, storm::storage::BitVector> result;

src/utility/initialize.cpp

@@ -1,6 +1,7 @@
 #include "initialize.h"
 
-#include "src/settings/SettingsManager.h"
+log4cplus::Logger logger;
+log4cplus::Logger printer;
 
 namespace storm {
     namespace utility {

src/utility/initialize.h

@@ -1,5 +1,5 @@
-#ifndef INITIALIZE_H
-#define	INITIALIZE_H
+#ifndef STORM_UTILITY_INITIALIZE_H
+#define	STORM_UTILITY_INITIALIZE_H
 
 
 
@@ -8,8 +8,10 @@
 #include "log4cplus/loggingmacros.h"
 #include "log4cplus/consoleappender.h"
 #include "log4cplus/fileappender.h"
-log4cplus::Logger logger;
-log4cplus::Logger printer;
+extern log4cplus::Logger logger;
+extern log4cplus::Logger printer;
+
+#include "src/settings/SettingsManager.h"
 
 
 namespace storm {