diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 4b21e29d6..4bc5bc28c 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -480,7 +480,7 @@ namespace storm { // requested and issue an error otherwise. if (totalNumberOfChoices == 0) { if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { - transitionMatrix.insertNextValue(currentRow, currentState, storm::utility::constGetOne(), true); + transitionMatrix.insertNextValue(currentRow, currentState, storm::utility::constantOne(), true); if (transitionRewards.size() > 0) { transitionRewardMatrix.insertEmptyRow(true); } diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index 9445c6683..14fc2cf30 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -10,6 +10,8 @@ #include +#include "gmm/gmm_matrix.h" + #include "src/storage/SparseMatrix.h" #include "src/utility/ConversionHelper.h" diff --git a/src/adapters/StormAdapter.h b/src/adapters/StormAdapter.h index c8ab870a1..1f4dacd44 100644 --- a/src/adapters/StormAdapter.h +++ b/src/adapters/StormAdapter.h @@ -8,6 +8,8 @@ #ifndef STORM_ADAPTERS_STORMADAPTER_H_ #define STORM_ADAPTERS_STORMADAPTER_H_ +#include "gmm/gmm_matrix.h" +#include "Eigen/Sparse" #include "src/storage/SparseMatrix.h" #include "log4cplus/logger.h" diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/Csl/ProbabilisticBoundOperator.h index 75a985e91..28937fab4 100644 --- a/src/formula/Csl/ProbabilisticBoundOperator.h +++ b/src/formula/Csl/ProbabilisticBoundOperator.h @@ -11,7 +11,7 @@ #include "AbstractStateFormula.h" #include "AbstractPathFormula.h" #include "src/formula/abstract/ProbabilisticBoundOperator.h" -#include "utility/ConstTemplates.h" +#include "utility/constants.h" namespace storm { namespace property { @@ -61,7 +61,7 @@ public: * Empty constructor */ ProbabilisticBoundOperator() : storm::property::abstract::ProbabilisticBoundOperator> - (LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + (LESS_EQUAL, storm::utility::constantZero(), nullptr) { // Intentionally left empty } diff --git a/src/formula/Csl/SteadyStateBoundOperator.h b/src/formula/Csl/SteadyStateBoundOperator.h index a63c64196..ddd9be3b2 100644 --- a/src/formula/Csl/SteadyStateBoundOperator.h +++ b/src/formula/Csl/SteadyStateBoundOperator.h @@ -62,7 +62,7 @@ public: * Empty constructor */ SteadyStateBoundOperator() : storm::property::abstract::SteadyStateBoundOperator> - (LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + (LESS_EQUAL, storm::utility::constantZero(), nullptr) { // Intentionally left empty } diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h index 5f6253e93..a2ea229aa 100644 --- a/src/formula/Prctl/ProbabilisticBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticBoundOperator.h @@ -11,7 +11,7 @@ #include "AbstractStateFormula.h" #include "AbstractPathFormula.h" #include "src/formula/abstract/ProbabilisticBoundOperator.h" -#include "utility/ConstTemplates.h" +#include "utility/constants.h" namespace storm { namespace property { diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h index 5aa4d83c0..4c5cf19d3 100644 --- a/src/formula/Prctl/RewardBoundOperator.h +++ b/src/formula/Prctl/RewardBoundOperator.h @@ -11,7 +11,7 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" #include "src/formula/abstract/RewardBoundOperator.h" -#include "utility/ConstTemplates.h" +#include "utility/constants.h" namespace storm { namespace property { diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h index cc841d78d..f6c1cd956 100644 --- a/src/formula/abstract/PathBoundOperator.h +++ b/src/formula/abstract/PathBoundOperator.h @@ -15,7 +15,7 @@ #include "src/formula/abstract/OptimizingOperator.h" -#include "src/utility/ConstTemplates.h" +#include "src/utility/constants.h" namespace storm { diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h index d8fc0764d..b326e1c05 100644 --- a/src/formula/abstract/ProbabilisticBoundOperator.h +++ b/src/formula/abstract/ProbabilisticBoundOperator.h @@ -11,7 +11,7 @@ #include "src/formula/abstract/AbstractFormula.h" #include "src/formula/abstract/PathBoundOperator.h" #include "src/formula/abstract/OptimizingOperator.h" -#include "utility/ConstTemplates.h" +#include "utility/constants.h" namespace storm { namespace property { @@ -53,7 +53,7 @@ public: * Empty constructor */ ProbabilisticBoundOperator() : PathBoundOperator - (LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + (LESS_EQUAL, storm::utility::constantZero(), nullptr) { // Intentionally left empty } diff --git a/src/formula/abstract/RewardBoundOperator.h b/src/formula/abstract/RewardBoundOperator.h index d607133f9..30d2f3221 100644 --- a/src/formula/abstract/RewardBoundOperator.h +++ b/src/formula/abstract/RewardBoundOperator.h @@ -9,7 +9,7 @@ #define STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_ #include "PathBoundOperator.h" -#include "utility/ConstTemplates.h" +#include "utility/constants.h" namespace storm { namespace property { @@ -47,7 +47,7 @@ public: /*! * Empty constructor */ - RewardBoundOperator() : PathBoundOperator(LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + RewardBoundOperator() : PathBoundOperator(LESS_EQUAL, storm::utility::constantZero(), nullptr) { // Intentionally left empty } diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h index 6258c7044..c274bd2b3 100644 --- a/src/formula/abstract/StateBoundOperator.h +++ b/src/formula/abstract/StateBoundOperator.h @@ -12,7 +12,7 @@ #include "src/formula/abstract/AbstractFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/formula/ComparisonType.h" -#include "src/utility/ConstTemplates.h" +#include "src/utility/constants.h" namespace storm { namespace property { diff --git a/src/formula/abstract/SteadyStateBoundOperator.h b/src/formula/abstract/SteadyStateBoundOperator.h index 5c24ccff0..a25e7d280 100644 --- a/src/formula/abstract/SteadyStateBoundOperator.h +++ b/src/formula/abstract/SteadyStateBoundOperator.h @@ -41,7 +41,7 @@ public: * Empty constructor */ SteadyStateBoundOperator() : StateBoundOperator - (LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + (LESS_EQUAL, storm::utility::constantZero(), nullptr) { // Intentionally left empty } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index d4feb1e88..96f71648c 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -98,9 +98,9 @@ namespace storm { for (auto element : row) { ValueType eTerm = std::exp(-exitRates[state] * delta); if (element.column() == rowIndex) { - element.value() = (storm::utility::constGetOne() - eTerm) * element.value() + eTerm; + element.value() = (storm::utility::constantOne() - eTerm) * element.value() + eTerm; } else { - element.value() = (storm::utility::constGetOne() - eTerm) * element.value(); + element.value() = (storm::utility::constantOne() - eTerm) * element.value(); } } ++rowIndex; @@ -125,7 +125,7 @@ namespace storm { std::vector bMarkovianFixed; bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); for (auto state : markovianNonGoalStates) { - bMarkovianFixed.push_back(storm::utility::constGetZero()); + bMarkovianFixed.push_back(storm::utility::constantZero()); typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]); for (auto element : row) { @@ -175,7 +175,7 @@ namespace storm { } // Check whether the given bounds were valid. - if (lowerBound < storm::utility::constGetZero() || upperBound < storm::utility::constGetZero() || upperBound < lowerBound) { + if (lowerBound < storm::utility::constantZero() || upperBound < storm::utility::constantZero() || upperBound < lowerBound) { throw storm::exceptions::InvalidArgumentException() << "Illegal interval ["; } @@ -204,14 +204,14 @@ namespace storm { computeBoundedReachability(min, transitionMatrix, nondeterministicChoiceIndices, exitRates, markovianStates, goalStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps); // (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration. - if (lowerBound != storm::utility::constGetZero()) { + if (lowerBound != storm::utility::constantZero()) { std::vector vAllProbabilistic((~markovianStates).getNumberOfSetBits()); std::vector vAllMarkovian(markovianStates.getNumberOfSetBits()); // Create the starting value vectors for the next value iteration based on the results of the previous one. - storm::utility::vector::setVectorValues(vAllProbabilistic, goalStates % ~markovianStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(vAllProbabilistic, goalStates % ~markovianStates, storm::utility::constantOne()); storm::utility::vector::setVectorValues(vAllProbabilistic, ~goalStates % ~markovianStates, vProbabilistic); - storm::utility::vector::setVectorValues(vAllMarkovian, goalStates % markovianStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(vAllMarkovian, goalStates % markovianStates, storm::utility::constantOne()); storm::utility::vector::setVectorValues(vAllMarkovian, ~goalStates % markovianStates, vMarkovian); // Compute the number of steps to reach the target interval. @@ -231,7 +231,7 @@ namespace storm { } else { // Create the result vector out of 1_G, vProbabilistic and vMarkovian and return it. std::vector result(this->getModel().getNumberOfStates()); - storm::utility::vector::setVectorValues(result, goalStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(result, goalStates, storm::utility::constantOne()); storm::utility::vector::setVectorValues(result, probabilisticNonGoalStates, vProbabilistic); storm::utility::vector::setVectorValues(result, markovianNonGoalStates, vMarkovian); return result; @@ -246,12 +246,12 @@ namespace storm { // If there are no goal states, we avoid the computation and directly return zero. if (goalStates.empty()) { - return std::vector(this->getModel().getNumberOfStates(), storm::utility::constGetZero()); + return std::vector(this->getModel().getNumberOfStates(), storm::utility::constantZero()); } // Likewise, if all bits are set, we can avoid the computation and set. if ((~goalStates).empty()) { - return std::vector(this->getModel().getNumberOfStates(), storm::utility::constGetOne()); + return std::vector(this->getModel().getNumberOfStates(), storm::utility::constantOne()); } // Start by decomposing the Markov automaton into its MECs. @@ -312,7 +312,7 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { std::vector auxiliaryStateToProbabilityMap(mecDecomposition.size()); - b.push_back(storm::utility::constGetZero()); + b.push_back(storm::utility::constantZero()); typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); for (auto element : row) { @@ -349,7 +349,7 @@ namespace storm { // If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state. if (!choicesInMec.contains(choice)) { - b.push_back(storm::utility::constGetZero()); + b.push_back(storm::utility::constantZero()); typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); for (auto element : row) { @@ -413,8 +413,8 @@ namespace storm { std::vector checkExpectedTime(bool min, storm::storage::BitVector const& goalStates) const { // Reduce the problem of computing the expected time to computing expected rewards where the rewards // for all probabilistic states are zero and the reward values of Markovian states is 1. - std::vector rewardValues(this->getModel().getNumberOfStates(), storm::utility::constGetZero()); - storm::utility::vector::setVectorValues(rewardValues, this->getModel().getMarkovianStates(), storm::utility::constGetOne()); + std::vector rewardValues(this->getModel().getNumberOfStates(), storm::utility::constantZero()); + storm::utility::vector::setVectorValues(rewardValues, this->getModel().getMarkovianStates(), storm::utility::constantOne()); return this->computeExpectedRewards(min, goalStates, rewardValues); } @@ -464,9 +464,9 @@ namespace storm { } variables.push_back(lraValueVariableIndex); - coefficients.push_back(storm::utility::constGetOne() / exitRates[state]); + coefficients.push_back(storm::utility::constantOne() / exitRates[state]); - solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, goalStates.get(state) ? storm::utility::constGetOne() / exitRates[state] : storm::utility::constGetZero()); + solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, goalStates.get(state) ? storm::utility::constantOne() / exitRates[state] : storm::utility::constantZero()); } else { // For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action // and the sum ranges over all states s'. @@ -483,7 +483,7 @@ namespace storm { coefficients.push_back(-element.value()); } - solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constGetZero()); + solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constantZero()); } } } @@ -582,8 +582,8 @@ namespace storm { // Set values of resulting vector according to previous result and return the result. storm::utility::vector::setVectorValues(result, maybeStates, x); - storm::utility::vector::setVectorValues(result, goalStates, storm::utility::constGetZero()); - storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); + storm::utility::vector::setVectorValues(result, goalStates, storm::utility::constantZero()); + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constantInfinity()); return result; } diff --git a/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h index 4e615c0af..702824a09 100644 --- a/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h @@ -12,7 +12,7 @@ #include "src/models/Dtmc.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "src/utility/ConstTemplates.h" +#include "src/utility/constants.h" #include "src/exceptions/NoConvergenceException.h" #include "Eigen/Sparse" diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 8505b3ca9..acef76037 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -134,7 +134,7 @@ public: // Create the vector with which to multiply. std::vector subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); - storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constantOne()); // Perform the matrix vector multiplication as often as required by the formula bound. if (linearEquationSolver != nullptr) { @@ -145,7 +145,7 @@ public: // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); - storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::constGetZero()); + storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::constantZero()); } return result; @@ -168,7 +168,7 @@ public: // Create the vector with which to multiply and initialize it correctly. std::vector result(this->getModel().getNumberOfStates()); - storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constantOne()); // Perform one single matrix-vector multiplication. if (linearEquationSolver != nullptr) { @@ -321,8 +321,8 @@ public: } // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); - storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::constantZero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::constantOne()); return result; } @@ -444,7 +444,7 @@ public: << " No exact rewards were computed."); // Set the values for all maybe-states to 1 to indicate that their reward values // are neither 0 nor infinity. - storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::constantOne()); } else { // In this case we have to compute the reward values for the remaining states. // We can eliminate the rows and columns from the original transition probability matrix. @@ -455,7 +455,7 @@ public: // Initialize the x vector with 1 for each element. This is the initial guess for // the iterative solvers. - std::vector x(submatrix.getColumnCount(), storm::utility::constGetOne()); + std::vector x(submatrix.getColumnCount(), storm::utility::constantOne()); // Prepare the right-hand side of the equation system. std::vector b(submatrix.getRowCount()); @@ -495,8 +495,8 @@ public: } // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constGetZero()); - storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); + storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constantZero()); + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constantInfinity()); return result; } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 2ffcba987..a03b9d080 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -126,13 +126,13 @@ namespace storm { // Create the vector with which to multiply. std::vector subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); - storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constantOne()); this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, subNondeterministicChoiceIndices, nullptr, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); - storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::constGetZero()); + storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::constantZero()); } return result; @@ -167,7 +167,7 @@ namespace storm { virtual std::vector checkNext(storm::storage::BitVector const& nextStates, bool qualitative) const { // Create the vector with which to multiply and initialize it correctly. std::vector result(this->getModel().getNumberOfStates()); - storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constantOne()); this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices()); @@ -336,8 +336,8 @@ namespace storm { } // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); - storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::constantZero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::constantOne()); // Finally, compute a scheduler that achieves the extramal value. storm::storage::TotalScheduler scheduler = computeExtremalScheduler(minimize, transitionMatrix, nondeterministicChoiceIndices, result); @@ -477,7 +477,7 @@ namespace storm { << " No exact rewards were computed."); // Set the values for all maybe-states to 1 to indicate that their reward values // are neither 0 nor infinity. - storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::constGetOne()); + storm::utility::vector::setVectorValues(result, maybeStates, storm::utility::constantOne()); } else { // In this case we have to compute the reward values for the remaining states. @@ -527,8 +527,8 @@ namespace storm { } // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constGetZero()); - storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); + storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constantZero()); + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constantInfinity()); // Finally, compute a scheduler that achieves the extramal value. storm::storage::TotalScheduler scheduler = computeExtremalScheduler(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), result, this->getModel().hasStateRewards() ? &this->getModel().getStateRewardVector() : nullptr, this->getModel().hasTransitionRewards() ? &this->getModel().getTransitionRewardMatrix() : nullptr); diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 0ba5166f6..7d4564280 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -98,7 +98,7 @@ class AbstractDeterministicModel: public AbstractModel { auto rowIt = this->transitionMatrix.begin(); for (uint_fast64_t i = 0; i < this->transitionMatrix.getRowCount(); ++i, ++rowIt) { for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) { - if (transitionIt.value() != storm::utility::constGetZero()) { + if (transitionIt.value() != storm::utility::constantZero()) { if (subsystem == nullptr || subsystem->get(transitionIt.column())) { outStream << "\t" << i << " -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ];" << std::endl; } diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 363820640..fa21aa9a5 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -101,7 +101,7 @@ namespace storm { } T getMaximalExitRate() const { - T result = storm::utility::constGetZero(); + T result = storm::utility::constantZero(); for (auto markovianState : this->markovianStates) { result = std::max(result, this->exitRates[markovianState]); } diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 6af4b3ffd..6ecea851a 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -173,7 +173,7 @@ public: // If no choice of the current state may be taken, we insert a self-loop to the state instead. if (!stateHasValidChoice) { nondeterministicChoiceIndices.push_back(currentRow); - transitionMatrix.insertNextValue(currentRow, state, storm::utility::constGetOne(), true); + transitionMatrix.insertNextValue(currentRow, state, storm::utility::constantOne(), true); newChoiceLabeling.emplace_back(); ++currentRow; } diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index f66c82926..efca04e02 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -7,7 +7,7 @@ #include "src/parser/CslParser.h" #include "src/utility/OsDetection.h" -#include "src/utility/ConstTemplates.h" +#include "src/utility/constants.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 2b21bcba5..e270c7a44 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -230,7 +230,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if (lastRow != row) { if ((lastRow != -1) && (!rowHadDiagonalEntry)) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero()); + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); @@ -241,7 +241,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; if (fixDeadlocks && !isRewardMatrix) { - resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constGetOne()); + resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); rowHadDiagonalEntry = true; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); } else if (!isRewardMatrix) { @@ -258,7 +258,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st } else if (col > row && !rowHadDiagonalEntry) { rowHadDiagonalEntry = true; if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - resultMatrix.addNextValue(row, row, storm::utility::constGetZero()); + resultMatrix.addNextValue(row, row, storm::utility::constantZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); @@ -271,7 +271,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero()); + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index cc1bee3e7..5083837b9 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -8,7 +8,7 @@ #include "LtlParser.h" #include "src/utility/OsDetection.h" -#include "src/utility/ConstTemplates.h" +#include "src/utility/constants.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 6f7cdf562..fb58d7ee9 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -1,6 +1,6 @@ #include "src/parser/PrctlParser.h" #include "src/utility/OsDetection.h" -#include "src/utility/ConstTemplates.h" +#include "src/utility/constants.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h index a43b9ca4b..de32a4a32 100644 --- a/src/solver/GmmxxLinearEquationSolver.h +++ b/src/solver/GmmxxLinearEquationSolver.h @@ -3,7 +3,7 @@ #include "AbstractLinearEquationSolver.h" #include "src/adapters/GmmxxAdapter.h" -#include "src/utility/ConstTemplates.h" +#include "src/utility/constants.h" #include "src/settings/Settings.h" #include "src/utility/vector.h" diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h index f69e37029..923d8b9f6 100644 --- a/src/storage/LabeledValues.h +++ b/src/storage/LabeledValues.h @@ -14,7 +14,7 @@ namespace storm { namespace utility { template - static ValueType constGetZero(); + static ValueType constantZero(); } namespace storage { @@ -186,7 +186,7 @@ namespace storm { * @return The sum of the values. */ ValueType getSum() const { - ValueType sum = storm::utility::constGetZero(); + ValueType sum = storm::utility::constantZero(); for (auto const& valueLabelListPair : *this) { sum += valueLabelListPair.first; } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 0a1813ccb..c23858b75 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -6,6 +6,9 @@ */ #include +#include + +#include "gmm/gmm_matrix.h" #include "src/storage/SparseMatrix.h" @@ -439,10 +442,10 @@ namespace storage { // If there is at least one nonzero entry in this row, we can just set it to one, modify its // column indication to the one given by the parameter and set all subsequent elements of this // row to zero. - valueStorage[rowStart] = storm::utility::constGetOne(); + valueStorage[rowStart] = storm::utility::constantOne(); columnIndications[rowStart] = column; for (uint_fast64_t index = rowStart + 1; index < rowEnd; ++index) { - valueStorage[index] = storm::utility::constGetZero(); + valueStorage[index] = storm::utility::constantZero(); columnIndications[index] = 0; } @@ -613,14 +616,14 @@ namespace storage { if (index == columnIndications[j]) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && columnIndications[j] > index) { - result.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constGetZero()); + result.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); insertedDiagonalElement = true; } result.addNextValue(rowCount, bitsSetBeforeIndex[columnIndications[j]], valueStorage[j]); } } if (insertDiagonalEntries && !insertedDiagonalElement) { - result.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constGetZero()); + result.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); } ++rowCount; @@ -675,13 +678,13 @@ namespace storage { if (columnIndications[i] == rowGroupIndex) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && columnIndications[i] > rowGroupIndex) { - submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constGetZero()); + submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); insertedDiagonalElement = true; } submatrix.addNextValue(rowGroupIndex, columnIndications[i], valueStorage[i]); } if (insertDiagonalEntries && !insertedDiagonalElement) { - submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constGetZero()); + submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); } } @@ -758,7 +761,7 @@ namespace storage { // Now iterate over all rows and set the diagonal elements to the inverted value. // If there is a row without the diagonal element, an exception is thrown. - T one = storm::utility::constGetOne(); + T one = storm::utility::constantOne(); bool foundDiagonalElement = false; for (uint_fast64_t row = 0; row < rowCount; ++row) { uint_fast64_t rowStart = rowIndications[row]; @@ -814,12 +817,12 @@ namespace storage { resultDinv.initialize(rowCount); // constant 1 for diagonal inversion - T constOne = storm::utility::constGetOne(); + T constOne = storm::utility::constantOne(); // copy diagonal entries to other matrix for (uint_fast64_t i = 0; i < rowCount; ++i) { resultDinv.addNextValue(i, i, constOne / resultLU.getValue(i, i)); - resultLU.getValue(i, i) = storm::utility::constGetZero(); + resultLU.getValue(i, i) = storm::utility::constantZero(); } resultDinv.finalize(); @@ -829,7 +832,7 @@ namespace storage { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { // Prepare result. - std::vector result(rowCount, storm::utility::constGetZero()); + std::vector result(rowCount, storm::utility::constantZero()); // Iterate over all elements of the current matrix and either continue with the next element // in case the given matrix does not have a non-zero element at this column position, or @@ -860,7 +863,7 @@ namespace storage { ConstRowIterator rowIt = this->begin(); for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++rowIt) { - *resultIt = storm::utility::constGetZero(); + *resultIt = storm::utility::constantZero(); for (auto elementIt = rowIt.begin(), elementIte = rowIt.end(); elementIt != elementIte; ++elementIt) { *resultIt += elementIt.value() * vector[elementIt.column()]; @@ -958,7 +961,7 @@ namespace storage { template T SparseMatrix::getRowSum(uint_fast64_t row) const { - T sum = storm::utility::constGetZero(); + T sum = storm::utility::constantZero(); for (auto it = this->constValueIteratorBegin(row), ite = this->constValueIteratorEnd(row); it != ite; ++it) { sum += *it; } @@ -1064,9 +1067,9 @@ namespace storage { boost::hash_combine(result, nonZeroEntryCount); boost::hash_combine(result, currentSize); boost::hash_combine(result, lastRow); - boost::hash_combine(result, storm::utility::Hash::getHash(valueStorage)); - boost::hash_combine(result, storm::utility::Hash::getHash(columnIndications)); - boost::hash_combine(result, storm::utility::Hash::getHash(rowIndications)); + boost::hash_combine(result, boost::hash_range(valueStorage.begin(), valueStorage.end())); + boost::hash_combine(result, boost::hash_range(columnIndications.begin(), columnIndications.end())); + boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end())); return result; } @@ -1085,7 +1088,7 @@ namespace storage { bool SparseMatrix::prepareInternalStorage(bool initializeElements) { if (initializeElements) { // Set up the arrays for the elements that are not on the diagonal. - valueStorage.resize(nonZeroEntryCount, storm::utility::constGetZero()); + valueStorage.resize(nonZeroEntryCount, storm::utility::constantZero()); columnIndications.resize(nonZeroEntryCount, 0); // Set up the rowIndications vector and reserve one element more than there are rows in @@ -1122,7 +1125,7 @@ namespace storage { uint_fast64_t indexEnd = matrixA->rowIndications.at(row + 1); // Initialize the result to be 0. - T element = storm::utility::constGetZero(); + T element = storm::utility::constantZero(); for (; index != indexEnd; ++index) { element += matrixA->valueStorage.at(index) * vectorX->at(matrixA->columnIndications.at(index)); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 05e62dd4a..ced60c8b1 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -11,29 +11,19 @@ # include #endif -#include -#include #include #include -#include -#include -#include #include +#include "src/storage/BitVector.h" +#include "src/utility/constants.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" -#include "src/exceptions/FileIoException.h" -#include "src/storage/BitVector.h" - -#include "src/utility/ConstTemplates.h" -#include "src/utility/Hash.h" -#include "Eigen/Sparse" -#include "gmm/gmm_matrix.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" - extern log4cplus::Logger logger; // Forward declaration for adapter classes. diff --git a/src/utility/ConstTemplates.h b/src/utility/constants.h similarity index 85% rename from src/utility/ConstTemplates.h rename to src/utility/constants.h index 71b489c3d..e8a194619 100644 --- a/src/utility/ConstTemplates.h +++ b/src/utility/constants.h @@ -1,5 +1,5 @@ /* - * ConstTemplates.h + * constants.h * * Created on: 11.10.2012 * Author: Thomas Heinemann @@ -33,12 +33,12 @@ namespace utility { * * @note * The template parameter is just inferred by the return type; GCC is not able to infer this - * automatically, hence the type should always be stated explicitly (e.g. @c constGetZero();) + * automatically, hence the type should always be stated explicitly (e.g. @c constantZero();) * * @return Value 0, fit to the return type */ template -static inline _Scalar constGetZero() { +static inline _Scalar constantZero() { return _Scalar(0); } @@ -51,7 +51,7 @@ static inline _Scalar constGetZero() { * @return Value 0, fit to the type int_fast32_t */ template <> -inline int_fast32_t constGetZero() { +inline int_fast32_t constantZero() { return 0; } @@ -60,7 +60,7 @@ inline int_fast32_t constGetZero() { * @return Value 0, fit to the type uint_fast64_t */ template <> -inline uint_fast64_t constGetZero() { +inline uint_fast64_t constantZero() { return 0; } @@ -69,7 +69,7 @@ inline uint_fast64_t constGetZero() { * @return Value 0.0, fit to the type double */ template <> -inline double constGetZero() { +inline double constantZero() { return 0.0; } @@ -78,7 +78,7 @@ inline double constGetZero() { * @return A LabeledValues object that represents a value of 0. */ template<> -inline storm::storage::LabeledValues constGetZero() { +inline storm::storage::LabeledValues constantZero() { return storm::storage::LabeledValues(0.0); } @@ -91,12 +91,12 @@ inline storm::storage::LabeledValues constGetZero() { * * @note * The template parameter is just inferred by the return type; GCC is not able to infer this - * automatically, hence the type should always be stated explicitly (e.g. @c constGetOne();) + * automatically, hence the type should always be stated explicitly (e.g. @c constantOne();) * * @return Value 1, fit to the return type */ template -static inline _Scalar constGetOne() { +static inline _Scalar constantOne() { return _Scalar(1); } @@ -109,7 +109,7 @@ static inline _Scalar constGetOne() { * @return Value 1, fit to the type int_fast32_t */ template<> -inline int_fast32_t constGetOne() { +inline int_fast32_t constantOne() { return 1; } @@ -118,7 +118,7 @@ inline int_fast32_t constGetOne() { * @return Value 1, fit to the type uint_fast61_t */ template<> -inline uint_fast64_t constGetOne() { +inline uint_fast64_t constantOne() { return 1; } @@ -127,7 +127,7 @@ inline uint_fast64_t constGetOne() { * @return Value 1.0, fit to the type double */ template<> -inline double constGetOne() { +inline double constantOne() { return 1.0; } @@ -136,7 +136,7 @@ inline double constGetOne() { * @return A LabeledValues object that represents a value of 1. */ template<> -inline storm::storage::LabeledValues constGetOne() { +inline storm::storage::LabeledValues constantOne() { return storm::storage::LabeledValues(1.0); } @@ -149,12 +149,12 @@ inline storm::storage::LabeledValues constGetOne() { * * @note * The template parameter is just inferred by the return type; GCC is not able to infer this - * automatically, hence the type should always be stated explicitly (e.g. @c constGetOne();) + * automatically, hence the type should always be stated explicitly (e.g. @c constantOne();) * * @return Value Infinity, fit to the return type */ template -static inline _Scalar constGetInfinity() { +static inline _Scalar constantInfinity() { return std::numeric_limits<_Scalar>::infinity(); } @@ -167,7 +167,7 @@ static inline _Scalar constGetInfinity() { * @return Value Infinity, fit to the type uint_fast32_t */ template<> -inline int_fast32_t constGetInfinity() { +inline int_fast32_t constantInfinity() { throw storm::exceptions::InvalidArgumentException() << "Integer has no infinity."; return std::numeric_limits::max(); } @@ -177,7 +177,7 @@ inline int_fast32_t constGetInfinity() { * @return Value Infinity, fit to the type uint_fast64_t */ template<> -inline uint_fast64_t constGetInfinity() { +inline uint_fast64_t constantInfinity() { throw storm::exceptions::InvalidArgumentException() << "Integer has no infinity."; return std::numeric_limits::max(); } @@ -187,7 +187,7 @@ inline uint_fast64_t constGetInfinity() { * @return Value Infinity, fit to the type double */ template<> -inline double constGetInfinity() { +inline double constantInfinity() { return std::numeric_limits::infinity(); } @@ -196,7 +196,7 @@ inline double constGetInfinity() { * @return Value Infinity, fit to the type LabeledValues. */ template<> -inline storm::storage::LabeledValues constGetInfinity() { +inline storm::storage::LabeledValues constantInfinity() { return storm::storage::LabeledValues(std::numeric_limits::infinity()); } diff --git a/src/utility/graph.h b/src/utility/graph.h index 5c08d94e7..3fd0c6693 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -20,7 +20,7 @@ #include "src/models/AbstractDeterministicModel.h" #include "src/models/AbstractNondeterministicModel.h" -#include "ConstTemplates.h" +#include "constants.h" #include "src/exceptions/InvalidArgumentException.h" #include "log4cplus/logger.h" @@ -668,8 +668,8 @@ namespace storm { LOG4CPLUS_INFO(logger, "Performing Dijkstra search."); - const uint_fast64_t noPredecessorValue = storm::utility::constGetZero(); - std::vector probabilities(model.getNumberOfStates(), storm::utility::constGetZero()); + const uint_fast64_t noPredecessorValue = storm::utility::constantZero(); + std::vector probabilities(model.getNumberOfStates(), storm::utility::constantZero()); std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); // Set the probability to 1 for all starting states. @@ -679,8 +679,8 @@ namespace storm { std::set, DistanceCompare> probabilityStateSet; #endif for (auto state : startingStates) { - probabilityStateSet.emplace(storm::utility::constGetOne(), state); - probabilities[state] = storm::utility::constGetOne(); + probabilityStateSet.emplace(storm::utility::constantOne(), state); + probabilities[state] = storm::utility::constantOne(); } // As long as there is one reachable state, we need to consider it. diff --git a/src/utility/matrix.h b/src/utility/matrix.h index 897db4374..e5520ac35 100644 --- a/src/utility/matrix.h +++ b/src/utility/matrix.h @@ -37,7 +37,7 @@ namespace storm { } } else { // If no valid choice for the state is defined, we insert a self-loop. - result.insertNextValue(state, state, storm::utility::constGetOne()); + result.insertNextValue(state, state, storm::utility::constantOne()); } } diff --git a/src/utility/vector.h b/src/utility/vector.h index c9bf3b35d..283bfbe7c 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -2,7 +2,7 @@ #define STORM_UTILITY_VECTOR_H_ #include "Eigen/Core" -#include "ConstTemplates.h" +#include "constants.h" #include #include #include @@ -130,7 +130,7 @@ namespace storm { template void subtractFromConstantOneVector(std::vector& vector) { for (auto& element : vector) { - element = storm::utility::constGetOne() - element; + element = storm::utility::constantOne() - element; } } diff --git a/test/performance/storage/BitVectorTest.cpp b/test/performance/storage/BitVectorTest.cpp new file mode 100644 index 000000000..a9486a2be --- /dev/null +++ b/test/performance/storage/BitVectorTest.cpp @@ -0,0 +1,15 @@ +#include "gtest/gtest.h" +#include "src/storage/BitVector.h" + +TEST(BitVectorTest, IterationTest) { + storm::storage::BitVector vector(819200, true); + + for (uint_fast64_t i = 0; i < 10000; ++i) { + for (auto bit : vector) { + // The following can never be true, but prevents the compiler from optimizing away the loop. + if (bit == 819200) { + ASSERT_TRUE(false); + } + } + } +} \ No newline at end of file