diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index eb8c6fb2c..14631fba5 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 57bfda26f..e9069a040 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 d457a4d50..d268754f5 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 553795c6f..be55228ca 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 { diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 57acf7f17..b05554e62 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" @@ -40,6 +41,7 @@ namespace storm { /// The direction in which to optimize, can be unset. OptimizationDirectionSetting direction; + /// The required precision for the iterative methods. double precision; @@ -70,7 +72,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. } diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h index ab959a032..3620de40d 100644 --- a/src/solver/SolveGoal.h +++ b/src/solver/SolveGoal.h @@ -57,6 +57,7 @@ namespace storm { VT threshold; storm::storage::BitVector relevantColumnVector; }; + template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template 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; diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index f48e6f5e2..3e12abcd2 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" @@ -24,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); @@ -57,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()); @@ -88,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(); @@ -144,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)); @@ -159,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(); @@ -169,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); @@ -178,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(); @@ -199,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(); @@ -226,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(); @@ -236,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(); @@ -299,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(); @@ -362,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); } @@ -375,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(); @@ -458,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); @@ -472,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(); @@ -546,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) { @@ -569,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(); @@ -600,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(); @@ -627,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) { @@ -664,7 +666,7 @@ namespace storm { } ++iterations; } - + return statesWithProbability1E; } @@ -686,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. @@ -723,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; } @@ -757,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, @@ -765,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(); @@ -788,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. @@ -815,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/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/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" 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", "", ""); 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", "", "");