diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h index f4728c663..19189f361 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -11,8 +11,6 @@ namespace storm { - class Environment; - namespace modelchecker { template diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index 23095377d..86a43778e 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -11,8 +11,6 @@ namespace storm { - class Environment; - namespace modelchecker { template diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index d63c635ca..57b1a63a6 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -9,8 +9,6 @@ namespace storm { - class Environment; - namespace modelchecker { template diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 95c3052c5..9dc4c1925 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -78,7 +78,7 @@ namespace storm { EpochCheckingData cachedData; ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber(storm::settings::getModule().getPrecision())); Environment newEnv = env; - newEnv.solver().minMax().setPrecision(precision); + newEnv.solver().minMax().setPrecision(storm::utility::convertNumber(precision)); storm::utility::ProgressMeasurement progress("epochs"); progress.setMaxCount(epochOrder.size()); progress.startNewMeasurement(0); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index ff74ed473..22fb31b64 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -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. diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index be7738276..2b69dda58 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -9,8 +9,6 @@ namespace storm { - class Environment; - namespace modelchecker { template diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 7c8f3e7a8..12524aed6 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -126,7 +126,7 @@ namespace storm { template std::unique_ptr HybridMdpPrctlModelChecker::checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) { auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer::translate(this->getModel()); - std::unique_ptr explicitResult = multiobjective::performMultiObjectiveModelChecking(*sparseModel, checkTask.getFormula()); + std::unique_ptr explicitResult = multiobjective::performMultiObjectiveModelChecking(env, *sparseModel, checkTask.getFormula()); // Convert the explicit result if(explicitResult->isExplicitQualitativeCheckResult()) { diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 01b4feb77..cff28c1ca 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -9,8 +9,6 @@ namespace storm { - class Environment; - namespace models { namespace symbolic { template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 7a00d7578..c4284218a 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -10,8 +10,6 @@ namespace storm { namespace modelchecker { - class Environment; - template class SparseDtmcPrctlModelChecker : public SparsePropositionalModelChecker { public: diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 680b7ed27..bb51f372d 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -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 subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -99,7 +99,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal(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::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().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 subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret))); } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 4dd023b4a..f0f09d965 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -8,8 +8,6 @@ namespace storm { - class Environment; - namespace modelchecker { template class SymbolicDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index b2369ca22..aac5b6aed 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -9,8 +9,6 @@ namespace storm { - class Environment; - namespace modelchecker { template class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 42df4009e..6b3ea5b6a 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -247,14 +247,14 @@ namespace storm { template std::unique_ptr HybridMdpPrctlHelper::computeGloballyProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { - std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Maximize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + std::unique_ptr result = computeUntilProbabilities(env, dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Maximize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); result->asQuantitativeCheckResult().oneMinus(); return result; } template std::unique_ptr HybridMdpPrctlHelper::computeNextProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { - return SymbolicMdpPrctlHelper::computeNextProbabilities(dir, model, transitionMatrix, nextStates); + return SymbolicMdpPrctlHelper::computeNextProbabilities(env, dir, model, transitionMatrix, nextStates); } template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 84f4e9327..ddf726015 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -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(storm::settings::getModule().getPrecision())); Environment preciseEnv = env; - preciseEnv.solver().minMax().setPrecision(precision); + preciseEnv.solver().minMax().setPrecision(storm::utility::convertNumber(precision)); // In case of cdf export we store the necessary data. std::vector> cdfData; @@ -217,7 +219,7 @@ namespace storm { if (epochModel.epochMatrix.getEntryCount() == 0) { rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialEpochModel(dir, epochModel)); } else { - rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, precision, lowerBound, upperBound)); + rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel(preciseEnv, dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, lowerBound, upperBound)); } swCheck.stop(); if (storm::settings::getModule().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 result = computeUntilProbabilities(std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values; + std::vector 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() - element; } @@ -830,7 +832,7 @@ namespace storm { MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory 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 const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); }, @@ -842,7 +844,7 @@ namespace storm { std::vector SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory 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 const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result; result.reserve(rowCount); @@ -1154,7 +1156,7 @@ namespace storm { std::vector stateRewards(psiStates.size(), storm::utility::zero()); storm::utility::vector::setVectorValues(stateRewards, psiStates, storm::utility::one()); storm::models::sparse::StandardRewardModel rewardModel(std::move(stateRewards)); - return computeLongRunAverageRewards(std::move(goal), transitionMatrix, backwardTransitions, rewardModel, minMaxLinearEquationSolverFactory); + return computeLongRunAverageRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, minMaxLinearEquationSolverFactory); } template @@ -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().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 conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, extendedConditionStates, false, false, minMaxLinearEquationSolverFactory).values); + std::vector 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(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 targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).values); + std::vector 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(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 goalProbabilities = std::move(computeUntilProbabilities(std::move(goal), newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).values); + std::vector 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(conditionalEnd - conditionalStart).count() << "ms."); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 1a08a09ec..b06b14192 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -45,8 +45,6 @@ namespace storm { static std::vector computeNextProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 679ec815e..791c49c46 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -120,7 +120,7 @@ namespace storm { template std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(Environment const& env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { - std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + std::unique_ptr result = computeUntilProbabilities(env, dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); result->asQuantitativeCheckResult().oneMinus(); return result; } diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 008074bac..e0497b95e 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -29,7 +29,7 @@ namespace storm { } template - std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(Environment const& env,, CheckTask const& checkTask) { + std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(Environment const& env, CheckTask const& checkTask) { storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); @@ -39,7 +39,7 @@ namespace storm { } template - std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(Environment const& env,, CheckTask const& checkTask) { + std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(Environment const& env, CheckTask 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(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 77d482333..2798d9c74 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -54,7 +54,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -113,7 +113,7 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask 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 - std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask 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 - std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(Environment const& env, CheckTask 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 - std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask 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 - std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(Environment const& env, CheckTask 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 trueFormula = std::make_shared(true); std::shared_ptr untilFormula = std::make_shared(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. diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 6dd387725..ad3d9039c 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -41,12 +41,12 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; // Static helper methods static std::unique_ptr computeUntilProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index b8d7ded00..4c4f20bc6 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -34,6 +34,23 @@ namespace storm { // Intentionally left empty. } + template + MinMaxMethod IterativeMinMaxLinearEquationSolver::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 bool IterativeMinMaxLinearEquationSolver::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector 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 MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction) const { // Start by copying the requirements of the linear equation solver. @@ -236,7 +237,7 @@ namespace storm { } template - typename IterativeMinMaxLinearEquationSolver::ValueIterationResult IterativeMinMaxLinearEquationSolver::performValueIteration(OptimizationDirection dir, std::vector*& currentX, std::vector*& newX, std::vector const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations, storm::solver::MultiplicationStyle const& multiplicationStyle) const { + typename IterativeMinMaxLinearEquationSolver::ValueIterationResult IterativeMinMaxLinearEquationSolver::performValueIteration(OptimizationDirection dir, std::vector*& currentX, std::vector*& newX, std::vector 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* 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(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 - bool IterativeMinMaxLinearEquationSolver::solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b, storm::solver::MultiplicationStyle const& multiplicationStyle) const { + bool IterativeMinMaxLinearEquationSolver::solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector 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 maxUpperDiff = storm::utility::zero(); bool relative = env.solver().minMax().getRelativeTerminationCriterion(); - ValueType precision = storm::utility::convertNumber(env.solver().minMax().getPrecision()) + ValueType precision = storm::utility::convertNumber(env.solver().minMax().getPrecision()); if (!relative) { precision *= storm::utility::convertNumber(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::ValueIterationResult result = impreciseSolver.performValueIteration(env, dir, currentX, newX, b, storm::utility::convertNumber(precision), env.solver().minMax().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, overallIterations); + typename IterativeMinMaxLinearEquationSolver::ValueIterationResult result = impreciseSolver.performValueIteration(dir, currentX, newX, b, storm::utility::convertNumber(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 - SolverStatus IterativeMinMaxLinearEquationSolver::updateStatusIfNotConverged(Environment const& env, SolverStatus status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const { + SolverStatus IterativeMinMaxLinearEquationSolver::updateStatusIfNotConverged(SolverStatus status, std::vector 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> IterativeMinMaxLinearEquationSolverFactory::create(Environment const& env) const { STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); - auto method = getMethod(env, std::is_same::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> result = std::make_unique>(this->linearEquationSolverFactory->clone()); result->setRequirementsChecked(this->isRequirementsCheckedSet()); return result; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index 98a865a06..f97808592 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -29,6 +29,9 @@ namespace storm { virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none) const override; private: + + MinMaxMethod getMethod(Environment const& env, bool isExactMode) const; + bool solveInducedEquationSystem(Environment const& env, std::unique_ptr>& linearEquationSolver, std::vector const& scheduler, std::vector& x, std::vector& subB, std::vector const& originalB) const; bool solveEquationsPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; @@ -40,11 +43,11 @@ namespace storm { template bool solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, IterativeMinMaxLinearEquationSolver const& impreciseSolver, storm::storage::SparseMatrix const& rationalA, std::vector& rationalX, std::vector const& rationalB, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector& tmpX) const; template - typename std::enable_if::value && !NumberTraits::IsExact, bool>::type solveEquationsRationalSearchHelper(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + typename std::enable_if::value && !NumberTraits::IsExact, bool>::type solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; template - typename std::enable_if::value && NumberTraits::IsExact, bool>::type solveEquationsRationalSearchHelper(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + typename std::enable_if::value && NumberTraits::IsExact, bool>::type solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; template - typename std::enable_if::value, bool>::type solveEquationsRationalSearchHelper(OptimizationDirection dir, std::vector& x, std::vector const& b) const; + typename std::enable_if::value, bool>::type solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; template static bool sharpen(storm::OptimizationDirection dir, uint64_t precision, storm::storage::SparseMatrix const& A, std::vector const& x, std::vector const& b, std::vector& tmp); static bool isSolution(storm::OptimizationDirection dir, storm::storage::SparseMatrix const& matrix, std::vector const& values, std::vector const& b); @@ -63,7 +66,7 @@ namespace storm { template friend class IterativeMinMaxLinearEquationSolver; - ValueIterationResult performValueIteration(OptimizationDirection dir, std::vector*& currentX, std::vector*& newX, std::vector 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*& currentX, std::vector*& newX, std::vector 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> auxiliaryRowGroupVector2; // A.rowGroupCount() entries mutable std::unique_ptr> rowGroupOrdering; // A.rowGroupCount() entries - SolverStatus updateStatusIfNotConverged(SolverStatus status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const; + SolverStatus updateStatusIfNotConverged(SolverStatus status, std::vector 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 settings; }; template diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 4e801ab4e..c0171aaa0 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -1,6 +1,8 @@ -#include #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 bool LpMinMaxLinearEquationSolver::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector 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> 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(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 - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming), lpSolverFactory(std::make_unique>()) { + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory(), lpSolverFactory(std::make_unique>()) { // Intentionally left empty } template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory(), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty } template - LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming), lpSolverFactory(std::move(lpSolverFactory)) { + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory(std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { // Intentionally left empty } template std::unique_ptr> LpMinMaxLinearEquationSolverFactory::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."); diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index ca3ff87dc..deb55f3b4 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -32,13 +32,13 @@ namespace storm { template bool MinMaxLinearEquationSolver::solveEquations(Environment const& env, OptimizationDirection d, std::vector& x, std::vector 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 void MinMaxLinearEquationSolver::solveEquations(Environment const& env, std::vector& x, std::vector 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 @@ -216,7 +216,6 @@ namespace storm { std::unique_ptr> result; auto method = env.solver().minMax().getMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch) { - IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::LinearProgramming) { result = std::make_unique>(std::make_unique>(), std::make_unique>()); diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 48092cf7b..a6b371dfb 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -181,7 +181,7 @@ namespace storm { bool isRequirementsCheckedSet() const; protected: - virtual bool internalSolveEquations(OptimizationDirection d, std::vector& x, std::vector const& b) const = 0; + virtual bool internalSolveEquations(Environment const& env, OptimizationDirection d, std::vector& x, std::vector 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; diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 43eab9e9d..16158afaa 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -83,7 +83,7 @@ namespace storm { } template - StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, MinMaxMethodSelection) : MinMaxLinearEquationSolverFactory(), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory) : MinMaxLinearEquationSolverFactory(), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 8ab33861d..b33a649a0 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -29,7 +29,8 @@ namespace storm { // Intentionally left empty. } - MinMaxMethod getMethod(Environment const& env, bool isExactMode) { + template + MinMaxMethod SymbolicMinMaxLinearEquationSolver::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(dir, *this, *this, b, impreciseX.template toValueType(), b); + rationalResult = solveEquationsRationalSearchHelper(env, dir, *this, *this, b, impreciseX.template toValueType(), b); } return rationalResult.template toValueType(); } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 043dbd638..ae76f8759 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -133,6 +133,8 @@ namespace storm { private: + MinMaxMethod getMethod(Environment const& env, bool isExactMode) const; + storm::dd::Add solveEquationsWithScheduler(storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b) const; storm::dd::Add solveEquationsWithScheduler(SymbolicLinearEquationSolver& solver, storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b, storm::dd::Add const& diagonal) const; diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index c658ac1ed..11eb9e505 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -1,12 +1,15 @@ #include "storm/solver/TopologicalMinMaxLinearEquationSolver.h" -#include #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 - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver() { // Get the settings object to customize solving. this->enableCuda = storm::settings::getModule().isUseCudaSet(); #ifdef STORM_HAVE_CUDA @@ -30,7 +33,7 @@ namespace storm { } template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : TopologicalMinMaxLinearEquationSolver(precision, maximalNumberOfIterations, relative) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : TopologicalMinMaxLinearEquationSolver() { this->setMatrix(A); } @@ -47,7 +50,12 @@ namespace storm { } template - bool TopologicalMinMaxLinearEquationSolver::internalSolveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + bool TopologicalMinMaxLinearEquationSolver::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector 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(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 newA = this->A->template toValueType(); - TopologicalMinMaxLinearEquationSolver newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative); + TopologicalMinMaxLinearEquationSolver newSolver(newA); std::vector new_x = storm::utility::vector::toValueType(x); std::vector const new_b = storm::utility::vector::toValueType(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(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); + result = __basicValueIteration_mvReduce_minimize(maxIters, precision, relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); } else { - result = __basicValueIteration_mvReduce_maximize(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations); + result = __basicValueIteration_mvReduce_maximize(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(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); + result = __basicValueIteration_mvReduce_minimize(maxIters, precision, relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); } else { - result = __basicValueIteration_mvReduce_maximize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); + result = __basicValueIteration_mvReduce_maximize(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(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(*currentX, *swap, static_cast(this->precision), this->relative); + converged = storm::utility::vector::equalModuloPrecision(*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 - ValueType TopologicalMinMaxLinearEquationSolver::getPrecision() const { - return this->precision; - } - - template - bool TopologicalMinMaxLinearEquationSolver::getRelative() const { - return this->relative; - } - template void TopologicalMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { std::unique_ptr> multiplyResult = std::make_unique>(this->A->getRowCount()); @@ -471,12 +469,13 @@ namespace storm { } template - TopologicalMinMaxLinearEquationSolverFactory::TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler) : MinMaxLinearEquationSolverFactory(MinMaxMethodSelection::Topological, trackScheduler) { + TopologicalMinMaxLinearEquationSolverFactory::TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler) { // Intentionally left empty. } template - std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create() const { + std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::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>(); } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h index 27e261961..8a07bba77 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h @@ -24,7 +24,7 @@ namespace storm { template class TopologicalMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { 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 const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); virtual void setMatrix(storm::storage::SparseMatrix const& matrix) override; virtual void setMatrix(storm::storage::SparseMatrix&& matrix) override; - virtual bool internalSolveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const override; + virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const override; virtual void repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const override; - ValueType getPrecision() const; - bool getRelative() const; - private: storm::storage::SparseMatrix const* A; std::unique_ptr> 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> create() const override; + virtual std::unique_ptr> create(Environment const& env) const override; }; } // namespace solver diff --git a/src/test/storm/solver/EigenLinearEquationSolverTest.cpp b/src/test/storm/solver/EigenLinearEquationSolverTest.cpp index 945c3349a..91a87d18c 100644 --- a/src/test/storm/solver/EigenLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/EigenLinearEquationSolverTest.cpp @@ -29,7 +29,7 @@ TEST(EigenLinearEquationSolver, SolveWithStandardOptions) { ASSERT_NO_THROW(storm::solver::EigenLinearEquationSolver solver(A)); storm::solver::EigenLinearEquationSolver 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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -58,7 +58,7 @@ TEST(EigenLinearEquationSolver, SparseLU) { solver.getSettings().setSolutionMethod(storm::solver::EigenLinearEquationSolverSettings::SolutionMethod::SparseLU); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -85,7 +85,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) { std::vector b = {16, -4, -7}; storm::solver::EigenLinearEquationSolver 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 b = {storm::RationalFunction(16), storm::RationalFunction(-4), storm::RationalFunction(-7)}; storm::solver::EigenLinearEquationSolver 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::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -174,7 +174,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Ilu) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -204,7 +204,7 @@ TEST(EigenLinearEquationSolver, DGMRES_Diagonal) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -236,7 +236,7 @@ TEST(EigenLinearEquationSolver, GMRES) { solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -266,7 +266,7 @@ TEST(EigenLinearEquationSolver, GMRES_Ilu) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -296,7 +296,7 @@ TEST(EigenLinearEquationSolver, GMRES_Diagonal) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -327,7 +327,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB) { solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -357,7 +357,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Ilu) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); @@ -387,7 +387,7 @@ TEST(EigenLinearEquationSolver, BiCGSTAB_Diagonal) { solver.getSettings().setPrecision(1e-6); solver.getSettings().setMaximalNumberOfIterations(10000); solver.getSettings().setPreconditioner(storm::solver::EigenLinearEquationSolverSettings::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().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule().getPrecision()); ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision());