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

Fixed an issue where scheduler generation in MDPs was not possible due to end components even if there actually were no end components.

tempestpy_adaptions
TimQu 6 years ago
parent
2b1ef118d3
commit
87fa9908bf
3 changed files with 7 additions and 6 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  2. 3
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  3. 2
      src/storm/solver/MinMaxLinearEquationSolver.h

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

@ -426,7 +426,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
SparseMdpHintType<ValueType> computeHints(Environment const& env, SolutionType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
SparseMdpHintType<ValueType> computeHints(Environment const& env, SolutionType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, bool produceScheduler, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
SparseMdpHintType<ValueType> result; SparseMdpHintType<ValueType> result;
// The solution to the min-max equation system is unique if we minimize until probabilities or // The solution to the min-max equation system is unique if we minimize until probabilities or
@ -438,7 +438,7 @@ namespace storm {
// Check for requirements of the solver. // Check for requirements of the solver.
bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint(); bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint();
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory; storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, hasSchedulerHint);
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, hasSchedulerHint, produceScheduler);
if (requirements.hasEnabledRequirement()) { if (requirements.hasEnabledRequirement()) {
// If the solver still requires no end-components, we have to eliminate them later. // If the solver still requires no end-components, we have to eliminate them later.
if (requirements.noEndComponents()) { if (requirements.noEndComponents()) {
@ -737,7 +737,7 @@ namespace storm {
// In this case we have have to compute the remaining probabilities. // In this case we have have to compute the remaining probabilities.
// Obtain proper hint information either from the provided hint or from requirements of the solver. // Obtain proper hint information either from the provided hint or from requirements of the solver.
SparseMdpHintType<ValueType> hintInformation = computeHints(env, SolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1);
SparseMdpHintType<ValueType> hintInformation = computeHints(env, SolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, produceScheduler);
// Declare the components of the equation system we will solve. // Declare the components of the equation system we will solve.
storm::storage::SparseMatrix<ValueType> submatrix; storm::storage::SparseMatrix<ValueType> submatrix;
@ -1222,7 +1222,7 @@ namespace storm {
} }
// Obtain proper hint information either from the provided hint or from requirements of the solver. // Obtain proper hint information either from the provided hint or from requirements of the solver.
SparseMdpHintType<ValueType> hintInformation = computeHints(env, SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, selectedChoices);
SparseMdpHintType<ValueType> hintInformation = computeHints(env, SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, produceScheduler, selectedChoices);
// Declare the components of the equation system we will solve. // Declare the components of the equation system we will solve.
storm::storage::SparseMatrix<ValueType> submatrix; storm::storage::SparseMatrix<ValueType> submatrix;

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

@ -161,9 +161,10 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& hasInitialScheduler) const {
MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction, bool hasInitialScheduler, bool trackScheduler) const {
// Create dummy solver and ask it for requirements. // Create dummy solver and ask it for requirements.
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->create(env); std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->create(env);
solver->setTrackScheduler(trackScheduler);
solver->setHasUniqueSolution(hasUniqueSolution); solver->setHasUniqueSolution(hasUniqueSolution);
return solver->getRequirements(env, direction, hasInitialScheduler); return solver->getRequirements(env, direction, hasInitialScheduler);
} }

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

@ -194,7 +194,7 @@ namespace storm {
* Retrieves the requirements of the solver that would be created when calling create() right now. The * Retrieves the requirements of the solver that would be created when calling create() right now. The
* requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type. * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type.
*/ */
MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool const& hasInitialScheduler = false) const;
MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool hasInitialScheduler = false, bool trackScheduler = false) const;
void setRequirementsChecked(bool value = true); void setRequirementsChecked(bool value = true);
bool isRequirementsCheckedSet() const; bool isRequirementsCheckedSet() const;

Write Preview
Loading…
Cancel
Save