From 7a050434d9011e44f5866256704343fdb17b636f Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Mon, 27 Jul 2015 17:22:22 +0200
Subject: [PATCH] bugfixes for NondeterministicModel, improvements for
StateActionPair, graph and initialize
Former-commit-id: 4531d784a172f7fd3f17d024a572f3547614133e
---
src/models/sparse/NondeterministicModel.cpp | 4 ++--
src/storage/StateActionPair.h | 2 +-
src/storage/StateActionTargetTuple.h | 6 +++++-
src/utility/graph.h | 17 +++++++++++++++++
src/utility/initialize.cpp | 3 ++-
src/utility/initialize.h | 10 ++++++----
6 files changed, 33 insertions(+), 9 deletions(-)
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<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];
}
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<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());
}
};
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 <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;
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 {