sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Started to improve performance of sparse CTMC model checker. 

Former-commit-id: 1d014412ec
main
dehnert 11 years ago
parent
d545fac471
commit
1990567b84
20 changed files with 316 additions and 42 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 44
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  2. 3
      src/modelchecker/csl/SparseCtmcCslModelChecker.h
  3. 8
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  4. 4
      src/settings/modules/GeneralSettings.cpp
  5. 7
      src/settings/modules/GeneralSettings.h
  6. 2
      src/solver/GmmxxLinearEquationSolver.cpp
  7. 2
      src/solver/GmmxxLinearEquationSolver.h
  8. 2
      src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
  9. 2
      src/solver/LinearEquationSolver.h
  10. 2
      src/solver/NativeLinearEquationSolver.cpp
  11. 2
      src/solver/NativeLinearEquationSolver.h
  12. 5
      src/solver/TopologicalNondeterministicLinearEquationSolver.cpp
  13. 1
      src/utility/cli.h
  14. 5
      src/utility/solver.cpp
  15. 2
      src/utility/solver.h
  16. 6
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  17. 159
      test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  18. 84
      test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  19. 6
      test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  20. 12
      test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

44
src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -117,15 +117,22 @@ namespace storm {
STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
// Compute the uniformized matrix. // Compute the uniformized matrix.
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0, psiStates, uniformizationRate, exitRates);
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0NonPsi, storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, exitRates);
// Finally compute the transient probabilities.
std::vector<ValueType> psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>());
// Compute the vector that is to be added as a compensation for removing the absorbing states.
std::vector<ValueType> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates);
for (auto& element : b) {
element /= uniformizationRate;
}
std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero<ValueType>());
std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, upperBound, uniformizationRate, psiStateValues, *this->linearEquationSolverFactory);
// Finally compute the transient probabilities.
std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, b, upperBound, uniformizationRate, values, *this->linearEquationSolverFactory);
result = std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>()); result = std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0NonPsi, subresult);
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
} else if (comparator.isInfinity(upperBound)) { } else if (comparator.isInfinity(upperBound)) {
// In this case, the interval is of the form [t, inf] with t != 0. // In this case, the interval is of the form [t, inf] with t != 0.
@ -150,7 +157,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, storm::storage::BitVector(result.size()), uniformizationRate, exitRates); storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, storm::storage::BitVector(result.size()), uniformizationRate, exitRates);
// Compute the transient probabilities. // Compute the transient probabilities.
subResult = this->computeTransientProbabilities(uniformizedMatrix, lowerBound, uniformizationRate, subResult, *this->linearEquationSolverFactory);
subResult = this->computeTransientProbabilities(uniformizedMatrix, std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>()), lowerBound, uniformizationRate, subResult, *this->linearEquationSolverFactory);
// Fill in the correct values. // Fill in the correct values.
storm::utility::vector::setVectorValues(result, ~relevantStates, storm::utility::zero<ValueType>()); storm::utility::vector::setVectorValues(result, ~relevantStates, storm::utility::zero<ValueType>());
@ -172,7 +179,7 @@ namespace storm {
// Start by computing the transient probabilities of reaching a psi state in time t' - t. // Start by computing the transient probabilities of reaching a psi state in time t' - t.
std::vector<ValueType> psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero<ValueType>()); std::vector<ValueType> psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>()); storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>());
std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, upperBound - lowerBound, uniformizationRate, psiStateValues, *this->linearEquationSolverFactory);
std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, std::vector<ValueType>(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero<ValueType>()), upperBound - lowerBound, uniformizationRate, psiStateValues, *this->linearEquationSolverFactory);
// Determine the set of states that must be considered further. // Determine the set of states that must be considered further.
storm::storage::BitVector relevantStates = storm::utility::vector::filterGreaterZero(subresult); storm::storage::BitVector relevantStates = storm::utility::vector::filterGreaterZero(subresult);
@ -192,7 +199,7 @@ namespace storm {
// Finally, we compute the second set of transient probabilities. // Finally, we compute the second set of transient probabilities.
uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, exitRates); uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, exitRates);
newSubresult = this->computeTransientProbabilities(uniformizedMatrix, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory);
newSubresult = this->computeTransientProbabilities(uniformizedMatrix, std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>()), lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory);
// Fill in the correct values. // Fill in the correct values.
result = std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>()); result = std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
@ -207,6 +214,9 @@ namespace storm {
template<class ValueType> template<class ValueType>
storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<ValueType>::computeUniformizedMatrix(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& absorbingStates, ValueType uniformizationRate, std::vector<ValueType> const& exitRates) { storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<ValueType>::computeUniformizedMatrix(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& absorbingStates, ValueType uniformizationRate, std::vector<ValueType> const& exitRates) {
STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << ".");
STORM_LOG_DEBUG("Keeping " << maybeStates.getNumberOfSetBits() << " rows.");
// Create the submatrix that only contains the states with a positive probability (including the // Create the submatrix that only contains the states with a positive probability (including the
// psi states) and reserve space for elements on the diagonal. // psi states) and reserve space for elements on the diagonal.
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = transitionMatrix.getSubmatrix(false, maybeStates, maybeStates, true); storm::storage::SparseMatrix<ValueType> uniformizedMatrix = transitionMatrix.getSubmatrix(false, maybeStates, maybeStates, true);
@ -240,7 +250,8 @@ namespace storm {
template<class ValueType> template<class ValueType>
template<bool computeCumulativeReward> template<bool computeCumulativeReward>
std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) const {
std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const& b, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) const {
ValueType lambda = timeBound * uniformizationRate; ValueType lambda = timeBound * uniformizationRate;
// If no time can pass, the current values are the result. // If no time can pass, the current values are the result.
@ -250,6 +261,7 @@ namespace storm {
// Use Fox-Glynn to get the truncation points and the weights. // Use Fox-Glynn to get the truncation points and the weights.
std::tuple<uint_fast64_t, uint_fast64_t, ValueType, std::vector<ValueType>> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::generalSettings().getPrecision() / 8.0); std::tuple<uint_fast64_t, uint_fast64_t, ValueType, std::vector<ValueType>> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::generalSettings().getPrecision() / 8.0);
STORM_LOG_DEBUG("Fox-Glynn cutoff points: left=" << std::get<0>(foxGlynnResult) << ", right=" << std::get<1>(foxGlynnResult));
// Scale the weights so they add up to one. // Scale the weights so they add up to one.
for (auto& element : std::get<3>(foxGlynnResult)) { for (auto& element : std::get<3>(foxGlynnResult)) {
@ -266,12 +278,16 @@ namespace storm {
} }
} }
STORM_LOG_DEBUG("Starting iterations with " << uniformizedMatrix.getRowCount() << " x " << uniformizedMatrix.getColumnCount() << " matrix.");
// Initialize result. // Initialize result.
std::vector<ValueType> result; std::vector<ValueType> result;
uint_fast64_t startingIteration = std::get<0>(foxGlynnResult); uint_fast64_t startingIteration = std::get<0>(foxGlynnResult);
if (startingIteration == 0) { if (startingIteration == 0) {
result = values; result = values;
storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]); storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]);
std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&foxGlynnResult] (ValueType const& a, ValueType const& b) { return a + std::get<3>(foxGlynnResult)[0] * b; };
storm::utility::vector::applyPointwiseInPlace(result, b, addAndScale);
++startingIteration; ++startingIteration;
} else { } else {
if (computeCumulativeReward) { if (computeCumulativeReward) {
@ -288,7 +304,7 @@ namespace storm {
if (!computeCumulativeReward && std::get<0>(foxGlynnResult) > 1) { if (!computeCumulativeReward && std::get<0>(foxGlynnResult) > 1) {
// Perform the matrix-vector multiplications (without adding). // Perform the matrix-vector multiplications (without adding).
solver->performMatrixVectorMultiplication(values, nullptr, std::get<0>(foxGlynnResult) - 1, &multiplicationResult);
solver->performMatrixVectorMultiplication(values, &b, std::get<0>(foxGlynnResult) - 1, &multiplicationResult);
} else if (computeCumulativeReward) { } else if (computeCumulativeReward) {
std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; }; std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; };
@ -304,7 +320,7 @@ namespace storm {
ValueType weight = 0; ValueType weight = 0;
std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; }; std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; };
for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) { for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) {
solver->performMatrixVectorMultiplication(values, nullptr, 1, &multiplicationResult);
solver->performMatrixVectorMultiplication(values, &b, 1, &multiplicationResult);
weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)]; weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)];
storm::utility::vector::applyPointwiseInPlace(result, values, addAndScale); storm::utility::vector::applyPointwiseInPlace(result, values, addAndScale);
@ -341,7 +357,7 @@ namespace storm {
STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector()); storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector());
result = this->computeTransientProbabilities(uniformizedMatrix, timeBound, uniformizationRate, result, *this->linearEquationSolverFactory);
result = this->computeTransientProbabilities(uniformizedMatrix, std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>()), timeBound, uniformizationRate, result, *this->linearEquationSolverFactory);
} }
return result; return result;
@ -386,7 +402,7 @@ namespace storm {
} }
// Finally, compute the transient probabilities. // Finally, compute the transient probabilities.
return this->computeTransientProbabilities<true>(uniformizedMatrix, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory);
return this->computeTransientProbabilities<true>(uniformizedMatrix, std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>()), timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory);
} }
template<class ValueType> template<class ValueType>

3
src/modelchecker/csl/SparseCtmcCslModelChecker.h
View File

@ -51,6 +51,7 @@ namespace storm {
* Computes the transient probabilities for lambda time steps. * Computes the transient probabilities for lambda time steps.
* *
* @param uniformizedMatrix The uniformized transition matrix. * @param uniformizedMatrix The uniformized transition matrix.
* @param b A vector that is added in each step as a possible compensation for the removed absorbing states.
* @param timeBound The time bound to use. * @param timeBound The time bound to use.
* @param uniformizationRate The used uniformization rate. * @param uniformizationRate The used uniformization rate.
* @param values A vector mapping each state to an initial probability. * @param values A vector mapping each state to an initial probability.
@ -60,7 +61,7 @@ namespace storm {
* @return The vector of transient probabilities. * @return The vector of transient probabilities.
*/ */
template<bool useMixedPoissonProbabilities = false> template<bool useMixedPoissonProbabilities = false>
std::vector<ValueType> computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) const;
std::vector<ValueType> computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, std::vector<ValueType> const& b, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) const;
/*! /*!
* Converts the given rate-matrix into a time-abstract probability matrix. * Converts the given rate-matrix into a time-abstract probability matrix.

8
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
View File

@ -106,7 +106,7 @@ namespace storm {
storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed); storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed);
// Now perform the inner value iteration for probabilistic states. // Now perform the inner value iteration for probabilistic states.
solver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
// (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic. // (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic.
aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian); aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian);
@ -119,7 +119,7 @@ namespace storm {
// After the loop, perform one more step of the value iteration for PS states. // After the loop, perform one more step of the value iteration for PS states.
aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic);
storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed); storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed);
solver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
} }
template<typename ValueType> template<typename ValueType>
@ -380,7 +380,7 @@ namespace storm {
std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size()); std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(sspMatrix); std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(sspMatrix);
solver->solveEquationSystem(minimize, sspMatrix, x, b);
solver->solveEquationSystem(minimize, x, b);
// Prepare result vector. // Prepare result vector.
std::vector<ValueType> result(model.getNumberOfStates()); std::vector<ValueType> result(model.getNumberOfStates());
@ -564,7 +564,7 @@ namespace storm {
// Solve the corresponding system of equations. // Solve the corresponding system of equations.
std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(submatrix); std::unique_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> solver = nondeterministicLinearEquationSolverFactory->create(submatrix);
solver->solveEquationSystem(minimize, submatrix, x, b);
solver->solveEquationSystem(minimize, x, b);
// Create resulting vector. // Create resulting vector.
std::vector<ValueType> result(model.getNumberOfStates()); std::vector<ValueType> result(model.getNumberOfStates());

4
src/settings/modules/GeneralSettings.cpp
View File

@ -233,6 +233,10 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'.");
} }
bool GeneralSettings::isEquationSolverSet() const {
return this->getOption(eqSolverOptionName).getHasOptionBeenSet();
}
GeneralSettings::LpSolver GeneralSettings::getLpSolver() const { GeneralSettings::LpSolver GeneralSettings::getLpSolver() const {
std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString();
if (lpSolverName == "gurobi") { if (lpSolverName == "gurobi") {

7
src/settings/modules/GeneralSettings.h
View File

@ -255,6 +255,13 @@ namespace storm {
*/ */
EquationSolver getEquationSolver() const; EquationSolver getEquationSolver() const;
/*!
* Retrieves whether a equation solver has been set.
*
* @return True iff an equation solver has been set.
*/
bool isEquationSolverSet() const;
/*! /*!
* Retrieves the selected LP solver. * Retrieves the selected LP solver.
* *

2
src/solver/GmmxxLinearEquationSolver.cpp
View File

@ -109,7 +109,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void GmmxxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// Set up some temporary variables so that we can just swap pointers instead of copying the result after // Set up some temporary variables so that we can just swap pointers instead of copying the result after
// each iteration. // each iteration.
std::vector<ValueType>* currentX = &x; std::vector<ValueType>* currentX = &x;

2
src/solver/GmmxxLinearEquationSolver.h
View File

@ -48,7 +48,7 @@ namespace storm {
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override; virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
private: private:
/*! /*!

2
src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
View File

@ -95,7 +95,7 @@ namespace storm {
void GmmxxNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const { void GmmxxNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
bool multiplyResultMemoryProvided = true; bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) { if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(rowGroupIndices.size() - 1);
multiplyResult = new std::vector<ValueType>(gmmxxMatrix->nr);
multiplyResultMemoryProvided = false; multiplyResultMemoryProvided = false;
} }

2
src/solver/LinearEquationSolver.h
View File

@ -39,7 +39,7 @@ namespace storm {
* @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this
* vector must be equal to the number of rows of A. * vector must be equal to the number of rows of A.
*/ */
virtual void performMatrixVectorMultiplication(std::vector<Type>& x, std::vector<Type>* b = nullptr, uint_fast64_t n = 1, std::vector<Type>* multiplyResult = nullptr) const = 0;
virtual void performMatrixVectorMultiplication(std::vector<Type>& x, std::vector<Type> const* b = nullptr, uint_fast64_t n = 1, std::vector<Type>* multiplyResult = nullptr) const = 0;
}; };
} // namespace solver } // namespace solver

2
src/solver/NativeLinearEquationSolver.cpp
View File

@ -83,7 +83,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void NativeLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// Set up some temporary variables so that we can just swap pointers instead of copying the result after // Set up some temporary variables so that we can just swap pointers instead of copying the result after
// each iteration. // each iteration.
std::vector<ValueType>* currentX = &x; std::vector<ValueType>* currentX = &x;

2
src/solver/NativeLinearEquationSolver.h
View File

@ -38,7 +38,7 @@ namespace storm {
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override; virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const override;
private: private:
/*! /*!

5
src/solver/TopologicalNondeterministicLinearEquationSolver.cpp
View File

@ -142,10 +142,7 @@ namespace storm {
storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true); storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true);
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(this->A, fullSystem, false, false); storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(this->A, fullSystem, false, false);
if (sccDecomposition.size() == 0) {
LOG4CPLUS_ERROR(logger, "Can not solve given Equation System as the SCC Decomposition returned no SCCs.");
throw storm::exceptions::IllegalArgumentException() << "Can not solve given Equation System as the SCC Decomposition returned no SCCs.";
}
STORM_LOG_THROW(sccDecomposition.size() > 0, storm::exceptions::IllegalArgumentException, "Can not solve given equation system as the SCC decomposition returned no SCCs.");
storm::storage::SparseMatrix<ValueType> stronglyConnectedComponentsDependencyGraph = sccDecomposition.extractPartitionDependencyGraph(this->A); storm::storage::SparseMatrix<ValueType> stronglyConnectedComponentsDependencyGraph = sccDecomposition.extractPartitionDependencyGraph(this->A);
std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);

1
src/utility/cli.h
View File

@ -66,7 +66,6 @@ log4cplus::Logger printer;
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h"
#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
// Headers for counterexample generation. // Headers for counterexample generation.

5
src/utility/solver.cpp
View File

@ -74,6 +74,11 @@ namespace storm {
return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name)); return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
} }
std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name) {
std::unique_ptr<storm::utility::solver::LpSolverFactory> factory(new LpSolverFactory());
return factory->create(name);
}
template class LinearEquationSolverFactory<double>; template class LinearEquationSolverFactory<double>;
template class GmmxxLinearEquationSolverFactory<double>; template class GmmxxLinearEquationSolverFactory<double>;
template class NativeLinearEquationSolverFactory<double>; template class NativeLinearEquationSolverFactory<double>;

2
src/utility/solver.h
View File

@ -81,6 +81,8 @@ namespace storm {
public: public:
virtual std::unique_ptr<storm::solver::LpSolver> create(std::string const& name) const override; virtual std::unique_ptr<storm::solver::LpSolver> create(std::string const& name) const override;
}; };
std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name);
} }
} }
} }

6
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -4,7 +4,7 @@
#include "src/settings/SettingMemento.h" #include "src/settings/SettingMemento.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/utility/solver.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
@ -17,7 +17,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -55,7 +55,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);

159
test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -0,0 +1,159 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/settings/SettingsManager.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/solver.h"
#include "src/parser/AutoParser.h"
TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(GmxxMdpPrctlModelCheckerTest, Consensus) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_0");
auto andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_1");
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
labelFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("agree");
auto notFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2);
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 50);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision());
}

84
test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -0,0 +1,84 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/solver.h"
#include "src/parser/AutoParser.h"
TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> 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", "", "");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.22968140721646868, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.22742305378217331, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 20);
result = checker.check(*boundedUntilFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
result = checker.check(*reachabilityRewardFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0252174454896057, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
}

6
test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp → test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -4,7 +4,7 @@
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/solver/NativeNondeterministicLinearEquationSolver.h"
#include "src/utility/solver.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
@ -17,7 +17,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -79,7 +79,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished"); auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);

12
test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -1,20 +1,20 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h"
#include "src/solver/NativeNondeterministicLinearEquationSolver.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/utility/solver.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h" #include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as<storm::models::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected"); auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
@ -81,12 +81,12 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
// Increase the maximal number of iterations, because the solver does not converge otherwise. // Increase the maximal number of iterations, because the solver does not converge otherwise.
// This is done in the main cpp unit // This is done in the main cpp unit
std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as<storm::models::Mdp<double>>();
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::modelchecker::SparseMdpPrctlModelChecker<double> mc(*mdp, std::unique_ptr<storm::utility::solver::NondeterministicLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory<double>()));
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished"); auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula); auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);

Write Preview
Loading…
Cancel
Save