diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h
index 6cbdd5aa3..a6d132745 100644
--- a/src/modelchecker/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h
@@ -211,9 +211,12 @@ public:
// Then, we need to identify the states which have to be taken out of the matrix, i.e.
// all states that have probability 0 and 1 of satisfying the until-formula.
- storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
- storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
- storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates);
+ storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
+ storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
+
+ std::cout << statesWithProbability0.toString() << std::endl;
+ std::cout << statesWithProbability1.toString() << std::endl;
// Delete intermediate results that are obsolete now.
delete leftStates;
@@ -360,7 +363,7 @@ public:
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
- storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates);
+ storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, infinityStates);
infinityStates.complement();
// Create resulting vector.
diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h
index e31212e36..50b20c81d 100644
--- a/src/modelchecker/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/SparseMdpPrctlModelChecker.h
@@ -216,9 +216,9 @@ public:
storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
if (this->minimumOperatorStack.top()) {
- storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
+ storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, statesWithProbability0, statesWithProbability1);
} else {
- storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
+ storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, statesWithProbability0, statesWithProbability1);
}
// Delete sub-results that are obsolete now.
@@ -359,9 +359,9 @@ public:
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
if (this->minimumOperatorStack.top()) {
- storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates, &infinityStates);
+ storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates, infinityStates);
} else {
- storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates, &infinityStates);
+ storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates, infinityStates);
}
infinityStates.complement();
diff --git a/src/utility/CommandLine.h b/src/utility/CommandLine.h
index 04599348d..134706ec2 100644
--- a/src/utility/CommandLine.h
+++ b/src/utility/CommandLine.h
@@ -13,7 +13,7 @@ namespace storm {
namespace utility {
/*!
- * Prints a separation line on the command line.
+ * Prints a separating line to the standard output.
*/
void printSeparationLine(std::ostream& out);
diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h
index fdc7762a5..ea65ab03a 100644
--- a/src/utility/ErrorHandling.h
+++ b/src/utility/ErrorHandling.h
@@ -12,12 +12,19 @@
#include <execinfo.h>
#include <cxxabi.h>
-std::string demangle(const char* symbol) {
+/*
+ * Demangles the given string. This is needed for the correct display of backtraces.
+ *
+ * @param symbol The name of the symbol that is to be demangled.
+ */
+std::string demangle(char const* symbol) {
int status;
- // Attention: sscanf format strings rely on size being 128
+
+ // Attention: sscanf format strings rely on the size being 128.
char temp[128];
char* demangled;
- // Check for C++ symbol
+
+ // Check for C++ symbol.
if (sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp) == 1) {
if (NULL != (demangled = abi::__cxa_demangle(temp, NULL, NULL, &status))) {
std::string result(demangled);
@@ -25,37 +32,49 @@ std::string demangle(const char* symbol) {
return result;
}
}
- // Check for C symbol
+ // Check for C symbol.
if (sscanf(symbol, "%127s", temp) == 1) {
return temp;
}
- // Return plain symbol
+
+ // Return plain symbol if none of the above cases matched.
return symbol;
}
+/*
+ * Handles the given signal. This will display the received signal and a backtrace.
+ *
+ * @param sig The code of the signal that needs to be handled.
+ */
void signalHandler(int sig) {
#define SIZE 128
- LOG4CPLUS_FATAL(logger, "We recieved a segfault. To start with, here is a backtrace.");
+ LOG4CPLUS_FATAL(logger, "The program received signal " << sig << ". The following backtrace shows the status upon reception of the signal.");
void *buffer[SIZE];
char **strings;
int nptrs;
nptrs = backtrace(buffer, SIZE);
+ // Try to retrieve the backtrace symbols.
strings = backtrace_symbols(buffer, nptrs);
if (strings == nullptr) {
- std::cerr << "Obtaining the backtrace symbols failed. Well, shit." << std::endl;
+ std::cerr << "Obtaining the backtrace symbols failed." << std::endl;
exit(2);
}
- // j = 2: skip the handler itself.
+
+ // Starting this for-loop at j=2 means that we skip the handler itself. Currently this is not
+ // done.
for (int j = 1; j < nptrs; j++) {
LOG4CPLUS_FATAL(logger, nptrs-j << ": " << demangle(strings[j]));
}
free(strings);
- LOG4CPLUS_FATAL(logger, "That's all we can do. Bye.");
+ LOG4CPLUS_FATAL(logger, "Exiting.");
exit(2);
}
+/*
+ * Registers some signal handlers so that we can display a backtrace upon erroneuous termination.
+ */
void installSignalHandler() {
signal(SIGSEGV, signalHandler);
}
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index 5bbb4295c..573d2baa6 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -26,73 +26,63 @@ public:
/*!
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
* deterministic model.
+ *
* @param model The model whose graph structure to search.
* @param phiStates The set of all states satisfying phi.
* @param psiStates The set of all states satisfying psi.
- * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will contain all states with
- * probability 0 after the invocation of the function.
- * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will contain all states with
- * probability 1 after the invocation of the function.
+ * @return A pair of bit vectors such that the first bit vector stores the indices of all states
+ * with probability 0 and the second stores all indices of states with probability 1.
*/
template <typename T>
- static void performProb01(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
- // Check for valid parameters.
- if (statesWithProbability0 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
- }
- if (statesWithProbability1 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
- }
-
- // Perform the actual search.
- GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbability0);
- GraphAnalyzer::performProb1(model, phiStates, psiStates, *statesWithProbability0, statesWithProbability1);
- statesWithProbability0->complement();
+ static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
+ result.first = GraphAnalyzer::performProbGreater0(model, phiStates, psiStates);
+ result.second = GraphAnalyzer::performProb1(model, phiStates, psiStates, result.first);
+ result.first.complement();
+ return result;
}
/*!
- * Performs a backwards depth-first search trough the underlying graph structure
+ * Performs a backwards breadt-first search trough the underlying graph structure
* of the given model to determine which states of the model have a positive probability
* of satisfying phi until psi. The resulting states are written to the given bit vector.
- * @param model The model whose graph structure to search.
+ *
+ * @param model The model whose graph structure to search.
* @param phiStates A bit vector of all states satisfying phi.
* @param psiStates A bit vector of all states satisfying psi.
- * @param statesWithProbabilityGreater0 A pointer to the result of the search for states that possess
- * a positive probability of satisfying phi until psi.
+ * @return A bit vector with all indices of states that have a probability greater than 0.
*/
template <typename T>
- static void performProbGreater0(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
- // Check for valid parameter.
- if (statesWithProbabilityGreater0 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbabilityGreater0' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbabilityGreater0' must not be null.");
- }
-
+ static storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ // Prepare the resulting bit vector.
+ storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
+
// Get the backwards transition relation from the model to ease the search.
storm::models::GraphTransitions<T> backwardTransitions(*model.getTransitionMatrix(), false);
// Add all psi states as the already satisfy the condition.
- *statesWithProbabilityGreater0 |= psiStates;
+ statesWithProbabilityGreater0 |= psiStates;
- // Initialize the stack used for the DFS with the states
+ // Initialize the stack used for the BFS with the states.
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
- psiStates.addSetIndicesToList(stack);
+ psiStates.addSetIndicesToVector(stack);
- // Perform the actual DFS.
+ // Perform the actual BFS.
while(!stack.empty()) {
uint_fast64_t currentState = stack.back();
stack.pop_back();
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
- if (phiStates.get(*it) && !statesWithProbabilityGreater0->get(*it)) {
- statesWithProbabilityGreater0->set(*it, true);
+ if (phiStates.get(*it) && !statesWithProbabilityGreater0.get(*it)) {
+ statesWithProbabilityGreater0.set(*it, true);
stack.push_back(*it);
}
}
}
+
+ // Return result.
+ return statesWithProbabilityGreater0;
}
/*!
@@ -101,24 +91,19 @@ public:
* before. In order to do this, it uses the given set of states that
* characterizes the states that possess at least one path to a target state.
* The results are written to the given bit vector.
+ *
* @param model The model whose graph structure to search.
* @param phiStates A bit vector of all states satisfying phi.
* @param psiStates A bit vector of all states satisfying psi.
* @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive
* probability mass of satisfying phi until psi.
- * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
- * have paths satisfying phi until psi.
+ * @return A bit vector with all indices of states that have a probability greater than 1.
*/
template <typename T>
- static void performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) {
- // Check for valid parameter.
- if (statesWithProbability1 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
- }
-
- GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0, statesWithProbability1);
- statesWithProbability1->complement();
+ static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) {
+ storm::storage::BitVector statesWithProbability1 = GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0);
+ statesWithProbability1.complement();
+ return statesWithProbability1;
}
/*!
@@ -127,87 +112,97 @@ public:
* before. In order to do this, it uses the given set of states that
* characterizes the states that possess at least one path to a target state.
* The results are written to the given bit vector.
+ *
* @param model The model whose graph structure to search.
* @param phiStates A bit vector of all states satisfying phi.
* @param psiStates A bit vector of all states satisfying psi.
- * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
- * have paths satisfying phi until psi.
+ * @return A bit vector with all indices of states that have a probability greater than 1.
*/
template <typename T>
- static void performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
- // Check for valid parameter.
- if (statesWithProbability1 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
- }
-
- storm::storage::BitVector* statesWithProbabilityGreater0 = new storm::storage::BitVector(model.getNumberOfStates());
- GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbabilityGreater0);
- GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(*statesWithProbabilityGreater0), statesWithProbability1);
- delete statesWithProbabilityGreater0;
- statesWithProbability1->complement();
+ static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
+ storm::storage::BitVector statesWithProbability1(model.getNumberOfStates());
+ GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbabilityGreater0);
+ GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0), statesWithProbability1);
+ statesWithProbability1.complement();
+ return statesWithProbability1;
}
+ /*!
+ * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi
+ * until psi in a non-deterministic model in which all non-deterministic choices are resolved
+ * such that the probability is maximized.
+ *
+ * @param model The model whose graph structure to search.
+ * @param phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 0 after the invocation of the function.
+ * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 1 after the invocation of the function.
+ */
template <typename T>
- static void performProb01Max(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
- // Check for valid parameters.
- if (statesWithProbability0 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
- }
- if (statesWithProbability1 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
- }
-
- // Perform the actual search.
+ static void performProb01Max(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0, storm::storage::BitVector& statesWithProbability1) {
GraphAnalyzer::performProb0A(model, phiStates, psiStates, statesWithProbability0);
GraphAnalyzer::performProb1E(model, phiStates, psiStates, statesWithProbability1);
}
+ /*!
+ * Computes the sets of states that have probability 0 of satisfying phi until psi under all
+ * possible resolutions of non-determinism in a non-deterministic model. Stated differently,
+ * this means that these states have probability 0 of satisfying phi until psi even if the
+ * scheduler tries to maximize this probability.
+ *
+ * @param model The model whose graph structure to search.
+ * @param phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 0 after the invocation of the function.
+ */
template <typename T>
- static void performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
- // Check for valid parameter.
- if (statesWithProbability0 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
- }
-
+ static void performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0) {
// Get the backwards transition relation from the model to ease the search.
storm::models::GraphTransitions<T> backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false);
// Add all psi states as the already satisfy the condition.
- *statesWithProbability0 |= psiStates;
+ statesWithProbability0 |= psiStates;
- // Initialize the stack used for the DFS with the states
+ // Initialize the stack used for the BFS with the states
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
- psiStates.addSetIndicesToList(stack);
+ psiStates.addSetIndicesToVector(stack);
- // Perform the actual DFS.
+ // Perform the actual BFS.
while(!stack.empty()) {
uint_fast64_t currentState = stack.back();
stack.pop_back();
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
- if (phiStates.get(*it) && !statesWithProbability0->get(*it)) {
- statesWithProbability0->set(*it, true);
+ if (phiStates.get(*it) && !statesWithProbability0.get(*it)) {
+ statesWithProbability0.set(*it, true);
stack.push_back(*it);
}
}
}
- statesWithProbability0->complement();
+ // Finally, invert the computed set of states.
+ statesWithProbability0.complement();
}
+ /*!
+ * 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 phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 1 after the invocation of the function.
+ */
template <typename T>
- static void performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
- // Check for valid parameters.
- if (statesWithProbability1 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
- }
-
+ static void performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability1) {
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -220,11 +215,12 @@ public:
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
+ // Perform the loop as long as the set of states gets larger.
bool done = false;
while (!done) {
stack.clear();
storm::storage::BitVector* nextStates = new storm::storage::BitVector(psiStates);
- psiStates.addSetIndicesToList(stack);
+ psiStates.addSetIndicesToVector(stack);
while (!stack.empty()) {
uint_fast64_t currentState = stack.back();
@@ -265,35 +261,42 @@ public:
delete nextStates;
}
- *statesWithProbability1 = *currentStates;
+ statesWithProbability1 = *currentStates;
delete currentStates;
}
-
- template <typename T>
- static void performProb01Min(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
- // Check for valid parameters.
- if (statesWithProbability0 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
- }
- if (statesWithProbability1 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
- }
-
- // Perform the actual search.
+ /*!
+ * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi
+ * until psi in a non-deterministic model in which all non-deterministic choices are resolved
+ * such that the probability is minimized.
+ *
+ * @param model The model whose graph structure to search.
+ * @param phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 0 after the invocation of the function.
+ * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 1 after the invocation of the function.
+ */
+ template <typename T>
+ static void performProb01Min(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0, storm::storage::BitVector& statesWithProbability1) {
GraphAnalyzer::performProb0E(model, phiStates, psiStates, statesWithProbability0);
GraphAnalyzer::performProb1A(model, phiStates, psiStates, statesWithProbability1);
}
+ /*!
+ * Computes the sets of states that have probability 0 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 0 of satisfying phi until psi if the
+ * scheduler tries to minimize this probability.
+ *
+ * @param model The model whose graph structure to search.
+ * @param phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 0 after the invocation of the function.
+ */
template <typename T>
- static void performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
- // Check for valid parameter.
- if (statesWithProbability0 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
- }
-
+ static void performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0) {
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -302,12 +305,12 @@ public:
storm::models::GraphTransitions<T> backwardTransitions(*transitionMatrix, *nondeterministicChoiceIndices, false);
// Add all psi states as the already satisfy the condition.
- *statesWithProbability0 |= psiStates;
+ statesWithProbability0 |= psiStates;
// Initialize the stack used for the DFS with the states
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
- psiStates.addSetIndicesToList(stack);
+ psiStates.addSetIndicesToVector(stack);
// Perform the actual DFS.
while(!stack.empty()) {
@@ -315,14 +318,14 @@ public:
stack.pop_back();
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
- if (phiStates.get(*it) && !statesWithProbability0->get(*it)) {
+ if (phiStates.get(*it) && !statesWithProbability0.get(*it)) {
// Check whether the predecessor has at least one successor in the current state
// set for every nondeterministic choice.
bool addToStatesWithProbability0 = true;
for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) {
bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
for (auto colIt = transitionMatrix->constColumnIteratorBegin(*rowIt); colIt != transitionMatrix->constColumnIteratorEnd(*rowIt); ++colIt) {
- if (statesWithProbability0->get(*colIt)) {
+ if (statesWithProbability0.get(*colIt)) {
hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
break;
}
@@ -336,24 +339,30 @@ public:
// If we need to add the state, then actually add it and perform further search
// from the state.
if (addToStatesWithProbability0) {
- statesWithProbability0->set(*it, true);
+ statesWithProbability0.set(*it, true);
stack.push_back(*it);
}
}
}
}
- statesWithProbability0->complement();
+ statesWithProbability0.complement();
}
+ /*!
+ * Computes the sets of states that have probability 1 of satisfying phi until psi under all
+ * possible resolutions of non-determinism in a non-deterministic model. Stated differently,
+ * this means that these states have probability 1 of satisfying phi until psi even if the
+ * scheduler tries to minimize this probability.
+ *
+ * @param model The model whose graph structure to search.
+ * @param phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will
+ * contain all states with probability 1 after the invocation of the function.
+ */
template <typename T>
- static void performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
- // Check for valid parameters.
- if (statesWithProbability1 == nullptr) {
- LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
- throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
- }
-
+ static void performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability1) {
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -366,11 +375,12 @@ public:
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
+ // Perform the loop as long as the set of states gets smaller.
bool done = false;
while (!done) {
stack.clear();
storm::storage::BitVector* nextStates = new storm::storage::BitVector(psiStates);
- psiStates.addSetIndicesToList(stack);
+ psiStates.addSetIndicesToVector(stack);
while (!stack.empty()) {
uint_fast64_t currentState = stack.back();
@@ -411,10 +421,16 @@ public:
delete nextStates;
}
- *statesWithProbability1 = *currentStates;
+ statesWithProbability1 = *currentStates;
delete currentStates;
}
+ /*
+ * Performs a decomposition of the given matrix and vector indicating the nondeterministic
+ * choices into SCCs.
+ *
+ * @param
+ */
template <typename T>
static void performSccDecomposition(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents, storm::models::GraphTransitions<T>& stronglyConnectedComponentsDependencyGraph) {
LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");