diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index 1810ffdec..860418f1e 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -40,8 +40,8 @@ namespace storm { } template - uint_fast64_t getNumberOfChoices(uint_fast64_t state) const { - auto indices = this->getNondetermininisticChoiceIndices(); + uint_fast64_t NondeterministicModel::getNumberOfChoices(uint_fast64_t state) const { + auto indices = this->getNondeterministicChoiceIndices(); return indices[state+1] - indices[state]; } diff --git a/src/storage/StateActionPair.h b/src/storage/StateActionPair.h index 09fede4a2..c567bfe14 100644 --- a/src/storage/StateActionPair.h +++ b/src/storage/StateActionPair.h @@ -36,7 +36,7 @@ namespace storm { namespace std { template<> struct hash { - size_t operator()(storm::storage::StateActionPair const& sap) { + size_t operator()(storm::storage::StateActionPair const& sap) const { return (sap.getState() << 3 ^ sap.getAction()); } }; diff --git a/src/storage/StateActionTargetTuple.h b/src/storage/StateActionTargetTuple.h index b354a30c6..8dff06918 100644 --- a/src/storage/StateActionTargetTuple.h +++ b/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; + } } } diff --git a/src/utility/graph.h b/src/utility/graph.h index fb8bdb158..4cb349a4e 100644 --- a/src/utility/graph.h +++ b/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 + storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + return performProb1E(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); + } + template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; diff --git a/src/utility/initialize.cpp b/src/utility/initialize.cpp index 7ca64f1d3..b0998972b 100644 --- a/src/utility/initialize.cpp +++ b/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 { diff --git a/src/utility/initialize.h b/src/utility/initialize.h index 4a848b89b..4a4680fe1 100644 --- a/src/utility/initialize.h +++ b/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 {