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

MaPcaaWeightVectorChecker now uses the acyclic solver if possible.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
5e9241fcd1
commit
5a6952899b
2 changed files with 41 additions and 22 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. 55
      src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
  2. 8
      src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h

55
src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
View File

@ -10,7 +10,8 @@
#include "storm/logic/Formulas.h"
#include "storm/solver/SolverSelectionOptions.h"
#include "storm/environment/solver/NativeSolverEnvironment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/InvalidPropertyException.h"
@ -84,7 +85,7 @@ namespace storm {
// Split the preprocessed model into transitions from/to probabilistic/Markovian states.
SubModel MS = createSubModel(true, weightedRewardVector);
SubModel PS = createSubModel(false, weightedRewardVector);
// Apply digitization to Markovian transitions
ValueType digitizationConstant = getDigitizationConstant(weightVector);
digitize(MS, digitizationConstant);
@ -93,13 +94,16 @@ namespace storm {
TimeBoundMap upperTimeBounds;
digitizeTimeBounds(upperTimeBounds, digitizationConstant);
// Check whether there is a cycle in of probabilistic states
bool acyclic = storm::utility::graph::hasCycle(PS.toPS);
// Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch
// No EC elimination is necessary as we assume non-zenoness
std::unique_ptr<MinMaxSolverData> minMax = initMinMaxSolver(env, PS, weightVector);
std::unique_ptr<MinMaxSolverData> minMax = initMinMaxSolver(env, PS, acyclic, weightVector);
// create a linear equation solver for the model induced by the optimal choice vector.
// the solver will be updated whenever the optimal choice vector has changed.
std::unique_ptr<LinEqSolverData> linEq = initLinEqSolver(env, PS);
std::unique_ptr<LinEqSolverData> linEq = initLinEqSolver(env, PS, acyclic);
// Store the optimal choices of PS as computed by the minMax solver.
std::vector<uint_fast64_t> optimalChoicesAtCurrentEpoch(PS.getNumberOfStates(), std::numeric_limits<uint_fast64_t>::max());
@ -316,15 +320,21 @@ namespace storm {
}
template <class SparseMaModelType>
std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<SparseMaModelType>::MinMaxSolverData> StandardMaPcaaWeightVectorChecker<SparseMaModelType>::initMinMaxSolver(Environment const& env, SubModel const& PS, std::vector<ValueType> const& weightVector) const {
std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<SparseMaModelType>::MinMaxSolverData> StandardMaPcaaWeightVectorChecker<SparseMaModelType>::initMinMaxSolver(Environment const& env, SubModel const& PS, bool acyclic, std::vector<ValueType> const& weightVector) const {
std::unique_ptr<MinMaxSolverData> result(new MinMaxSolverData());
result->env = std::make_unique<storm::Environment>(env);
// For acyclic models we switch to the more efficient acyclic solver (Unless the solver / method was explicitly specified)
if (acyclic && result->env->solver().minMax().isMethodSetFromDefault() && result->env->solver().minMax().getMethod() != storm::solver::MinMaxMethod::Acyclic) {
STORM_LOG_INFO("Switching to Acyclic linear equation solver method. To overwrite this, explicitly specify another solver.");
result->env->solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic);
}
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
result->solver = minMaxSolverFactory.create(env, PS.toPS);
result->solver = minMaxSolverFactory.create(*result->env, PS.toPS);
result->solver->setHasUniqueSolution(true);
result->solver->setHasNoEndComponents(true); // Non-zeno MA
result->solver->setTrackScheduler(true);
result->solver->setCachingEnabled(true);
auto req = result->solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, false);
auto req = result->solver->getRequirements(*result->env, storm::solver::OptimizationDirection::Maximize, false);
boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true));
if (lowerBound) {
result->solver->setLowerBound(lowerBound.get());
@ -335,6 +345,9 @@ namespace storm {
result->solver->setUpperBound(upperBound.get());
req.clearUpperBounds();
}
if (acyclic) {
req.clearAcyclic();
}
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
result->solver->setRequirementsChecked(true);
result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
@ -346,15 +359,14 @@ namespace storm {
template <class SparseMaModelType>
template <typename VT, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type>
std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<SparseMaModelType>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<SparseMaModelType>::initLinEqSolver(Environment const& env, SubModel const& PS) const {
std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<SparseMaModelType>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<SparseMaModelType>::initLinEqSolver(Environment const& env, SubModel const& PS, bool acyclic) const {
std::unique_ptr<LinEqSolverData> result(new LinEqSolverData());
result->env = std::make_unique<Environment>();
// Unless the solver / method was explicitly specified, we switch it to Native / Power.
// We choose the Power method since we call the solver very frequently on 'easy' inputs and power has little overhead).
if ((result->env->solver().isLinearEquationSolverTypeSetFromDefaultValue() || result->env->solver().getLinearEquationSolverType() == storm::solver::EquationSolverType::Native) && (result->env->solver().native().isMethodSetFromDefault() || result->env->solver().native().getMethod() == storm::solver::NativeLinearEquationSolverMethod::Power)) {
STORM_LOG_INFO("Switching to Native/Power linear equation solver method. To overwrite this, explicitly specify another method.");
result->env->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
result->env->solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
result->env = std::make_unique<Environment>(env);
result->acyclic = acyclic;
// For acyclic models we switch to the more efficient acyclic solver (Unless the solver / method was explicitly specified)
if (acyclic && result->env->solver().isLinearEquationSolverTypeSetFromDefaultValue() && result->env->solver().getLinearEquationSolverType() != storm::solver::EquationSolverType::Acyclic) {
STORM_LOG_INFO("Switching to Acyclic linear equation solver method. To overwrite this, explicitly specify another solver.");
result->env->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Acyclic);
}
result->factory = std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<ValueType>>();
result->b.resize(PS.getNumberOfStates());
@ -363,7 +375,7 @@ namespace storm {
template <class SparseMaModelType>
template <typename VT, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type>
std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<SparseMaModelType>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<SparseMaModelType>::initLinEqSolver(Environment const& env, SubModel const& PS) const {
std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<SparseMaModelType>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<SparseMaModelType>::initLinEqSolver(Environment const& env, SubModel const& PS, bool acyclic) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type.");
}
@ -389,7 +401,7 @@ namespace storm {
template <class SparseMaModelType>
void StandardMaPcaaWeightVectorChecker<SparseMaModelType>::performPSStep(Environment const& env, SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector<uint_fast64_t>& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives, std::vector<ValueType> const& weightVector) const {
// compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector
minMax.solver->solveEquations(env, PS.weightedSolutionVector, minMax.b);
minMax.solver->solveEquations(*minMax.env, PS.weightedSolutionVector, minMax.b);
auto const& newChoices = minMax.solver->getSchedulerChoices();
if (consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) {
// In this case there is no need to perform the computation on the individual objectives
@ -410,6 +422,11 @@ namespace storm {
}
linEq.solver = linEq.factory->create(*linEq.env, std::move(linEqMatrix));
linEq.solver->setCachingEnabled(true);
auto req = linEq.solver->getRequirements(*linEq.env);
if (linEq.acyclic) {
req.clearAcyclic();
}
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
}
// Get the results for the individual objectives.
@ -463,13 +480,13 @@ namespace storm {
template double StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::getDigitizationConstant<double>(std::vector<double> const& direction) const;
template void StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::digitize<double>(StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::SubModel& subModel, double const& digitizationConstant) const;
template void StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::digitizeTimeBounds<double>( StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant);
template std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::initLinEqSolver<double>(Environment const& env, StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::SubModel const& PS ) const;
template std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::initLinEqSolver<double>(Environment const& env, StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::SubModel const& PS, bool acyclic) const;
#ifdef STORM_HAVE_CARL
template class StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
template storm::RationalNumber StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::getDigitizationConstant<storm::RationalNumber>(std::vector<storm::RationalNumber> const& direction) const;
template void StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::digitize<storm::RationalNumber>(StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const;
template void StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::digitizeTimeBounds<storm::RationalNumber>(StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant);
template std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::initLinEqSolver<storm::RationalNumber>(Environment const& env, StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::SubModel const& PS ) const;
template std::unique_ptr<typename StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::LinEqSolverData> StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::initLinEqSolver<storm::RationalNumber>(Environment const& env, StandardMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::SubModel const& PS, bool acyclic) const;
#endif
}

8
src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.h
View File

@ -66,12 +66,14 @@ namespace storm {
* Stores the data that is relevant to invoke the minMaxSolver and retrieve the result.
*/
struct MinMaxSolverData {
std::unique_ptr<Environment> env;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver;
std::vector<ValueType> b;
};
struct LinEqSolverData {
std::unique_ptr<Environment> env;
bool acyclic;
std::unique_ptr<storm::solver::LinearEquationSolverFactory<ValueType>> factory;
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver;
std::vector<ValueType> b;
@ -120,15 +122,15 @@ namespace storm {
/*!
* Initializes the data for the MinMax solver
*/
std::unique_ptr<MinMaxSolverData> initMinMaxSolver(Environment const& env, SubModel const& PS, std::vector<ValueType> const& weightVector) const;
std::unique_ptr<MinMaxSolverData> initMinMaxSolver(Environment const& env, SubModel const& PS, bool acyclic, std::vector<ValueType> const& weightVector) const;
/*!
* Initializes the data for the LinEq solver
*/
template <typename VT = ValueType, typename std::enable_if<storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
std::unique_ptr<LinEqSolverData> initLinEqSolver(Environment const& env, SubModel const& PS) const;
std::unique_ptr<LinEqSolverData> initLinEqSolver(Environment const& env, SubModel const& PS, bool acyclic) const;
template <typename VT = ValueType, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type = 0>
std::unique_ptr<LinEqSolverData> initLinEqSolver(Environment const& env, SubModel const& PS) const;
std::unique_ptr<LinEqSolverData> initLinEqSolver(Environment const& env, SubModel const& PS, bool acyclic) const;
/*
* Updates the reward vectors within the split model,

Write Preview
Loading…
Cancel
Save