diff --git a/src/models/AbstractNonDeterministicModel.h b/src/models/AbstractNondeterministicModel.h
similarity index 65%
rename from src/models/AbstractNonDeterministicModel.h
rename to src/models/AbstractNondeterministicModel.h
index 257644093..0ca1dea37 100644
--- a/src/models/AbstractNonDeterministicModel.h
+++ b/src/models/AbstractNondeterministicModel.h
@@ -16,7 +16,7 @@ namespace models {
* This is base class defines a common interface for all non-deterministic models.
*/
template<class T>
-class AbstractNonDeterministicModel: public AbstractModel<T> {
+class AbstractNondeterministicModel: public AbstractModel<T> {
public:
/*! Constructs an abstract non-determinstic model from the given parameters.
@@ -27,27 +27,27 @@ class AbstractNonDeterministicModel: public AbstractModel<T> {
* @param stateRewardVector The reward values associated with the states.
* @param transitionRewardMatrix The reward values associated with the transitions of the model.
*/
- AbstractNonDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+ AbstractNondeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
- std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
+ std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices,
std::shared_ptr<std::vector<T>> stateRewardVector,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix),
- choiceIndices(choiceIndices) {
+ nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
}
/*!
* Destructor.
*/
- virtual ~AbstractNonDeterministicModel() {
+ virtual ~AbstractNondeterministicModel() {
// Intentionally left empty.
}
/*!
* Copy Constructor.
*/
- AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel<T>(other),
- choiceIndices(other.choiceIndices) {
+ AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel<T>(other),
+ nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) {
// Intentionally left empty.
}
@@ -57,12 +57,22 @@ class AbstractNonDeterministicModel: public AbstractModel<T> {
* measured in bytes.
*/
virtual uint_fast64_t getSizeInMemory() const {
- return AbstractModel<T>::getSizeInMemory() + choiceIndices->size() * sizeof(uint_fast64_t);
+ return AbstractModel<T>::getSizeInMemory() + nondeterministicChoiceIndices->size() * sizeof(uint_fast64_t);
+ }
+
+ /*!
+ * Retrieves the vector indicating which matrix rows represent non-deterministic choices
+ * of a certain state.
+ * @param the vector indicating which matrix rows represent non-deterministic choices
+ * of a certain state.
+ */
+ std::shared_ptr<std::vector<uint_fast64_t>> getNondeterministicChoiceIndices() const {
+ return nondeterministicChoiceIndices;
}
private:
/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
- std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
+ std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;
};
} // namespace models
diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h
index 3e1f8f5b8..e693c70a1 100644
--- a/src/models/Ctmdp.h
+++ b/src/models/Ctmdp.h
@@ -12,7 +12,7 @@
#include <vector>
#include "AtomicPropositionsLabeling.h"
-#include "AbstractNonDeterministicModel.h"
+#include "AbstractNondeterministicModel.h"
#include "src/storage/SparseMatrix.h"
#include "src/utility/Settings.h"
@@ -25,7 +25,7 @@ namespace models {
* labeled with atomic propositions.
*/
template <class T>
-class Ctmdp : public storm::models::AbstractNonDeterministicModel<T> {
+class Ctmdp : public storm::models::AbstractNondeterministicModel<T> {
public:
//! Constructor
@@ -42,7 +42,7 @@ public:
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
- : AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
+ : AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -54,7 +54,7 @@ public:
* Copy Constructor. Performs a deep copy of the given CTMDP.
* @param ctmdp A reference to the CTMDP that is to be copied.
*/
- Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNonDeterministicModel<T>(ctmdp) {
+ Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNondeterministicModel<T>(ctmdp) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index dc92dfda6..515a1842e 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -16,7 +16,7 @@
#include "AtomicPropositionsLabeling.h"
#include "src/storage/SparseMatrix.h"
#include "src/utility/Settings.h"
-#include "src/models/AbstractNonDeterministicModel.h"
+#include "src/models/AbstractNondeterministicModel.h"
namespace storm {
@@ -27,7 +27,7 @@ namespace models {
* labeled with atomic propositions.
*/
template <class T>
-class Mdp : public storm::models::AbstractNonDeterministicModel<T> {
+class Mdp : public storm::models::AbstractNondeterministicModel<T> {
public:
//! Constructor
@@ -44,7 +44,7 @@ public:
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
- : AbstractNonDeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
+ : AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -56,7 +56,7 @@ public:
* Copy Constructor. Performs a deep copy of the given MDP.
* @param mdp A reference to the MDP that is to be copied.
*/
- Mdp(const Mdp<T> &mdp) : AbstractNonDeterministicModel<T>(mdp) {
+ Mdp(const Mdp<T> &mdp) : AbstractNondeterministicModel<T>(mdp) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h
index d7337ae54..f7331da7e 100644
--- a/src/parser/AutoParser.h
+++ b/src/parser/AutoParser.h
@@ -7,7 +7,7 @@
#include "src/exceptions/WrongFileFormatException.h"
#include "src/models/AbstractModel.h"
#include "src/parser/DeterministicModelParser.h"
-#include "src/parser/NonDeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
#include <memory>
#include <iostream>
@@ -57,12 +57,12 @@ class AutoParser : Parser {
break;
}
case storm::models::MDP: {
- NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+ NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser.getMdp();
break;
}
case storm::models::CTMDP: {
- NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+ NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser.getCtmdp();
break;
}
diff --git a/src/parser/NonDeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
similarity index 87%
rename from src/parser/NonDeterministicModelParser.cpp
rename to src/parser/NondeterministicModelParser.cpp
index 017d3b31e..036f0dc9b 100644
--- a/src/parser/NonDeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -10,7 +10,7 @@
#include <string>
#include <vector>
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
+#include "src/parser/NondeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h"
@@ -27,9 +27,9 @@ namespace parser {
* @param stateRewardFile String containing the location of the state reward file (...srew)
* @param transitionRewardFile String containing the location of the transition reward file (...trew)
*/
-NonDeterministicModelParser::NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
- storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile);
+ storm::parser::NondeterministicSparseTransitionParser tp(transitionSystemFile);
uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
@@ -38,7 +38,7 @@ NonDeterministicModelParser::NonDeterministicModelParser(std::string const & tra
this->stateRewards = srp.getStateRewards();
}
if (transitionRewardFile != "") {
- storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile);
+ storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile);
this->transitionRewardMatrix = trp.getMatrix();
}
diff --git a/src/parser/NonDeterministicModelParser.h b/src/parser/NondeterministicModelParser.h
similarity index 93%
rename from src/parser/NonDeterministicModelParser.h
rename to src/parser/NondeterministicModelParser.h
index 379fdf07c..bdc4c42d4 100644
--- a/src/parser/NonDeterministicModelParser.h
+++ b/src/parser/NondeterministicModelParser.h
@@ -13,6 +13,7 @@
#include "src/models/Ctmdp.h"
namespace storm {
+
namespace parser {
/*!
@@ -23,9 +24,9 @@ namespace parser {
*
* @note The labeling representation in the file may use at most as much nodes as are specified in the mdp.
*/
-class NonDeterministicModelParser: public storm::parser::Parser {
+class NondeterministicModelParser: public storm::parser::Parser {
public:
- NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+ NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
std::shared_ptr<storm::models::Mdp<double>> getMdp() {
@@ -58,5 +59,7 @@ private:
};
} /* namespace parser */
+
} /* namespace storm */
+
#endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */
diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
similarity index 97%
rename from src/parser/NonDeterministicSparseTransitionParser.cpp
rename to src/parser/NondeterministicSparseTransitionParser.cpp
index 26436fb55..a17f48552 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -5,7 +5,7 @@
* Author: Gereon Kremer
*/
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
+#include "src/parser/NondeterministicSparseTransitionParser.h"
#include <errno.h>
#include <time.h>
@@ -49,7 +49,7 @@ namespace parser {
* @param maxnode Is set to highest id of all nodes.
* @return The number of non-zero elements.
*/
-uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
+uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
/*
* Check file header and extract number of transitions.
*/
@@ -154,7 +154,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
* @return a pointer to the created sparse matrix.
*/
-NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename)
+NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename)
: matrix(nullptr) {
/*
* Enforce locale where decimal point is '.'.
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h
similarity index 88%
rename from src/parser/NonDeterministicSparseTransitionParser.h
rename to src/parser/NondeterministicSparseTransitionParser.h
index a0d9ea50a..209c0e7a0 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NondeterministicSparseTransitionParser.h
@@ -17,9 +17,9 @@ namespace parser {
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
*/
-class NonDeterministicSparseTransitionParser : public Parser {
+class NondeterministicSparseTransitionParser : public Parser {
public:
- NonDeterministicSparseTransitionParser(std::string const &filename);
+ NondeterministicSparseTransitionParser(std::string const &filename);
inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
return this->matrix;
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index 3464c9710..4b1db5178 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -9,7 +9,7 @@
#define STORM_UTILITY_GRAPHANALYZER_H_
#include "src/models/AbstractDeterministicModel.h"
-#include "src/models/AbstractNonDeterministicModel.h"
+#include "src/models/AbstractNondeterministicModel.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "log4cplus/logger.h"
@@ -149,7 +149,7 @@ public:
}
template <class T>
- static void performProb01Max(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+ static void performProb01Max(storm::models::AbstractNondeterministicModel<T>& 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.");
@@ -166,17 +166,47 @@ public:
}
template <class T>
- static void performProb0A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+ static void performProb0A(storm::models::AbstractNondeterministicModel<T>& 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.");
+ }
+
+ // 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;
+
+ // Initialize the stack used for the DFS with the states
+ std::vector<uint_fast64_t> stack;
+ stack.reserve(model.getNumberOfStates());
+ psiStates.getList(stack);
+ // Perform the actual DFS.
+ 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);
+ stack.push_back(*it);
+ }
+ }
+ }
+
+ statesWithProbability0->complement();
}
template <class T>
- static void performProb1E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+ static void performProb1E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
}
template <class T>
- static void performProb01Min(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+ static void performProb01Min(storm::models::AbstractNondeterministicModel<T>& 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.");
@@ -193,12 +223,12 @@ public:
}
template <class T>
- static void performProb0E(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+ static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
}
template <class T>
- static void performProb1A(storm::models::AbstractNonDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+ static void performProb1A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
// This result is a rough guess and does not compute all states with probability 1.
// TODO: Check whether it makes sense to implement the precise but complicated algorithm here.
*statesWithProbability1 = psiStates;
diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp
index 0dd6a4e3b..02302dc2a 100644
--- a/test/parser/ParseMdpTest.cpp
+++ b/test/parser/ParseMdpTest.cpp
@@ -8,12 +8,12 @@
#include "gtest/gtest.h"
#include "storm-config.h"
-#include "src/parser/NonDeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
#include "src/utility/IoUtility.h"
TEST(ParseMdpTest, parseAndOutput) {
- storm::parser::NonDeterministicModelParser* mdpParser = nullptr;
- ASSERT_NO_THROW(mdpParser = new storm::parser::NonDeterministicModelParser(
+ storm::parser::NondeterministicModelParser* mdpParser = nullptr;
+ ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp
index 6a20050dd..69d11cc37 100644
--- a/test/storage/SparseMatrixTest.cpp
+++ b/test/storage/SparseMatrixTest.cpp
@@ -80,7 +80,7 @@ TEST(SparseMatrixTest, Test) {
int position_row[50] = {
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, /* first row empty, one full row ��������� 25 minus the diagonal entry */
+ 2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */
4, 4, /* one empty row, then first and last column */
13, 13, 13, 13, /* a few empty rows, middle columns */
24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
@@ -288,9 +288,9 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
- const std::vector<uint_fast64_t> rowP = ssm->getRowIndicationsPointer();
- const std::vector<uint_fast64_t> colP = ssm->getColumnIndicationsPointer();
- const std::vector<int> valP = ssm->getStoragePointer();
+ const std::vector<uint_fast64_t> rowP = ssm->getRowIndications();
+ const std::vector<uint_fast64_t> colP = ssm->getColumnIndications();
+ const std::vector<int> valP = ssm->getStorage();
int target = -1;
for (auto &coeff: tripletList) {