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

allowed for more fine grained solver requirements

tempestpy_adaptions
TimQu 7 years ago
parent
9559a96fd7
commit
3310f51857
19 changed files with 299 additions and 140 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. 6
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
  2. 6
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  3. 8
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  4. 4
      src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
  5. 2
      src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
  6. 9
      src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
  7. 6
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  8. 34
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  9. 6
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  10. 16
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  11. 16
      src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  12. 64
      src/storm/solver/LinearEquationSolverRequirements.cpp
  13. 29
      src/storm/solver/LinearEquationSolverRequirements.h
  14. 103
      src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
  15. 41
      src/storm/solver/MinMaxLinearEquationSolverRequirements.h
  16. 32
      src/storm/solver/SolverRequirement.cpp
  17. 39
      src/storm/solver/SolverRequirement.h
  18. 16
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
  19. 2
      src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp

6
src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
View File

@ -152,7 +152,7 @@ namespace storm {
// The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
auto req = solverFactory->getRequirements(env, true, boost::none, true); auto req = solverFactory->getRequirements(env, true, boost::none, true);
req.clearBounds(); req.clearBounds();
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
solverFactory->setRequirementsChecked(true); solverFactory->setRequirementsChecked(true);
} }
@ -191,11 +191,11 @@ namespace storm {
// The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
auto req = solverFactory->getRequirements(env, true, boost::none, true); auto req = solverFactory->getRequirements(env, true, boost::none, true);
req.clearLowerBounds(); req.clearLowerBounds();
if (req.requiresUpperBounds()) {
if (req.upperBounds()) {
solvingRequiresUpperRewardBounds = true; solvingRequiresUpperRewardBounds = true;
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
solverFactory->setRequirementsChecked(true); solverFactory->setRequirementsChecked(true);

6
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -492,7 +492,8 @@ namespace storm {
{ {
// Check solver requirements // Check solver requirements
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory; storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
STORM_LOG_THROW(linearEquationSolverFactory.getRequirements(env).empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched.");
auto requirements = linearEquationSolverFactory.getRequirements(env);
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
// Check whether we have the right input format for the solver. // Check whether we have the right input format for the solver.
STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format."); STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format.");
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(bsccEquationSystem)); std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(bsccEquationSystem));
@ -565,7 +566,8 @@ namespace storm {
{ {
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory; storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
// Check solver requirements // Check solver requirements
STORM_LOG_THROW(linearEquationSolverFactory.getRequirements(env).empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched.");
auto requirements = linearEquationSolverFactory.getRequirements(env);
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
// Check whether we have the right input format for the solver. // Check whether we have the right input format for the solver.
STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format."); STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format.");
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(rewardEquationSystemMatrix)); std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(rewardEquationSystemMatrix));

8
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -287,7 +287,7 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory; storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir);
requirements.clearBounds(); requirements.clearBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
if (numberOfProbabilisticChoices > 0) { if (numberOfProbabilisticChoices > 0) {
solver = minMaxLinearEquationSolverFactory.create(env, probMatrix); solver = minMaxLinearEquationSolverFactory.create(env, probMatrix);
@ -449,7 +449,7 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory; storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir);
requirements.clearBounds(); requirements.clearBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(env, aProbabilistic); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(env, aProbabilistic);
solver->setHasUniqueSolution(); solver->setHasUniqueSolution();
@ -757,7 +757,7 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory; storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir);
requirements.clearBounds(); requirements.clearBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(env, sspMatrix); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(env, sspMatrix);
solver->setHasUniqueSolution(); solver->setHasUniqueSolution();
@ -971,7 +971,7 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory; storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir);
requirements.clearLowerBounds(); requirements.clearLowerBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
auto solver = minMaxLinearEquationSolverFactory.create(env, std::move(aProbabilistic)); auto solver = minMaxLinearEquationSolverFactory.create(env, std::move(aProbabilistic));
solver->setLowerBound(storm::utility::zero<ValueType>()); solver->setLowerBound(storm::utility::zero<ValueType>());

4
src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
View File

@ -295,7 +295,7 @@ namespace storm {
cachedData.linEqSolver->setUpperBound(*obj.upperResultBound); cachedData.linEqSolver->setUpperBound(*obj.upperResultBound);
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
cachedData.linEqSolver->solveEquations(env, x, cachedData.bLinEq); cachedData.linEqSolver->solveEquations(env, x, cachedData.bLinEq);
auto resultIt = result.begin(); auto resultIt = result.begin();
for (auto const& state : epochModel.epochInStates) { for (auto const& state : epochModel.epochInStates) {
@ -331,7 +331,7 @@ namespace storm {
cachedData.minMaxSolver->setUpperBound(upperBound.get()); cachedData.minMaxSolver->setUpperBound(upperBound.get());
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
cachedData.minMaxSolver->setRequirementsChecked(true); cachedData.minMaxSolver->setRequirementsChecked(true);
cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);

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

@ -314,7 +314,7 @@ namespace storm {
result->solver->setUpperBound(upperBound.get()); result->solver->setUpperBound(upperBound.get());
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
result->solver->setRequirementsChecked(true); result->solver->setRequirementsChecked(true);
result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);

9
src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
View File

@ -180,14 +180,14 @@ namespace storm {
solver->setHasUniqueSolution(true); solver->setHasUniqueSolution(true);
solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize); auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize);
setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues);
setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues);
if (solver->hasLowerBound()) { if (solver->hasLowerBound()) {
req.clearLowerBounds(); req.clearLowerBounds();
} }
if (solver->hasUpperBound()) { if (solver->hasUpperBound()) {
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
solver->setRequirementsChecked(true); solver->setRequirementsChecked(true);
// Use the (0...0) vector as initial guess for the solution. // Use the (0...0) vector as initial guess for the solution.
@ -266,15 +266,14 @@ namespace storm {
solver->clearBounds(); solver->clearBounds();
storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates; storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates;
submatrixRowsWithSumLessOne.complement(); submatrixRowsWithSumLessOne.complement();
this->setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b);
this->setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b);
if (solver->hasLowerBound()) { if (solver->hasLowerBound()) {
req.clearLowerBounds(); req.clearLowerBounds();
} }
if (solver->hasUpperBound()) { if (solver->hasUpperBound()) {
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
solver->solveEquations(env, x, b); solver->solveEquations(env, x, b);
// Set the result for this objective accordingly // Set the result for this objective accordingly
storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], maybeStates, x); storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], maybeStates, x);

6
src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
View File

@ -72,7 +72,7 @@ namespace storm {
auto req = linearEquationSolverFactory.getRequirements(env); auto req = linearEquationSolverFactory.getRequirements(env);
req.clearLowerBounds(); req.clearLowerBounds();
req.clearUpperBounds(); req.clearUpperBounds();
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
// Check whether we need to create an equation system. // Check whether we need to create an equation system.
bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
@ -285,14 +285,14 @@ namespace storm {
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory; storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
auto req = linearEquationSolverFactory.getRequirements(env); auto req = linearEquationSolverFactory.getRequirements(env);
req.clearLowerBounds(); req.clearLowerBounds();
if (req.requiresUpperBounds()) {
if (req.upperBounds()) {
storm::dd::Add<DdType, ValueType> targetStatesAsColumn = targetStates.template toAdd<ValueType>(); storm::dd::Add<DdType, ValueType> targetStatesAsColumn = targetStates.template toAdd<ValueType>();
targetStatesAsColumn = targetStatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); targetStatesAsColumn = targetStatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs());
oneStepTargetProbs = submatrix * targetStatesAsColumn; oneStepTargetProbs = submatrix * targetStatesAsColumn;
oneStepTargetProbs = oneStepTargetProbs->sumAbstract(model.getColumnVariables()); oneStepTargetProbs = oneStepTargetProbs->sumAbstract(model.getColumnVariables());
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
// Check whether we need to create an equation system. // Check whether we need to create an equation system.
bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;

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

@ -155,18 +155,18 @@ namespace storm {
SolverRequirementsData<ValueType> solverRequirementsData; SolverRequirementsData<ValueType> solverRequirementsData;
bool extendMaybeStates = false; bool extendMaybeStates = false;
if (!clearedRequirements.empty()) {
if (clearedRequirements.requiresNoEndComponents()) {
if (clearedRequirements.hasEnabledRequirement()) {
if (clearedRequirements.noEndComponents()) {
STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
extendMaybeStates = true; extendMaybeStates = true;
clearedRequirements.clearNoEndComponents(); clearedRequirements.clearNoEndComponents();
} }
if (clearedRequirements.requiresValidInitialScheduler()) {
if (clearedRequirements.validInitialScheduler()) {
STORM_LOG_DEBUG("Scheduling valid scheduler computation, because the solver requires it."); STORM_LOG_DEBUG("Scheduling valid scheduler computation, because the solver requires it.");
clearedRequirements.clearValidInitialScheduler(); clearedRequirements.clearValidInitialScheduler();
} }
clearedRequirements.clearBounds(); clearedRequirements.clearBounds();
STORM_LOG_THROW(clearedRequirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
STORM_LOG_THROW(!clearedRequirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + clearedRequirements.getEnabledRequirementsAsString() + " not checked.");
} }
storm::dd::Bdd<DdType> extendedMaybeStates = maybeStates; storm::dd::Bdd<DdType> extendedMaybeStates = maybeStates;
@ -228,7 +228,7 @@ namespace storm {
explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd); explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd);
conversionWatch.stop(); conversionWatch.stop();
if (requirements.requiresValidInitialScheduler()) {
if (requirements.validInitialScheduler()) {
solverRequirementsData.initialScheduler = computeValidInitialSchedulerForUntilProbabilities<ValueType>(explicitRepresentation.first, explicitRepresentation.second); solverRequirementsData.initialScheduler = computeValidInitialSchedulerForUntilProbabilities<ValueType>(explicitRepresentation.first, explicitRepresentation.second);
} }
} }
@ -251,7 +251,7 @@ namespace storm {
solver->solveEquations(env, dir, x, explicitRepresentation.second); solver->solveEquations(env, dir, x, explicitRepresentation.second);
// If we included some target and non-filter states in the ODD, we need to expand the result from the solver. // If we included some target and non-filter states in the ODD, we need to expand the result from the solver.
if (requirements.requiresNoEndComponents() && solverRequirementsData.ecInformation) {
if (requirements.noEndComponents() && solverRequirementsData.ecInformation) {
std::vector<ValueType> extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits()); std::vector<ValueType> extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits());
solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x); solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x);
x = std::move(extendedVector); x = std::move(extendedVector);
@ -549,24 +549,24 @@ namespace storm {
storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir);
storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements;
bool extendMaybeStates = false; bool extendMaybeStates = false;
if (!clearedRequirements.empty()) {
if (clearedRequirements.requiresNoEndComponents()) {
if (clearedRequirements.hasEnabledRequirement()) {
if (clearedRequirements.noEndComponents()) {
STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
extendMaybeStates = true; extendMaybeStates = true;
clearedRequirements.clearNoEndComponents(); clearedRequirements.clearNoEndComponents();
} }
if (clearedRequirements.requiresValidInitialScheduler()) {
if (clearedRequirements.validInitialScheduler()) {
STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
extendMaybeStates = true; extendMaybeStates = true;
clearedRequirements.clearValidInitialScheduler(); clearedRequirements.clearValidInitialScheduler();
} }
clearedRequirements.clearLowerBounds(); clearedRequirements.clearLowerBounds();
if (clearedRequirements.requiresUpperBounds()) {
if (clearedRequirements.upperBounds()) {
STORM_LOG_DEBUG("Computing upper bounds, because the solver requires it."); STORM_LOG_DEBUG("Computing upper bounds, because the solver requires it.");
extendMaybeStates = true; extendMaybeStates = true;
clearedRequirements.clearUpperBounds(); clearedRequirements.clearUpperBounds();
} }
STORM_LOG_THROW(clearedRequirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
STORM_LOG_THROW(!clearedRequirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + clearedRequirements.getEnabledRequirementsAsString() + " not checked.");
} }
// Compute the set of maybe states that we are required to keep in the translation to explicit. // Compute the set of maybe states that we are required to keep in the translation to explicit.
@ -611,17 +611,17 @@ namespace storm {
storm::storage::BitVector targetStates = computeTargetStatesForReachabilityRewardsFromExplicitRepresentation(explicitRepresentation.first); storm::storage::BitVector targetStates = computeTargetStatesForReachabilityRewardsFromExplicitRepresentation(explicitRepresentation.first);
solverRequirementsData.properMaybeStates = ~targetStates; solverRequirementsData.properMaybeStates = ~targetStates;
if (requirements.requiresNoEndComponents()) {
eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.requiresUpperBounds());
if (requirements.noEndComponents()) {
eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.upperBounds());
// The solution becomes unique after end components have been eliminated. // The solution becomes unique after end components have been eliminated.
uniqueSolution = true; uniqueSolution = true;
} else { } else {
if (requirements.requiresValidInitialScheduler()) {
if (requirements.validInitialScheduler()) {
// Compute a valid initial scheduler. // Compute a valid initial scheduler.
solverRequirementsData.initialScheduler = computeValidInitialSchedulerForReachabilityRewards<ValueType>(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates); solverRequirementsData.initialScheduler = computeValidInitialSchedulerForReachabilityRewards<ValueType>(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates);
} }
if (requirements.requiresUpperBounds()) {
if (requirements.upperBounds()) {
solverRequirementsData.oneStepTargetProbabilities = computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates); solverRequirementsData.oneStepTargetProbabilities = computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates);
} }
@ -641,7 +641,7 @@ namespace storm {
solver->setHasUniqueSolution(uniqueSolution); solver->setHasUniqueSolution(uniqueSolution);
// If the solver requires upper bounds, compute them now. // If the solver requires upper bounds, compute them now.
if (requirements.requiresUpperBounds()) {
if (requirements.upperBounds()) {
setUpperRewardBounds(*solver, dir, explicitRepresentation.first, explicitRepresentation.second, solverRequirementsData.oneStepTargetProbabilities.get()); setUpperRewardBounds(*solver, dir, explicitRepresentation.first, explicitRepresentation.second, solverRequirementsData.oneStepTargetProbabilities.get());
} }
@ -657,7 +657,7 @@ namespace storm {
solver->solveEquations(env, dir, x, explicitRepresentation.second); solver->solveEquations(env, dir, x, explicitRepresentation.second);
// If we eliminated end components, we need to extend the solution vector. // If we eliminated end components, we need to extend the solution vector.
if (requirements.requiresNoEndComponents() && solverRequirementsData.ecInformation) {
if (requirements.noEndComponents() && solverRequirementsData.ecInformation) {
std::vector<ValueType> extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits()); std::vector<ValueType> extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits());
solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x); solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x);
x = std::move(extendedVector); x = std::move(extendedVector);

6
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -128,7 +128,7 @@ namespace storm {
linEqSolver->setUpperBound(upperBound.get()); linEqSolver->setUpperBound(upperBound.get());
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
} }
// Prepare the right hand side of the equation system // Prepare the right hand side of the equation system
@ -487,11 +487,11 @@ namespace storm {
storm::solver::LinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env); storm::solver::LinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env);
boost::optional<std::vector<ValueType>> upperRewardBounds; boost::optional<std::vector<ValueType>> upperRewardBounds;
requirements.clearLowerBounds(); requirements.clearLowerBounds();
if (requirements.requiresUpperBounds()) {
if (requirements.upperBounds()) {
upperRewardBounds = computeUpperRewardBounds(submatrix, b, transitionMatrix.getConstrainedRowSumVector(maybeStates, rew0States)); upperRewardBounds = computeUpperRewardBounds(submatrix, b, transitionMatrix.getConstrainedRowSumVector(maybeStates, rew0States));
requirements.clearUpperBounds(); requirements.clearUpperBounds();
} }
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
// If necessary, convert the matrix from the fixpoint notation to the form needed for the equation system. // If necessary, convert the matrix from the fixpoint notation to the form needed for the equation system.
if (convertToEquationSystem) { if (convertToEquationSystem) {

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

@ -158,7 +158,7 @@ namespace storm {
minMaxSolver->setUpperBound(upperBound.get()); minMaxSolver->setUpperBound(upperBound.get());
req.clearUpperBounds(); req.clearUpperBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
minMaxSolver->setRequirementsChecked(); minMaxSolver->setRequirementsChecked();
} else { } else {
auto choicesTmp = minMaxSolver->getSchedulerChoices(); auto choicesTmp = minMaxSolver->getSchedulerChoices();
@ -437,10 +437,9 @@ namespace storm {
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);
if (!requirements.empty()) {
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.requiresNoEndComponents()) {
if (requirements.noEndComponents()) {
STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique."); STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
result.eliminateEndComponents = true; result.eliminateEndComponents = true;
@ -450,7 +449,7 @@ namespace storm {
} }
// If the solver requires an initial scheduler, compute one now. // If the solver requires an initial scheduler, compute one now.
if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
if (requirements.validInitialScheduler()) {
STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
result.schedulerHint = computeValidSchedulerHint(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates); result.schedulerHint = computeValidSchedulerHint(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates);
requirements.clearValidInitialScheduler(); requirements.clearValidInitialScheduler();
@ -462,11 +461,11 @@ namespace storm {
} else if (type == SolutionType::ExpectedRewards) { } else if (type == SolutionType::ExpectedRewards) {
requirements.clearLowerBounds(); requirements.clearLowerBounds();
} }
if (requirements.requiresUpperBounds()) {
if (requirements.upperBounds()) {
result.computeUpperBounds = true; result.computeUpperBounds = true;
requirements.clearUpperBounds(); requirements.clearUpperBounds();
} }
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
} else { } else {
STORM_LOG_DEBUG("Solver has no requirements."); STORM_LOG_DEBUG("Solver has no requirements.");
} }
@ -1343,7 +1342,8 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory; storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, goal.direction()); storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, goal.direction());
requirements.clearBounds(); requirements.clearBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
std::vector<ValueType> sspResult(numberOfSspStates); std::vector<ValueType> sspResult(numberOfSspStates);
goal.restrictRelevantValues(statesNotContainedInAnyMec); goal.restrictRelevantValues(statesNotContainedInAnyMec);

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

@ -75,20 +75,20 @@ namespace storm {
// Check requirements of solver. // Check requirements of solver.
storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir); storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir);
boost::optional<storm::dd::Bdd<DdType>> initialScheduler; boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
if (!requirements.empty()) {
if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
if (requirements.hasEnabledRequirement()) {
if (requirements.validInitialScheduler()) {
STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
initialScheduler = computeValidSchedulerHint(EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability1); initialScheduler = computeValidSchedulerHint(EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability1);
requirements.clearValidInitialScheduler(); requirements.clearValidInitialScheduler();
} }
requirements.clearBounds(); requirements.clearBounds();
if (requirements.requiresNoEndComponents()) {
if (requirements.noEndComponents()) {
// Check whether there are end components // Check whether there are end components
if (storm::utility::graph::performProb0E(model, transitionMatrix.notZero(), maybeStates, !maybeStates && model.getReachableStates()).isZero()) { if (storm::utility::graph::performProb0E(model, transitionMatrix.notZero(), maybeStates, !maybeStates && model.getReachableStates()).isZero()) {
requirements.clearNoEndComponents(); requirements.clearNoEndComponents();
} }
} }
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
} }
if (initialScheduler) { if (initialScheduler) {
solver->setInitialScheduler(initialScheduler.get()); solver->setInitialScheduler(initialScheduler.get());
@ -246,20 +246,20 @@ namespace storm {
// Check requirements of solver. // Check requirements of solver.
storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir); storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir);
boost::optional<storm::dd::Bdd<DdType>> initialScheduler; boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
if (!requirements.empty()) {
if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
if (requirements.hasEnabledRequirement()) {
if (requirements.validInitialScheduler()) {
STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
initialScheduler = computeValidSchedulerHint(EquationSystemType::ExpectedRewards, model, transitionMatrix, maybeStates, targetStates); initialScheduler = computeValidSchedulerHint(EquationSystemType::ExpectedRewards, model, transitionMatrix, maybeStates, targetStates);
requirements.clearValidInitialScheduler(); requirements.clearValidInitialScheduler();
} }
requirements.clearLowerBounds(); requirements.clearLowerBounds();
if (requirements.requiresNoEndComponents()) {
if (requirements.noEndComponents()) {
// Check whether there are end components // Check whether there are end components
if (storm::utility::graph::performProb0E(model, transitionMatrixBdd, maybeStates, !maybeStates && model.getReachableStates()).isZero()) { if (storm::utility::graph::performProb0E(model, transitionMatrixBdd, maybeStates, !maybeStates && model.getReachableStates()).isZero()) {
requirements.clearNoEndComponents(); requirements.clearNoEndComponents();
} }
} }
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver.");
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
} }
if (initialScheduler) { if (initialScheduler) {
solver->setInitialScheduler(initialScheduler.get()); solver->setInitialScheduler(initialScheduler.get());

64
src/storm/solver/LinearEquationSolverRequirements.cpp
View File

@ -3,52 +3,78 @@
namespace storm { namespace storm {
namespace solver { namespace solver {
LinearEquationSolverRequirements::LinearEquationSolverRequirements() : lowerBounds(false), upperBounds(false) {
LinearEquationSolverRequirements::LinearEquationSolverRequirements() {
// Intentionally left empty. // Intentionally left empty.
} }
LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireLowerBounds() {
lowerBounds = true;
LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireLowerBounds(bool critical) {
lowerBoundsRequirement.enable(critical);
return *this; return *this;
} }
LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireUpperBounds() {
upperBounds = true;
LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireUpperBounds(bool critical) {
upperBoundsRequirement.enable(critical);
return *this; return *this;
} }
LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireBounds() {
requireLowerBounds();
requireUpperBounds();
LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireBounds(bool critical) {
requireLowerBounds(critical);
requireUpperBounds(critical);
return *this; return *this;
} }
bool LinearEquationSolverRequirements::requiresLowerBounds() const {
return lowerBounds;
SolverRequirement const& LinearEquationSolverRequirements::lowerBounds() const {
return lowerBoundsRequirement;
} }
bool LinearEquationSolverRequirements::requiresUpperBounds() const {
return upperBounds;
SolverRequirement const& LinearEquationSolverRequirements::upperBounds() const {
return upperBoundsRequirement;
} }
bool LinearEquationSolverRequirements::requires(Element const& element) const {
SolverRequirement const& LinearEquationSolverRequirements::get(Element const& element) const {
switch (element) { switch (element) {
case Element::LowerBounds: return lowerBounds; break;
case Element::UpperBounds: return upperBounds; break;
case Element::LowerBounds: return lowerBounds(); break;
case Element::UpperBounds: return upperBounds(); break;
} }
} }
void LinearEquationSolverRequirements::clearLowerBounds() { void LinearEquationSolverRequirements::clearLowerBounds() {
lowerBounds = false;
lowerBoundsRequirement.clear();
} }
void LinearEquationSolverRequirements::clearUpperBounds() { void LinearEquationSolverRequirements::clearUpperBounds() {
upperBounds = false;
upperBoundsRequirement.clear();
} }
bool LinearEquationSolverRequirements::empty() const {
return !lowerBounds && !upperBounds;
bool LinearEquationSolverRequirements::hasEnabledRequirement() const {
return lowerBoundsRequirement || upperBoundsRequirement;
} }
bool LinearEquationSolverRequirements::hasEnabledCriticalRequirement() const {
return lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical();
}
std::string LinearEquationSolverRequirements::getEnabledRequirementsAsString() const {
std::string res = "[";
bool first = true;
if (lowerBounds()) {
if (!first) { res += ", "; } else {first = false;}
res += "lowerBounds";
if (lowerBounds().isCritical()) {
res += "(mandatory)";
}
}
if (upperBounds()) {
if (!first) { res += ", "; } else {first = false;}
res += "upperBounds";
if (upperBounds().isCritical()) {
res += "(mandatory)";
}
}
res += "]";
return res;
}
} }
} }

29
src/storm/solver/LinearEquationSolverRequirements.h
View File

@ -1,5 +1,9 @@
#pragma once #pragma once
#include <string>
#include "storm/solver/SolverRequirement.h"
namespace storm { namespace storm {
namespace solver { namespace solver {
@ -14,22 +18,29 @@ namespace storm {
LinearEquationSolverRequirements(); LinearEquationSolverRequirements();
LinearEquationSolverRequirements& requireLowerBounds();
LinearEquationSolverRequirements& requireUpperBounds();
LinearEquationSolverRequirements& requireBounds();
LinearEquationSolverRequirements& requireLowerBounds(bool critical = true);
LinearEquationSolverRequirements& requireUpperBounds(bool critical = true);
LinearEquationSolverRequirements& requireBounds(bool critical = true);
bool requiresLowerBounds() const;
bool requiresUpperBounds() const;
bool requires(Element const& element) const;
SolverRequirement const& lowerBounds() const;
SolverRequirement const& upperBounds() const;
SolverRequirement const& get(Element const& element) const;
void clearLowerBounds(); void clearLowerBounds();
void clearUpperBounds(); void clearUpperBounds();
bool empty() const;
bool hasEnabledRequirement() const;
bool hasEnabledCriticalRequirement() const;
/*!
* Checks whether there are no critical requirements left.
* In case there is a critical requirement left an exception is thrown.
*/
std::string getEnabledRequirementsAsString() const;
private: private:
bool lowerBounds;
bool upperBounds;
SolverRequirement lowerBoundsRequirement;
SolverRequirement upperBoundsRequirement;
}; };
} }

103
src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
View File

@ -3,76 +3,76 @@
namespace storm { namespace storm {
namespace solver { namespace solver {
MinMaxLinearEquationSolverRequirements::MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements) : noEndComponents(false), validInitialScheduler(false), lowerBounds(linearEquationSolverRequirements.requiresLowerBounds()), upperBounds(linearEquationSolverRequirements.requiresUpperBounds()) {
MinMaxLinearEquationSolverRequirements::MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements) : lowerBoundsRequirement(linearEquationSolverRequirements.lowerBounds()), upperBoundsRequirement(linearEquationSolverRequirements.upperBounds()) {
// Intentionally left empty. // Intentionally left empty.
} }
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireNoEndComponents() {
noEndComponents = true;
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireNoEndComponents(bool critical) {
noEndComponentsRequirement.enable(critical);
return *this; return *this;
} }
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireValidInitialScheduler() {
validInitialScheduler = true;
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireValidInitialScheduler(bool critical) {
validInitialSchedulerRequirement.enable(critical);
return *this; return *this;
} }
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireLowerBounds() {
lowerBounds = true;
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireLowerBounds(bool critical) {
lowerBoundsRequirement.enable(critical);
return *this; return *this;
} }
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireUpperBounds() {
upperBounds = true;
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireUpperBounds(bool critical) {
upperBoundsRequirement.enable(critical);
return *this; return *this;
} }
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireBounds() {
requireLowerBounds();
requireUpperBounds();
MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireBounds(bool critical) {
requireLowerBounds(critical);
requireUpperBounds(critical);
return *this; return *this;
} }
bool MinMaxLinearEquationSolverRequirements::requiresNoEndComponents() const {
return noEndComponents;
SolverRequirement const& MinMaxLinearEquationSolverRequirements::noEndComponents() const {
return noEndComponentsRequirement;
} }
bool MinMaxLinearEquationSolverRequirements::requiresValidInitialScheduler() const {
return validInitialScheduler;
SolverRequirement const& MinMaxLinearEquationSolverRequirements::validInitialScheduler() const {
return validInitialSchedulerRequirement;
} }
bool MinMaxLinearEquationSolverRequirements::requiresLowerBounds() const {
return lowerBounds;
SolverRequirement const& MinMaxLinearEquationSolverRequirements::lowerBounds() const {
return lowerBoundsRequirement;
} }
bool MinMaxLinearEquationSolverRequirements::requiresUpperBounds() const {
return upperBounds;
SolverRequirement const& MinMaxLinearEquationSolverRequirements::upperBounds() const {
return upperBoundsRequirement;
} }
bool MinMaxLinearEquationSolverRequirements::requires(Element const& element) const {
SolverRequirement const& MinMaxLinearEquationSolverRequirements::get(Element const& element) const {
switch (element) { switch (element) {
case Element::NoEndComponents: return noEndComponents; break;
case Element::ValidInitialScheduler: return validInitialScheduler; break;
case Element::LowerBounds: return lowerBounds; break;
case Element::UpperBounds: return upperBounds; break;
case Element::NoEndComponents: return noEndComponents(); break;
case Element::ValidInitialScheduler: return validInitialScheduler(); break;
case Element::LowerBounds: return lowerBounds(); break;
case Element::UpperBounds: return upperBounds(); break;
} }
} }
void MinMaxLinearEquationSolverRequirements::clearNoEndComponents() { void MinMaxLinearEquationSolverRequirements::clearNoEndComponents() {
noEndComponents = false;
validInitialScheduler = false;
noEndComponentsRequirement.clear();
validInitialSchedulerRequirement.clear();
} }
void MinMaxLinearEquationSolverRequirements::clearValidInitialScheduler() { void MinMaxLinearEquationSolverRequirements::clearValidInitialScheduler() {
validInitialScheduler = false;
validInitialSchedulerRequirement.clear();
} }
void MinMaxLinearEquationSolverRequirements::clearLowerBounds() { void MinMaxLinearEquationSolverRequirements::clearLowerBounds() {
lowerBounds = false;
lowerBoundsRequirement.clear();
} }
void MinMaxLinearEquationSolverRequirements::clearUpperBounds() { void MinMaxLinearEquationSolverRequirements::clearUpperBounds() {
upperBounds = false;
upperBoundsRequirement.clear();
} }
void MinMaxLinearEquationSolverRequirements::clearBounds() { void MinMaxLinearEquationSolverRequirements::clearBounds() {
@ -80,8 +80,47 @@ namespace storm {
clearUpperBounds(); clearUpperBounds();
} }
bool MinMaxLinearEquationSolverRequirements::empty() const {
return !noEndComponents && !validInitialScheduler && !lowerBounds && !upperBounds;
bool MinMaxLinearEquationSolverRequirements::hasEnabledRequirement() const {
return noEndComponentsRequirement || validInitialSchedulerRequirement || lowerBoundsRequirement || upperBoundsRequirement;
}
bool MinMaxLinearEquationSolverRequirements::hasEnabledCriticalRequirement() const {
return noEndComponentsRequirement.isCritical() || validInitialSchedulerRequirement.isCritical() || lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical();
}
std::string MinMaxLinearEquationSolverRequirements::getEnabledRequirementsAsString() const {
std::string res = "[";
bool first = true;
if (noEndComponents()) {
if (!first) { res += ", "; } else {first = false;}
res += "NoEndComponents";
if (noEndComponents().isCritical()) {
res += "(mandatory)";
}
}
if (validInitialScheduler()) {
if (!first) { res += ", "; } else {first = false;}
res += "validInitialScheduler";
if (validInitialScheduler().isCritical()) {
res += "(mandatory)";
}
}
if (lowerBounds()) {
if (!first) { res += ", "; } else {first = false;}
res += "lowerBounds";
if (lowerBounds().isCritical()) {
res += "(mandatory)";
}
}
if (upperBounds()) {
if (!first) { res += ", "; } else {first = false;}
res += "upperBounds";
if (upperBounds().isCritical()) {
res += "(mandatory)";
}
}
res += "]";
return res;
} }
} }

41
src/storm/solver/MinMaxLinearEquationSolverRequirements.h
View File

@ -1,6 +1,9 @@
#pragma once #pragma once
#include <string>
#include "storm/solver/LinearEquationSolverRequirements.h" #include "storm/solver/LinearEquationSolverRequirements.h"
#include "storm/solver/SolverRequirement.h"
namespace storm { namespace storm {
namespace solver { namespace solver {
@ -20,19 +23,21 @@ namespace storm {
UpperBounds UpperBounds
}; };
// The type of a requirement.
MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements = LinearEquationSolverRequirements()); MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements = LinearEquationSolverRequirements());
MinMaxLinearEquationSolverRequirements& requireNoEndComponents();
MinMaxLinearEquationSolverRequirements& requireValidInitialScheduler();
MinMaxLinearEquationSolverRequirements& requireLowerBounds();
MinMaxLinearEquationSolverRequirements& requireUpperBounds();
MinMaxLinearEquationSolverRequirements& requireBounds();
MinMaxLinearEquationSolverRequirements& requireNoEndComponents(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireValidInitialScheduler(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireLowerBounds(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireUpperBounds(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireBounds(bool critical = true);
bool requiresNoEndComponents() const;
bool requiresValidInitialScheduler() const;
bool requiresLowerBounds() const;
bool requiresUpperBounds() const;
bool requires(Element const& element) const;
SolverRequirement const& noEndComponents() const;
SolverRequirement const& validInitialScheduler() const;
SolverRequirement const& lowerBounds() const;
SolverRequirement const& upperBounds() const;
SolverRequirement const& get(Element const& element) const;
void clearNoEndComponents(); void clearNoEndComponents();
void clearValidInitialScheduler(); void clearValidInitialScheduler();
@ -40,13 +45,19 @@ namespace storm {
void clearUpperBounds(); void clearUpperBounds();
void clearBounds(); void clearBounds();
bool empty() const;
bool hasEnabledRequirement() const;
bool hasEnabledCriticalRequirement() const;
/*!
* Returns a string that enumerates the enabled requirements
*/
std::string getEnabledRequirementsAsString() const;
private: private:
bool noEndComponents;
bool validInitialScheduler;
bool lowerBounds;
bool upperBounds;
SolverRequirement noEndComponentsRequirement;
SolverRequirement validInitialSchedulerRequirement;
SolverRequirement lowerBoundsRequirement;
SolverRequirement upperBoundsRequirement;
}; };
} }

32
src/storm/solver/SolverRequirement.cpp
View File

@ -0,0 +1,32 @@
#include "storm/solver/SolverRequirement.h"
#include <vector>
#include "storm/utility/vector.h"
namespace storm {
namespace solver {
SolverRequirement::SolverRequirement() : enabled(false), critical(false) {
// Intentionally left empty
}
SolverRequirement::operator bool() const {
return enabled;
}
void SolverRequirement::enable(bool critical) {
this->enabled = true;
this->critical = critical;
}
void SolverRequirement::clear() {
enabled = false;
critical = false;
}
bool SolverRequirement::isCritical() const {
return this->critical;
}
}
}

39
src/storm/solver/SolverRequirement.h
View File

@ -0,0 +1,39 @@
#pragma once
namespace storm {
namespace solver {
class SolverRequirement {
public:
SolverRequirement();
SolverRequirement(SolverRequirement const& other) = default;
/*!
* Returns true if this is a requirement of the considered solver.
*/
operator bool() const;
/*!
* Enables this requirement.
* @param critical if set, it is assumed that the solver will fail in case this requirement is not met
*/
void enable(bool critical = true);
/*!
* Clears this requirement.
*/
void clear();
/*!
* Returns true if the solver fails in case this requirement is not met.
*/
bool isCritical() const;
private:
bool enabled;
bool critical;
};
}
}

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

@ -8,7 +8,7 @@
#include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/InvalidEnvironmentException.h"
#include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/UnmetRequirementException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm { namespace storm {
namespace solver { namespace solver {
@ -184,13 +184,13 @@ namespace storm {
this->sccSolver->setInitialScheduler(std::move(choices)); this->sccSolver->setInitialScheduler(std::move(choices));
} }
auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir);
if (req.requiresUpperBounds() && this->hasUpperBound()) {
if (req.upperBounds() && this->hasUpperBound()) {
req.clearUpperBounds(); req.clearUpperBounds();
} }
if (req.requiresLowerBounds() && this->hasLowerBound()) {
if (req.lowerBounds() && this->hasLowerBound()) {
req.clearLowerBounds(); req.clearLowerBounds();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
this->sccSolver->setRequirementsChecked(true); this->sccSolver->setRequirementsChecked(true);
bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, x, b); bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, x, b);
@ -252,16 +252,16 @@ namespace storm {
// Requirements // Requirements
auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir);
if (req.requiresUpperBounds() && this->hasUpperBound()) {
if (req.upperBounds() && this->hasUpperBound()) {
req.clearUpperBounds(); req.clearUpperBounds();
} }
if (req.requiresLowerBounds() && this->hasLowerBound()) {
if (req.lowerBounds() && this->hasLowerBound()) {
req.clearLowerBounds(); req.clearLowerBounds();
} }
if (req.requiresValidInitialScheduler() && this->hasInitialScheduler()) {
if (req.validInitialScheduler() && this->hasInitialScheduler()) {
req.clearValidInitialScheduler(); req.clearValidInitialScheduler();
} }
STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met.");
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
this->sccSolver->setRequirementsChecked(true); this->sccSolver->setRequirementsChecked(true);
// Invoke scc solver // Invoke scc solver

2
src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp
View File

@ -152,7 +152,7 @@ namespace {
solver->setBounds(this->parseNumber("0"), this->parseNumber("2")); solver->setBounds(this->parseNumber("0"), this->parseNumber("2"));
storm::solver::MinMaxLinearEquationSolverRequirements req = solver->getRequirements(this->env()); storm::solver::MinMaxLinearEquationSolverRequirements req = solver->getRequirements(this->env());
req.clearBounds(); req.clearBounds();
ASSERT_TRUE(req.empty());
ASSERT_FALSE(req.hasEnabledRequirement());
ASSERT_NO_THROW(solver->solveEquations(this->env(), storm::OptimizationDirection::Minimize, x, b)); ASSERT_NO_THROW(solver->solveEquations(this->env(), storm::OptimizationDirection::Minimize, x, b));
EXPECT_NEAR(x[0], this->parseNumber("0.5"), this->precision()); EXPECT_NEAR(x[0], this->parseNumber("0.5"), this->precision());

Write Preview
Loading…
Cancel
Save