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

Making libstorm compile again

main
TimQu 8 years ago
parent
0b0b5446cc
commit
6d23c79737
30 changed files with 141 additions and 157 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h
  2. 2
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h
  3. 2
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  4. 2
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  5. 2
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  6. 2
      src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
  7. 2
      src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  8. 2
      src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h
  9. 2
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  10. 6
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  11. 2
      src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
  12. 2
      src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
  13. 4
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  14. 34
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  15. 2
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
  16. 2
      src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  17. 4
      src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp
  18. 14
      src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  19. 12
      src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
  20. 59
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  21. 16
      src/storm/solver/IterativeMinMaxLinearEquationSolver.h
  22. 18
      src/storm/solver/LpMinMaxLinearEquationSolver.cpp
  23. 5
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  24. 2
      src/storm/solver/MinMaxLinearEquationSolver.h
  25. 2
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  26. 5
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
  27. 2
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
  28. 49
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
  29. 14
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
  30. 26
      src/test/storm/solver/EigenLinearEquationSolverTest.cpp

2
src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h
View File

@ -11,8 +11,6 @@
namespace storm {
class Environment;
namespace modelchecker {
template<typename ModelType>

2
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h
View File

@ -11,8 +11,6 @@
namespace storm {
class Environment;
namespace modelchecker {
template<class SparseCtmcModelType>

2
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -9,8 +9,6 @@
namespace storm {
class Environment;
namespace modelchecker {
template<typename SparseMarkovAutomatonModelType>

2
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
View File

@ -78,7 +78,7 @@ namespace storm {
EpochCheckingData cachedData;
ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
Environment newEnv = env;
newEnv.solver().minMax().setPrecision(precision);
newEnv.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(precision));
storm::utility::ProgressMeasurement progress("epochs");
progress.setMaxCount(epochOrder.size());
progress.startNewMeasurement(0);

2
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
View File

@ -187,7 +187,7 @@ namespace storm {
req.clearUpperBounds();
}
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
solver->setRequirementsChecked(env, true);
solver->setRequirementsChecked(true);
solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
// Use the (0...0) vector as initial guess for the solution.

2
src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
View File

@ -9,8 +9,6 @@
namespace storm {
class Environment;
namespace modelchecker {
template<typename ModelType>

2
src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
View File

@ -126,7 +126,7 @@ namespace storm {
template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ValueType>::translate(this->getModel());
std::unique_ptr<CheckResult> explicitResult = multiobjective::performMultiObjectiveModelChecking(*sparseModel, checkTask.getFormula());
std::unique_ptr<CheckResult> explicitResult = multiobjective::performMultiObjectiveModelChecking(env, *sparseModel, checkTask.getFormula());
// Convert the explicit result
if(explicitResult->isExplicitQualitativeCheckResult()) {

2
src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h
View File

@ -9,8 +9,6 @@
namespace storm {
class Environment;
namespace models {
namespace symbolic {
template<storm::dd::DdType Type, typename ValueType>

2
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
View File

@ -10,8 +10,6 @@
namespace storm {
namespace modelchecker {
class Environment;
template<class SparseDtmcModelType>
class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker<SparseDtmcModelType> {
public:

6
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -87,7 +87,7 @@ namespace storm {
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory);
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
@ -99,7 +99,7 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint());
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint());
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
@ -113,7 +113,7 @@ namespace storm {
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeGloballyProbabilities(storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeGloballyProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret)));
}

2
src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
View File

@ -8,8 +8,6 @@
namespace storm {
class Environment;
namespace modelchecker {
template<typename ModelType>
class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> {

2
src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
View File

@ -9,8 +9,6 @@
namespace storm {
class Environment;
namespace modelchecker {
template<typename ModelType>
class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<ModelType> {

4
src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
View File

@ -247,14 +247,14 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridMdpPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Maximize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory);
std::unique_ptr<CheckResult> result = computeUntilProbabilities(env, dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Maximize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory);
result->asQuantitativeCheckResult<ValueType>().oneMinus();
return result;
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) {
return SymbolicMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(dir, model, transitionMatrix, nextStates);
return SymbolicMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(env, dir, model, transitionMatrix, nextStates);
}
template<storm::dd::DdType DdType, typename ValueType>

34
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -33,7 +33,9 @@
#include "storm/utility/ProgressMeasurement.h"
#include "storm/utility/export.h"
#include "storm/environment/environments.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidPropertyException.h"
@ -147,7 +149,7 @@ namespace storm {
minMaxSolver->setOptimizationDirection(dir);
minMaxSolver->setCachingEnabled(true);
minMaxSolver->setTrackScheduler(true);
auto req = minMaxSolver->getRequirements(dir);
auto req = minMaxSolver->getRequirements(env, dir);
if (lowerBound) {
minMaxSolver->setLowerBound(lowerBound.get());
req.clearLowerBounds();
@ -200,7 +202,7 @@ namespace storm {
ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
Environment preciseEnv = env;
preciseEnv.solver().minMax().setPrecision(precision);
preciseEnv.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(precision));
// In case of cdf export we store the necessary data.
std::vector<std::vector<ValueType>> cdfData;
@ -217,7 +219,7 @@ namespace storm {
if (epochModel.epochMatrix.getEntryCount() == 0) {
rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialEpochModel<ValueType>(dir, epochModel));
} else {
rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel<ValueType>(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, precision, lowerBound, upperBound));
rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel<ValueType>(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, lowerBound, upperBound));
}
swCheck.stop();
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) {
@ -446,7 +448,7 @@ namespace storm {
// If the solver requires an initial scheduler, compute one now.
if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
result.schedulerHint = computeValidSchedulerHint(type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates);
result.schedulerHint = computeValidSchedulerHint(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates);
requirements.clearValidInitialScheduler();
}
@ -779,10 +781,10 @@ namespace storm {
}
}
return std::move(computeUntilProbabilities(std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).values);
return std::move(computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).values);
} else {
goal.oneMinus();
std::vector<ValueType> result = computeUntilProbabilities(std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values;
std::vector<ValueType> result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values;
for (auto& element : result) {
element = storm::utility::one<ValueType>() - element;
}
@ -830,7 +832,7 @@ namespace storm {
MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
// Only compute the result if the model has at least one reward this->getModel().
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
return computeReachabilityRewardsHelper(std::move(goal), transitionMatrix, backwardTransitions,
return computeReachabilityRewardsHelper(env, std::move(goal), transitionMatrix, backwardTransitions,
[&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
},
@ -842,7 +844,7 @@ namespace storm {
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
// Only compute the result if the reward model is not empty.
STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
return computeReachabilityRewardsHelper(std::move(goal), transitionMatrix, backwardTransitions, \
return computeReachabilityRewardsHelper(env, std::move(goal), transitionMatrix, backwardTransitions, \
[&] (uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
std::vector<ValueType> result;
result.reserve(rowCount);
@ -1154,7 +1156,7 @@ namespace storm {
std::vector<ValueType> stateRewards(psiStates.size(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(stateRewards, psiStates, storm::utility::one<ValueType>());
storm::models::sparse::StandardRewardModel<ValueType> rewardModel(std::move(stateRewards));
return computeLongRunAverageRewards(std::move(goal), transitionMatrix, backwardTransitions, rewardModel, minMaxLinearEquationSolverFactory);
return computeLongRunAverageRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, minMaxLinearEquationSolverFactory);
}
template<typename ValueType>
@ -1178,7 +1180,7 @@ namespace storm {
for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) {
storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex];
lraValuesForEndComponents[currentMecIndex] = computeLraForMaximalEndComponent(goal.direction(), transitionMatrix, rewardModel, mec, minMaxLinearEquationSolverFactory);
lraValuesForEndComponents[currentMecIndex] = computeLraForMaximalEndComponent(env, goal.direction(), transitionMatrix, rewardModel, mec, minMaxLinearEquationSolverFactory);
// Gather information for later use.
for (auto const& stateChoicesPair : mec) {
@ -1333,9 +1335,9 @@ namespace storm {
// Solve MEC with the method specified in the settings
storm::solver::LraMethod method = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>().getLraMethod();
if (method == storm::solver::LraMethod::LinearProgramming) {
return computeLraForMaximalEndComponentLP(dir, transitionMatrix, rewardModel, mec);
return computeLraForMaximalEndComponentLP(env, dir, transitionMatrix, rewardModel, mec);
} else if (method == storm::solver::LraMethod::ValueIteration) {
return computeLraForMaximalEndComponentVI(dir, transitionMatrix, rewardModel, mec, minMaxLinearEquationSolverFactory);
return computeLraForMaximalEndComponentVI(env, dir, transitionMatrix, rewardModel, mec, minMaxLinearEquationSolverFactory);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
@ -1517,7 +1519,7 @@ namespace storm {
STORM_LOG_DEBUG("Computing probabilities to satisfy condition.");
std::chrono::high_resolution_clock::time_point conditionStart = std::chrono::high_resolution_clock::now();
std::vector<ValueType> conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, extendedConditionStates, false, false, minMaxLinearEquationSolverFactory).values);
std::vector<ValueType> conditionProbabilities = std::move(computeUntilProbabilities(env, OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, extendedConditionStates, false, false, minMaxLinearEquationSolverFactory).values);
std::chrono::high_resolution_clock::time_point conditionEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Computed probabilities to satisfy for condition in " << std::chrono::duration_cast<std::chrono::milliseconds>(conditionEnd - conditionStart).count() << "ms.");
@ -1528,7 +1530,7 @@ namespace storm {
STORM_LOG_DEBUG("Computing probabilities to reach target.");
std::chrono::high_resolution_clock::time_point targetStart = std::chrono::high_resolution_clock::now();
std::vector<ValueType> targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).values);
std::vector<ValueType> targetProbabilities = std::move(computeUntilProbabilities(env, OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).values);
std::chrono::high_resolution_clock::time_point targetEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Computed probabilities to reach target in " << std::chrono::duration_cast<std::chrono::milliseconds>(targetEnd - targetStart).count() << "ms.");
@ -1620,7 +1622,7 @@ namespace storm {
}
std::chrono::high_resolution_clock::time_point conditionalStart = std::chrono::high_resolution_clock::now();
std::vector<ValueType> goalProbabilities = std::move(computeUntilProbabilities(std::move(goal), newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).values);
std::vector<ValueType> goalProbabilities = std::move(computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).values);
std::chrono::high_resolution_clock::time_point conditionalEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Computed conditional probabilities in transformed model in " << std::chrono::duration_cast<std::chrono::milliseconds>(conditionalEnd - conditionalStart).count() << "ms.");

2
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
View File

@ -45,8 +45,6 @@ namespace storm {
static std::vector<ValueType> computeNextProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
static std::vector<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false);

2
src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
View File

@ -120,7 +120,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory);
std::unique_ptr<CheckResult> result = computeUntilProbabilities(env, dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory);
result->asQuantitativeCheckResult<ValueType>().oneMinus();
return result;
}

4
src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp
View File

@ -29,7 +29,7 @@ namespace storm {
}
template<typename SparseModelType>
std::unique_ptr<CheckResult> SparsePropositionalModelChecker<SparseModelType>::checkBooleanLiteralFormula(Environment const& env,, CheckTask<storm::logic::BooleanLiteralFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparsePropositionalModelChecker<SparseModelType>::checkBooleanLiteralFormula(Environment const& env, CheckTask<storm::logic::BooleanLiteralFormula, ValueType> const& checkTask) {
storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula();
if (stateFormula.isTrueFormula()) {
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
@ -39,7 +39,7 @@ namespace storm {
}
template<typename SparseModelType>
std::unique_ptr<CheckResult> SparsePropositionalModelChecker<SparseModelType>::checkAtomicLabelFormula(Environment const& env,, CheckTask<storm::logic::AtomicLabelFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparsePropositionalModelChecker<SparseModelType>::checkAtomicLabelFormula(Environment const& env, CheckTask<storm::logic::AtomicLabelFormula, ValueType> const& checkTask) {
storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula();
STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel())));

14
src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -54,7 +54,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
@ -113,7 +113,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
// Do some sanity checks to establish some required properties.
RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : "");
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model.");
@ -320,7 +320,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
@ -426,7 +426,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
// Retrieve the appropriate bitvectors by model checking the subformulas.
@ -500,7 +500,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
// Retrieve the appropriate bitvectors by model checking the subformulas.
@ -597,7 +597,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) {
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(Environment const& env, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) {
storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
// Retrieve the appropriate bitvectors by model checking the subformulas.
@ -632,7 +632,7 @@ namespace storm {
STORM_LOG_INFO("The condition holds with probability 1, so the regular reachability probability is computed.");
std::shared_ptr<storm::logic::BooleanLiteralFormula> trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
std::shared_ptr<storm::logic::UntilFormula> untilFormula = std::make_shared<storm::logic::UntilFormula>(trueFormula, conditionalFormula.getSubformula().asSharedPointer());
return this->computeUntilProbabilities(*untilFormula);
return this->computeUntilProbabilities(env, *untilFormula);
}
// From now on, we know the condition does not have a trivial probability in the initial state.

12
src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
View File

@ -41,12 +41,12 @@ namespace storm {
// The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(Environment const& env, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
// Static helper methods
static std::unique_ptr<CheckResult> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly);

59
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View File

@ -34,6 +34,23 @@ namespace storm {
// Intentionally left empty.
}
template<typename ValueType>
MinMaxMethod IterativeMinMaxLinearEquationSolver<ValueType>::getMethod(Environment const& env, bool isExactMode) const {
// Adjust the method if none was specified and we are using rational numbers.
auto method = env.solver().minMax().getMethod();
if (isExactMode && method != MinMaxMethod::PolicyIteration && method != MinMaxMethod::RationalSearch) {
if (env.solver().minMax().isMethodSetFromDefault()) {
STORM_LOG_INFO("Selecting 'Policy iteration' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method.");
method = MinMaxMethod::PolicyIteration;
} else {
STORM_LOG_WARN("The selected solution method does not guarantee exact results.");
}
}
STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method.");
return method;
}
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool result = false;
@ -145,7 +162,7 @@ namespace storm {
// Update environment variables.
++iterations;
status = updateStatusIfNotConverged(status, x, iterations, dir == storm::OptimizationDirection::Minimize ? SolverGuarantee::GreaterOrEqual : SolverGuarantee::LessOrEqual);
status = updateStatusIfNotConverged(status, x, iterations, env.solver().minMax().getMaximalNumberOfIterations(), dir == storm::OptimizationDirection::Minimize ? SolverGuarantee::GreaterOrEqual : SolverGuarantee::LessOrEqual);
// Potentially show progress.
this->showProgressIterative(iterations);
@ -174,22 +191,6 @@ namespace storm {
}
}
MinMaxMethod getMethod(Environment const& env, bool isExactMode) {
// Adjust the method if none was specified and we are using rational numbers.
auto method = env.solver().minMax().getMethod();
if (isExactMode && method != MinMaxMethod::PolicyIteration || method != MinMaxMethod::RationalSearch) {
if (env.solver().minMax().isMethodSetFromDefault()) {
STORM_LOG_INFO("Selecting 'Policy iteration' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method.");
method = MinMaxMethod::PolicyIteration;
} else {
STORM_LOG_WARN("The selected solution method does not guarantee exact results.");
}
}
STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method.");
return method;
}
template<typename ValueType>
MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
// Start by copying the requirements of the linear equation solver.
@ -236,7 +237,7 @@ namespace storm {
}
template<typename ValueType>
typename IterativeMinMaxLinearEquationSolver<ValueType>::ValueIterationResult IterativeMinMaxLinearEquationSolver<ValueType>::performValueIteration(OptimizationDirection dir, std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX, std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations, storm::solver::MultiplicationStyle const& multiplicationStyle) const {
typename IterativeMinMaxLinearEquationSolver<ValueType>::ValueIterationResult IterativeMinMaxLinearEquationSolver<ValueType>::performValueIteration(OptimizationDirection dir, std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX, std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations, uint64_t maximalNumberOfIterations, storm::solver::MultiplicationStyle const& multiplicationStyle) const {
STORM_LOG_ASSERT(currentX != newX, "Vectors must not be aliased.");
@ -270,7 +271,7 @@ namespace storm {
// Update environment variables.
std::swap(currentX, newX);
++iterations;
status = updateStatusIfNotConverged(status, *currentX, iterations, guarantee);
status = updateStatusIfNotConverged(status, *currentX, iterations, maximalNumberOfIterations, guarantee);
// Potentially show progress.
this->showProgressIterative(iterations);
@ -327,7 +328,7 @@ namespace storm {
std::vector<ValueType>* currentX = &x;
this->startMeasureProgress();
ValueIterationResult result = performValueIteration(dir, currentX, newX, b, env.solver().minMax().getPrecision(), env.solver().minMax().getRelativeTerminationCriterion(), guarantee, 0);
ValueIterationResult result = performValueIteration(dir, currentX, newX, b, storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision()), env.solver().minMax().getRelativeTerminationCriterion(), guarantee, 0, env.solver().minMax().getMaximalNumberOfIterations(), env.solver().minMax().getMultiplicationStyle());
// Swap the result into the output x.
if (currentX == auxiliaryRowGroupVector.get()) {
@ -380,7 +381,7 @@ namespace storm {
* Model Checker: Interval Iteration for Markov Decision Processes, CAV 2017).
*/
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, storm::solver::MultiplicationStyle const& multiplicationStyle) const {
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(this->hasUpperBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
if (!this->linEqSolverA) {
@ -419,7 +420,7 @@ namespace storm {
ValueType maxLowerDiff = storm::utility::zero<ValueType>();
ValueType maxUpperDiff = storm::utility::zero<ValueType>();
bool relative = env.solver().minMax().getRelativeTerminationCriterion();
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision())
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
if (!relative) {
precision *= storm::utility::convertNumber<ValueType>(2.0);
}
@ -517,10 +518,10 @@ namespace storm {
++iterations;
doConvergenceCheck = !doConvergenceCheck;
if (lowerStep) {
status = updateStatusIfNotConverged(status, *lowerX, iterations, SolverGuarantee::LessOrEqual);
status = updateStatusIfNotConverged(status, *lowerX, iterations, env.solver().minMax().getMaximalNumberOfIterations(), SolverGuarantee::LessOrEqual);
}
if (upperStep) {
status = updateStatusIfNotConverged(status, *upperX, iterations, SolverGuarantee::GreaterOrEqual);
status = updateStatusIfNotConverged(status, *upperX, iterations, env.solver().minMax().getMaximalNumberOfIterations(), SolverGuarantee::GreaterOrEqual);
}
// Potentially show progress.
@ -785,7 +786,7 @@ namespace storm {
impreciseSolver.startMeasureProgress();
while (status == SolverStatus::InProgress && overallIterations < env.solver().minMax().getMaximalNumberOfIterations()) {
// Perform value iteration with the current precision.
typename IterativeMinMaxLinearEquationSolver<ImpreciseType>::ValueIterationResult result = impreciseSolver.performValueIteration(env, dir, currentX, newX, b, storm::utility::convertNumber<ImpreciseType, ValueType>(precision), env.solver().minMax().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, overallIterations);
typename IterativeMinMaxLinearEquationSolver<ImpreciseType>::ValueIterationResult result = impreciseSolver.performValueIteration(dir, currentX, newX, b, storm::utility::convertNumber<ImpreciseType, ValueType>(precision), env.solver().minMax().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, overallIterations, env.solver().minMax().getMaximalNumberOfIterations(), env.solver().minMax().getMultiplicationStyle());
// At this point, the result of the imprecise value iteration is stored in the (imprecise) current x.
@ -861,11 +862,11 @@ namespace storm {
}
template<typename ValueType>
SolverStatus IterativeMinMaxLinearEquationSolver<ValueType>::updateStatusIfNotConverged(Environment const& env, SolverStatus status, std::vector<ValueType> const& x, uint64_t iterations, SolverGuarantee const& guarantee) const {
SolverStatus IterativeMinMaxLinearEquationSolver<ValueType>::updateStatusIfNotConverged(SolverStatus status, std::vector<ValueType> const& x, uint64_t iterations, uint64_t maximalNumberOfIterations, SolverGuarantee const& guarantee) const {
if (status != SolverStatus::Converged) {
if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x, guarantee)) {
status = SolverStatus::TerminatedEarly;
} else if (iterations >= env.solver().minMax().getMaximalNumberOfIterations()) {
} else if (iterations >= maximalNumberOfIterations) {
status = SolverStatus::MaximalIterationsExceeded;
}
}
@ -910,7 +911,9 @@ namespace storm {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> IterativeMinMaxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized.");
auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
auto method = env.solver().minMax().getMethod();
STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone());
result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;

16
src/storm/solver/IterativeMinMaxLinearEquationSolver.h
View File

@ -29,6 +29,9 @@ namespace storm {
virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
private:
MinMaxMethod getMethod(Environment const& env, bool isExactMode) const;
bool solveInducedEquationSystem(Environment const& env, std::unique_ptr<LinearEquationSolver<ValueType>>& linearEquationSolver, std::vector<uint64_t> const& scheduler, std::vector<ValueType>& x, std::vector<ValueType>& subB, std::vector<ValueType> const& originalB) const;
bool solveEquationsPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
@ -40,11 +43,11 @@ namespace storm {
template<typename RationalType, typename ImpreciseType>
bool solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, IterativeMinMaxLinearEquationSolver<ImpreciseType> const& impreciseSolver, storm::storage::SparseMatrix<RationalType> const& rationalA, std::vector<RationalType>& rationalX, std::vector<RationalType> const& rationalB, storm::storage::SparseMatrix<ImpreciseType> const& A, std::vector<ImpreciseType>& x, std::vector<ImpreciseType> const& b, std::vector<ImpreciseType>& tmpX) const;
template<typename ImpreciseType>
typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && !NumberTraits<ValueType>::IsExact, bool>::type solveEquationsRationalSearchHelper(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && !NumberTraits<ValueType>::IsExact, bool>::type solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
template<typename ImpreciseType>
typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && NumberTraits<ValueType>::IsExact, bool>::type solveEquationsRationalSearchHelper(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && NumberTraits<ValueType>::IsExact, bool>::type solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
template<typename ImpreciseType>
typename std::enable_if<!std::is_same<ValueType, ImpreciseType>::value, bool>::type solveEquationsRationalSearchHelper(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
typename std::enable_if<!std::is_same<ValueType, ImpreciseType>::value, bool>::type solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
template<typename RationalType, typename ImpreciseType>
static bool sharpen(storm::OptimizationDirection dir, uint64_t precision, storm::storage::SparseMatrix<RationalType> const& A, std::vector<ImpreciseType> const& x, std::vector<RationalType> const& b, std::vector<RationalType>& tmp);
static bool isSolution(storm::OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& matrix, std::vector<ValueType> const& values, std::vector<ValueType> const& b);
@ -63,7 +66,7 @@ namespace storm {
template <typename ValueTypePrime>
friend class IterativeMinMaxLinearEquationSolver;
ValueIterationResult performValueIteration(OptimizationDirection dir, std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX, std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations, storm::solver::MultiplicationStyle const& multiplicationStyle) const;
ValueIterationResult performValueIteration(OptimizationDirection dir, std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX, std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations, uint64_t maximalNumberOfIterations, storm::solver::MultiplicationStyle const& multiplicationStyle) const;
void createLinearEquationSolver() const;
@ -72,11 +75,8 @@ namespace storm {
mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector2; // A.rowGroupCount() entries
mutable std::unique_ptr<std::vector<uint64_t>> rowGroupOrdering; // A.rowGroupCount() entries
SolverStatus updateStatusIfNotConverged(SolverStatus status, std::vector<ValueType> const& x, uint64_t iterations, SolverGuarantee const& guarantee) const;
SolverStatus updateStatusIfNotConverged(SolverStatus status, std::vector<ValueType> const& x, uint64_t iterations, uint64_t maximalNumberOfIterations, SolverGuarantee const& guarantee) const;
static void reportStatus(SolverStatus status, uint64_t iterations);
/// The settings of this solver.
IterativeMinMaxLinearEquationSolverSettings<ValueType> settings;
};
template<typename ValueType>

18
src/storm/solver/LpMinMaxLinearEquationSolver.cpp
View File

@ -1,6 +1,8 @@
#include <storm/exceptions/InvalidEnvironmentException.h>
#include "storm/solver/LpMinMaxLinearEquationSolver.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/utility/vector.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidEnvironmentException.h"
@ -27,7 +29,7 @@ namespace storm {
template<typename ValueType>
bool LpMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(env.solver().minMax().getMethod == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique.")
STORM_LOG_THROW(env.solver().minMax().getMethod() == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique.");
// Set up the LP solver
std::unique_ptr<storm::solver::LpSolver<ValueType>> solver = lpSolverFactory->create("");
@ -84,7 +86,7 @@ namespace storm {
}
// If requested, we store the scheduler for retrieval.
if (env.solver().minMax().isTrackSchedulerSet()) {
if (this->isTrackSchedulerSet()) {
this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) {
uint64_t row = this->A->getRowGroupIndices()[rowGroup];
@ -116,7 +118,7 @@ namespace storm {
MinMaxLinearEquationSolverRequirements requirements;
// In case we need to retrieve a scheduler, the solution has to be unique
if (!this->hasUniqueSolution() && env.solver().minMax().isTrackSchedulerSet()) {
if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) {
requirements.requireNoEndComponents();
}
@ -124,23 +126,23 @@ namespace storm {
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory<ValueType>(), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
// Intentionally left empty
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory<ValueType>(), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory<ValueType>(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory<ValueType>(std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> LpMinMaxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
STORM_LOG_THROW(env.solver().minMax().getMethod == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique.")
STORM_LOG_THROW(env.solver().minMax().getMethod() == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique.");
STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized.");
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized.");

5
src/storm/solver/MinMaxLinearEquationSolver.cpp
View File

@ -32,13 +32,13 @@ namespace storm {
template<typename ValueType>
bool MinMaxLinearEquationSolver<ValueType>::solveEquations(Environment const& env, OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_WARN_COND_DEBUG(this->isRequirementsCheckedSet(), "The requirements of the solver have not been marked as checked. Please provide the appropriate check or mark the requirements as checked (if applicable).");
return internalSolveEquations(Environment const& env, d, x, b);
return internalSolveEquations(env, d, x, b);
}
template<typename ValueType>
void MinMaxLinearEquationSolver<ValueType>::solveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(isSet(this->direction), storm::exceptions::IllegalFunctionCallException, "Optimization direction not set.");
solveEquations(Environment const& env, convert(this->direction), x, b);
solveEquations(env, convert(this->direction), x, b);
}
template<typename ValueType>
@ -216,7 +216,6 @@ namespace storm {
std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> result;
auto method = env.solver().minMax().getMethod();
if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch) {
IterativeMinMaxLinearEquationSolverSettings<storm::RationalNumber> iterativeSolverSettings;
result = std::make_unique<IterativeMinMaxLinearEquationSolver<storm::RationalNumber>>(std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>());
} else if (method == MinMaxMethod::LinearProgramming) {
result = std::make_unique<LpMinMaxLinearEquationSolver<storm::RationalNumber>>(std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>(), std::make_unique<storm::utility::solver::LpSolverFactory<storm::RationalNumber>>());

2
src/storm/solver/MinMaxLinearEquationSolver.h
View File

@ -181,7 +181,7 @@ namespace storm {
bool isRequirementsCheckedSet() const;
protected:
virtual bool internalSolveEquations(OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const& b) const = 0;
virtual bool internalSolveEquations(Environment const& env, OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const& b) const = 0;
/// The optimization direction to use for calls to functions that do not provide it explicitly. Can also be unset.
OptimizationDirectionSetting direction;

2
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -83,7 +83,7 @@ namespace storm {
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverFactory<ValueType>::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, MinMaxMethodSelection) : MinMaxLinearEquationSolverFactory<ValueType>(), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) {
StandardMinMaxLinearEquationSolverFactory<ValueType>::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : MinMaxLinearEquationSolverFactory<ValueType>(), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) {
// Intentionally left empty.
}

5
src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
View File

@ -29,7 +29,8 @@ namespace storm {
// Intentionally left empty.
}
MinMaxMethod getMethod(Environment const& env, bool isExactMode) {
template<storm::dd::DdType DdType, typename ValueType>
MinMaxMethod SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getMethod(Environment const& env, bool isExactMode) const {
// Adjust the method if none was specified and we are using rational numbers.
auto method = env.solver().minMax().getMethod();
@ -222,7 +223,7 @@ namespace storm {
STORM_LOG_WARN("Precision of value type was exceeded, trying to recover by switching to rational arithmetic.");
// Fall back to precise value type if the precision of the imprecise value type was exceeded.
rationalResult = solveEquationsRationalSearchHelper<ValueType, ValueType>(dir, *this, *this, b, impreciseX.template toValueType<ValueType>(), b);
rationalResult = solveEquationsRationalSearchHelper<ValueType, ValueType>(env, dir, *this, *this, b, impreciseX.template toValueType<ValueType>(), b);
}
return rationalResult.template toValueType<ValueType>();
}

2
src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
View File

@ -133,6 +133,8 @@ namespace storm {
private:
MinMaxMethod getMethod(Environment const& env, bool isExactMode) const;
storm::dd::Add<DdType, ValueType> solveEquationsWithScheduler(storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
storm::dd::Add<DdType, ValueType> solveEquationsWithScheduler(SymbolicLinearEquationSolver<DdType, ValueType>& solver, storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b, storm::dd::Add<DdType, ValueType> const& diagonal) const;

49
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -1,12 +1,15 @@
#include "storm/solver/TopologicalMinMaxLinearEquationSolver.h"
#include <utility>
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidEnvironmentException.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
@ -21,7 +24,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver() {
// Get the settings object to customize solving.
this->enableCuda = storm::settings::getModule<storm::settings::modules::CoreSettings>().isUseCudaSet();
#ifdef STORM_HAVE_CUDA
@ -30,7 +33,7 @@ namespace storm {
}
template<typename ValueType>
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : TopologicalMinMaxLinearEquationSolver(precision, maximalNumberOfIterations, relative) {
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : TopologicalMinMaxLinearEquationSolver() {
this->setMatrix(A);
}
@ -47,7 +50,12 @@ namespace storm {
}
template<typename ValueType>
bool TopologicalMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool TopologicalMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(env.solver().minMax().getMethod() == MinMaxMethod::Topological, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique.");
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
uint64_t maxIters = env.solver().minMax().getMaximalNumberOfIterations();
bool relative = env.solver().minMax().getMaximalNumberOfIterations();
#ifdef GPU_USE_FLOAT
#define __FORCE_FLOAT_CALCULATION true
@ -58,12 +66,12 @@ namespace storm {
// FIXME: This actually allocates quite some storage, because of this conversion, is it really necessary?
storm::storage::SparseMatrix<float> newA = this->A->template toValueType<float>();
TopologicalMinMaxLinearEquationSolver<float> newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative);
TopologicalMinMaxLinearEquationSolver<float> newSolver(newA);
std::vector<float> new_x = storm::utility::vector::toValueType<float>(x);
std::vector<float> const new_b = storm::utility::vector::toValueType<float>(b);
bool callConverged = newSolver.solveEquations(dir, new_x, new_b);
bool callConverged = newSolver.solveEquations(env, dir, new_x, new_b);
for (size_t i = 0, size = new_x.size(); i < size; ++i) {
x.at(i) = new_x.at(i);
@ -104,9 +112,9 @@ namespace storm {
bool result = false;
size_t globalIterations = 0;
if (dir == OptimizationDirection::Minimize) {
result = __basicValueIteration_mvReduce_minimize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
result = __basicValueIteration_mvReduce_minimize<uint_fast64_t, ValueType>(maxIters, precision, relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
} else {
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(maxIters, precision, relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
}
STORM_LOG_INFO("Executed " << globalIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
@ -206,9 +214,9 @@ namespace storm {
bool result = false;
localIterations = 0;
if (dir == OptimizationDirection::Minimum) {
result = __basicValueIteration_mvReduce_minimize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations);
result = __basicValueIteration_mvReduce_minimize<uint_fast64_t, ValueType>(maxIters, precision, relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations);
} else {
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations);
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(maxIters, precision, relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations);
}
STORM_LOG_INFO("Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
@ -235,7 +243,7 @@ namespace storm {
STORM_LOG_INFO("Performance Warning: Using CPU based TopoSolver! (double)");
localIterations = 0;
converged = false;
while (!converged && localIterations < this->maximalNumberOfIterations) {
while (!converged && localIterations < maxIters) {
// Compute x' = A*x + b.
sccSubmatrix.multiplyWithVector(*currentX, sccMultiplyResult);
storm::utility::vector::addVectors<ValueType>(sccMultiplyResult, sccSubB, sccMultiplyResult);
@ -256,7 +264,7 @@ namespace storm {
// TODO: It seems that the equalModuloPrecision call that compares all values should have a higher
// running time. In fact, it is faster. This has to be investigated.
// converged = storm::utility::equalModuloPrecision(*currentX, *newX, scc, precision, relative);
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *swap, static_cast<ValueType>(this->precision), this->relative);
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *swap, precision, relative);
// Update environment variables.
std::swap(currentX, swap);
@ -264,7 +272,7 @@ namespace storm {
++localIterations;
++globalIterations;
}
STORM_LOG_INFO("Executed " << localIterations << " of max. " << this->maximalNumberOfIterations << " Iterations.");
STORM_LOG_INFO("Executed " << localIterations << " of max. " << maxIters << " Iterations.");
}
@ -441,16 +449,6 @@ namespace storm {
return result;
}
template<typename ValueType>
ValueType TopologicalMinMaxLinearEquationSolver<ValueType>::getPrecision() const {
return this->precision;
}
template<typename ValueType>
bool TopologicalMinMaxLinearEquationSolver<ValueType>::getRelative() const {
return this->relative;
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
std::unique_ptr<std::vector<ValueType>> multiplyResult = std::make_unique<std::vector<ValueType>>(this->A->getRowCount());
@ -471,12 +469,13 @@ namespace storm {
}
template<typename ValueType>
TopologicalMinMaxLinearEquationSolverFactory<ValueType>::TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler) : MinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::Topological, trackScheduler) {
TopologicalMinMaxLinearEquationSolverFactory<ValueType>::TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler) {
// Intentionally left empty.
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create() const {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
STORM_LOG_THROW(env.solver().minMax().getMethod() == MinMaxMethod::Topological, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique.");
return std::make_unique<TopologicalMinMaxLinearEquationSolver<ValueType>>();
}

14
src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
View File

@ -24,7 +24,7 @@ namespace storm {
template<class ValueType>
class TopologicalMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
public:
TopologicalMinMaxLinearEquationSolver(double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true);
TopologicalMinMaxLinearEquationSolver();
/*!
* Constructs a min-max linear equation solver with parameters being set according to the settings
@ -32,24 +32,18 @@ namespace storm {
*
* @param A The matrix defining the coefficients of the linear equation system.
*/
TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true);
TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A);
virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) override;
virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) override;
virtual bool internalSolveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const override;
ValueType getPrecision() const;
bool getRelative() const;
private:
storm::storage::SparseMatrix<ValueType> const* A;
std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localA;
double precision;
uint_fast64_t maximalNumberOfIterations;
bool relative;
bool enableCuda;
/*!
@ -151,7 +145,7 @@ namespace storm {
TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler = false);
protected:
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create() const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(Environment const& env) const override;
};
} // namespace solver

26
src/test/storm/solver/EigenLinearEquationSolverTest.cpp
View File

@ -29,7 +29,7 @@ TEST(EigenLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver<double> solver(A));
storm::solver::EigenLinearEquationSolver<double> solver(A);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -58,7 +58,7 @@ TEST(EigenLinearEquationSolver, SparseLU) {
solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings<double>::SolutionMethod::SparseLU);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::None);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -85,7 +85,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) {
std::vector<storm::RationalNumber> b = {16, -4, -7};
storm::solver::EigenLinearEquationSolver<storm::RationalNumber> solver(A);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_TRUE(storm::utility::isOne(x[0]));
ASSERT_TRUE(x[1] == 3);
ASSERT_TRUE(x[2] == -1);
@ -111,7 +111,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalFunction) {
std::vector<storm::RationalFunction> b = {storm::RationalFunction(16), storm::RationalFunction(-4), storm::RationalFunction(-7)};
storm::solver::EigenLinearEquationSolver<storm::RationalFunction> solver(A);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_TRUE(storm::utility::isOne(x[0]));
ASSERT_TRUE(x[1] == storm::RationalFunction(3));
ASSERT_TRUE(x[2] == storm::RationalFunction(-1));
@ -144,7 +144,7 @@ TEST(EigenLinearEquationSolver, DGMRES) {
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::None);
solver.getSettings().setNumberOfIterationsUntilRestart(50);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -174,7 +174,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Ilu) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::Ilu);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -204,7 +204,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Diagonal) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::Diagonal);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -236,7 +236,7 @@ TEST(EigenLinearEquationSolver, GMRES) {
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::None);
solver.getSettings().setNumberOfIterationsUntilRestart(50);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -266,7 +266,7 @@ TEST(EigenLinearEquationSolver, GMRES_Ilu) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::Ilu);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -296,7 +296,7 @@ TEST(EigenLinearEquationSolver, GMRES_Diagonal) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::Diagonal);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -327,7 +327,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB) {
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::None);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -357,7 +357,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Ilu) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::Ilu);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
@ -387,7 +387,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Diagonal) {
solver.getSettings().setPrecision(1e-6);
solver.getSettings().setMaximalNumberOfIterations(10000);
solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings<double>::Preconditioner::Diagonal);
ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_NO_THROW(solver.solveEquations(env, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());

Write Preview
Loading…
Cancel
Save