From ad660f0f98f561596acadf91bf868249b8b7002f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 11:09:13 +0200 Subject: [PATCH 1/7] more ifdefs for everyone Former-commit-id: f94a2c55bc6039955b83cbd8284f882003177969 --- src/storage/SparseMatrix.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 21ecfd931..20b7cd7f5 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1158,32 +1158,28 @@ namespace storm { } // Explicitly instantiate the entry, builder and the matrix. - //double + // double template class MatrixEntry::index_type, double>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - //float + // float template class MatrixEntry::index_type, float>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; - //int + // int template class MatrixEntry::index_type, int>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); - template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; #ifdef STORM_HAVE_CARL // Rat Function @@ -1193,8 +1189,12 @@ namespace storm { template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; // Intervals + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template class MatrixEntry::index_type, Interval>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; From 3ea084b77792f0bb0f01cb62116b95eb0b56ac69 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 11:15:49 +0200 Subject: [PATCH 2/7] included missing header Former-commit-id: 7e002652edd22ac99c380a30a5d823e1c1d21bac --- src/utility/graph.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index f48e6f5e2..b775c5b14 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -7,8 +7,10 @@ #include "src/storage/sparse/StateType.h" #include "src/models/symbolic/DeterministicModel.h" #include "src/models/symbolic/NondeterministicModel.h" +#include "src/models/symbolic/StandardRewardModel.h" #include "src/models/sparse/DeterministicModel.h" #include "src/models/sparse/NondeterministicModel.h" +#include "src/models/sparse/StandardRewardModel.h" #include "src/utility/constants.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/storage/dd/CuddBdd.h" From b418782bcd49aedb352b6ee47544b5eec4c2e552 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 11:23:04 +0200 Subject: [PATCH 3/7] added missing header Former-commit-id: b3b4deddb7068c929630727beb47d5e738c3c578 --- src/utility/graph.cpp | 220 +++++++++++++++++++++--------------------- src/utility/solver.h | 1 + 2 files changed, 111 insertions(+), 110 deletions(-) diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index b775c5b14..3e12abcd2 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -26,7 +26,7 @@ namespace storm { namespace utility { namespace graph { - template + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { storm::storage::BitVector reachableStates(initialStates); @@ -59,7 +59,7 @@ namespace storm { return reachableStates; } - template + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates) { std::vector distances(transitionMatrix.getRowGroupCount()); @@ -90,7 +90,7 @@ namespace storm { return distances; } - template + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { // Prepare the resulting bit vector. uint_fast64_t numberOfStates = phiStates.size(); @@ -146,14 +146,14 @@ namespace storm { return statesWithProbabilityGreater0; } - template + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0); statesWithProbability1.complement(); return statesWithProbability1; } - template + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(backwardTransitions, phiStates, psiStates); storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0)); @@ -161,7 +161,7 @@ namespace storm { return statesWithProbability1; } - template + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); @@ -171,7 +171,7 @@ namespace storm { return result; } - template + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; result.first = performProbGreater0(backwardTransitions, phiStates, psiStates); @@ -180,7 +180,7 @@ namespace storm { return result; } - template + template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); @@ -201,24 +201,24 @@ namespace storm { statesWithProbabilityGreater0 |= lastIterationStates; ++iterations; } - + return statesWithProbabilityGreater0; } - template + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0) { storm::dd::Bdd statesWithProbability1 = performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !statesWithProbabilityGreater0 && model.getReachableStates()); statesWithProbability1 = !statesWithProbability1 && model.getReachableStates(); return statesWithProbability1; } - template + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { storm::dd::Bdd statesWithProbabilityGreater0 = performProbGreater0(model, transitionMatrix, phiStates, psiStates); return performProb1(model, transitionMatrix, phiStates, psiStates, statesWithProbabilityGreater0); } - template + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); @@ -228,7 +228,7 @@ namespace storm { return result; } - template + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); @@ -238,7 +238,7 @@ namespace storm { return result; } - template + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { size_t numberOfStates = phiStates.size(); @@ -301,12 +301,12 @@ namespace storm { return statesWithProbability0; } - template + template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { return performProb0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); } - - template + + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { size_t numberOfStates = phiStates.size(); @@ -364,7 +364,7 @@ namespace storm { return currentStates; } - template + 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); } @@ -377,13 +377,13 @@ namespace storm { result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); return result; } - - template + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { return performProb01Max(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates); } - template + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { size_t numberOfStates = phiStates.size(); @@ -460,13 +460,13 @@ namespace storm { return statesWithProbabilityGreater0; } - template + template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); statesWithProbability0.complement(); return statesWithProbability0; } - + template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { storm::storage::BitVector statesWithProbability0 = performProbGreater0A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); @@ -474,7 +474,7 @@ namespace storm { return statesWithProbability0; } - template + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { size_t numberOfStates = phiStates.size(); @@ -548,19 +548,19 @@ namespace storm { result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); return result; } - - template + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { return performProb01Min(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates); } - template + template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd lastIterationStates = manager.getBddZero(); storm::dd::Bdd statesWithProbabilityGreater0E = psiStates; - + uint_fast64_t iterations = 0; storm::dd::Bdd abstractedTransitionMatrix = transitionMatrix.existsAbstract(model.getNondeterminismVariables()); while (lastIterationStates != statesWithProbabilityGreater0E) { @@ -571,16 +571,16 @@ namespace storm { statesWithProbabilityGreater0E |= lastIterationStates; ++iterations; } - + return statesWithProbabilityGreater0E; } - template + template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { return !performProbGreater0E(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); } - template + template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); @@ -602,12 +602,12 @@ namespace storm { return statesWithProbabilityGreater0A; } - template + template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { return !performProbGreater0A(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); } - template + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); @@ -629,12 +629,12 @@ namespace storm { return statesWithProbability1A; } - template + template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd statesWithProbability1E = statesWithProbabilityGreater0E; - + uint_fast64_t iterations = 0; bool outerLoopDone = false; while (!outerLoopDone) { @@ -666,7 +666,7 @@ namespace storm { } ++iterations; } - + return statesWithProbability1E; } @@ -688,13 +688,13 @@ namespace storm { return result; } - template + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) { if (matrix.getRowCount() != matrix.getColumnCount()) { LOG4CPLUS_ERROR(logger, "Provided matrix is required to be square."); throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square."; } - + uint_fast64_t numberOfStates = matrix.getRowCount(); // Prepare the result. This relies on the matrix being square. @@ -725,10 +725,10 @@ namespace storm { for (; successorIterator != matrix.end(currentState); ++successorIterator) { if (!visitedStates.get(successorIterator->getColumn())) { // Put unvisited successor on top of our recursion stack and remember that. - recursionStack.push_back(successorIterator->getColumn()); + recursionStack.push_back(successorIterator->getColumn()); // Also, put initial value for iterator on corresponding recursion stack. - iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); + iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); goto recursionStepForward; } @@ -759,7 +759,7 @@ namespace storm { - template + template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, @@ -767,13 +767,13 @@ namespace storm { LOG4CPLUS_INFO(logger, "Performing Dijkstra search."); - const uint_fast64_t noPredecessorValue = storm::utility::zero(); + const uint_fast64_t noPredecessorValue = storm::utility::zero(); std::vector probabilities(model.getNumberOfStates(), storm::utility::zero()); std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); // Set the probability to 1 for all starting states. std::set, DistanceCompare> probabilityStateSet; - + for (auto state : startingStates) { probabilityStateSet.emplace(storm::utility::one(), state); probabilities[state] = storm::utility::one(); @@ -790,7 +790,7 @@ namespace storm { // Only follow the transition if it lies within the filtered states. if (filterStates != nullptr && filterStates->get(transition.first)) { // Calculate the distance we achieve when we take the path to the successor via the current state. - T newDistance = probabilityStatePair.first; + T newDistance = probabilityStatePair.first; // We found a cheaper way to get to the target state of the transition. if (newDistance > probabilities[transition.first]) { // Remove the old distance. @@ -817,209 +817,209 @@ namespace storm { - + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); - + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); - + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + 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); 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) ; - - + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); - + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); - + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + 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); 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) ; - - + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; #ifdef STORM_HAVE_CARL - - + + template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); - + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); - + template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - + template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + 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); 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) ; - - + + template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - - + + template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - -#endif - +#endif + + template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); - + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0); - + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - + template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); - + template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; - + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; - + } // namespace graph } // namespace utility diff --git a/src/utility/solver.h b/src/utility/solver.h index f112f9a99..e18f435d6 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/storage/dd/DdType.h" #include "src/solver/SolverSelectionOptions.h" From 56eae69703b061040f4c782e594421bf17e95c06 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 11:31:40 +0200 Subject: [PATCH 4/7] added more missing headers Former-commit-id: 11be18e0d93693a398e871c98bc87ba16571bc4c --- src/modelchecker/csl/SparseCtmcCslModelChecker.cpp | 3 ++- src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp | 2 ++ src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp | 2 ++ src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp | 4 ++-- 4 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 8b3a2d9c5..cea164aa3 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -3,6 +3,8 @@ #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" +#include "src/models/sparse/StandardRewardModel.h" + #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" @@ -15,7 +17,6 @@ #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/NotImplementedException.h" - namespace storm { namespace modelchecker { template diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index f2d7463fe..90c133a50 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -2,6 +2,8 @@ #include "src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" +#include "src/models/sparse/StandardRewardModel.h" + #include "src/utility/macros.h" #include "src/settings/SettingsManager.h" diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 5c3684223..bf298ec27 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -11,6 +11,8 @@ #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" +#include "src/models/sparse/StandardRewardModel.h" + #include "src/settings/modules/GeneralSettings.h" #include "src/exceptions/InvalidStateException.h" diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 3c1c3bc4d..6005e6f07 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -8,11 +8,12 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/models/sparse/StandardRewardModel.h" + #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "src/solver/LpSolver.h" - #include "src/settings/modules/GeneralSettings.h" #include "src/exceptions/InvalidStateException.h" @@ -21,7 +22,6 @@ #include "src/storage/MaximalEndComponentDecomposition.h" - #include "src/exceptions/InvalidArgumentException.h" namespace storm { From f4211637db41a887d9f5ce3193bc0ea4ee479dc7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 11:37:35 +0200 Subject: [PATCH 5/7] fixed warning and missing include Former-commit-id: 09ad5ffb73f6ec3f849c088820943e9315f48b5b --- src/solver/MinMaxLinearEquationSolver.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index b5d53a68e..bf2e45020 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -3,6 +3,7 @@ #include #include +#include #include "SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" #include "AllowEarlyTerminationCondition.h" @@ -25,7 +26,6 @@ namespace storm { protected: AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech); - /// The required precision for the iterative methods. double precision; @@ -56,7 +56,7 @@ namespace storm { protected: MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), - A(matrix), earlyTermination(new NoEarlyTerminationCondition()) { + earlyTermination(new NoEarlyTerminationCondition()), A(matrix) { // Intentionally left empty. } From 57338640bee59643b5469d95055ccf88a6eb86b2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 12:00:20 +0200 Subject: [PATCH 6/7] added missing include Former-commit-id: c67bb4a99e36b21ef4bb556b9c3d734aa9617109 --- src/utility/macros.h | 23 +++++++++++-------- .../MaximalEndComponentDecompositionTest.cpp | 1 + 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/src/utility/macros.h b/src/utility/macros.h index 539b6b268..b84cd53b5 100644 --- a/src/utility/macros.h +++ b/src/utility/macros.h @@ -14,11 +14,12 @@ extern log4cplus::Logger logger; #define STORM_LOG_DEBUG(message) \ { \ LOG4CPLUS_DEBUG(logger, message); \ -} while (false) +} while (false) \ + #define STORM_LOG_TRACE(message) \ { \ LOG4CPLUS_TRACE(logger, message); \ -} while (false) +} while (false) \ // Define STORM_LOG_ASSERT which is only checked when NDEBUG is not set. #ifndef NDEBUG @@ -28,7 +29,8 @@ if (!(cond)) { \ LOG4CPLUS_ERROR(logger, message); \ assert(cond); \ } \ -} while (false) +} while (false) \ + #else #define STORM_LOG_ASSERT(cond, message) #endif @@ -39,44 +41,45 @@ assert(cond); \ LOG4CPLUS_ERROR(logger, message); \ throw exception() << message; \ } \ -} while (false) +} while (false) \ + // Define STORM_LOG_WARN, STORM_LOG_ERROR and STORM_LOG_INFO to log the given message with the corresponding log levels. #define STORM_LOG_WARN(message) \ { \ LOG4CPLUS_WARN(logger, message); \ -} while (false) +} while (false) \ #define STORM_LOG_WARN_COND(cond, message) \ { \ if (!(cond)) { \ LOG4CPLUS_WARN(logger, message); \ } \ -} while (false) +} while (false) \ #define STORM_LOG_INFO(message) \ { \ LOG4CPLUS_INFO(logger, message); \ -} while (false) +} while (false) \ #define STORM_LOG_INFO_COND(cond, message) \ { \ if (!(cond)) { \ LOG4CPLUS_INFO(logger, message); \ } \ -} while (false) +} while (false) \ #define STORM_LOG_ERROR(message) \ { \ LOG4CPLUS_ERROR(logger, message); \ -} while (false) +} while (false) \ #define STORM_LOG_ERROR_COND(cond, message) \ { \ if (!(cond)) { \ LOG4CPLUS_ERROR(logger, message); \ } \ -} while (false) +} while (false) \ /*! * Define the macros that print information and optionally also log it. diff --git a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp index 7af8bdb2c..73f53d069 100644 --- a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp +++ b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp @@ -3,6 +3,7 @@ #include "src/parser/AutoParser.h" #include "src/storage/MaximalEndComponentDecomposition.h" #include "src/models/sparse/Mdp.h" +#include "src/models/sparse/StandardRewardModel.h" TEST(MaximalEndComponentDecomposition, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); From 08bc810b2cf0aa4b4d7b95001e24d854034a21e8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 31 Aug 2015 12:41:20 +0200 Subject: [PATCH 7/7] added missing include Former-commit-id: 7eed5aaba7c695b02b07064c461915a472e7fa42 --- .../storage/StronglyConnectedComponentDecompositionTest.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp index 9f4f0ad5c..ca6f55907 100644 --- a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -4,6 +4,7 @@ #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/models/sparse/Mdp.h" #include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/StandardRewardModel.h" TEST(StronglyConnectedComponentDecomposition, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");