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

moved requirements to new file

tempestpy_adaptions
dehnert 7 years ago
parent
4c5cdfeafc
commit
3c4de8ace3
3 changed files with 79 additions and 71 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. 6
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
  2. 69
      src/storm/solver/MinMaxLinearEquationSolver.h
  3. 75
      src/storm/solver/MinMaxLinearEquationSolverRequirements.h

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

@ -230,9 +230,9 @@ namespace storm {
if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
if (upperResultBound) solver->setUpperBound(upperResultBound.get());
if (!stepBound) solver->setTrackScheduler(true);
if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setSchedulerHint(std::move(minSchedChoices.get()));
if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setSchedulerHint(std::move(maxSchedChoices.get()));
if (this->currentCheckTask->isBoundSet() && solver->hasSchedulerHint()) {
if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setInitialScheduler(std::move(minSchedChoices.get()));
if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setInitialScheduler(std::move(maxSchedChoices.get()));
if (this->currentCheckTask->isBoundSet() && solver->hasInitialScheduler()) {
// If we reach this point, we know that after applying the hint, the x-values can only become larger (if we maximize) or smaller (if we minimize).
std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel->getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);

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

@ -12,6 +12,7 @@
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/Scheduler.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/MinMaxLinearEquationSolverRequirements.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/utility/macros.h"
@ -29,74 +30,6 @@ namespace storm {
StochasticShortestPath
};
class MinMaxLinearEquationSolverRequirements {
public:
enum class Element {
NoEndComponents, NoZeroRewardEndComponents, ValidInitialScheduler, GlobalLowerBound, GlobalUpperBound
};
MinMaxLinearEquationSolverRequirements() : noEndComponents(false), noZeroRewardEndComponents(false), validInitialScheduler(false), globalLowerBound(false), globalUpperBound(false) {
// Intentionally left empty.
}
MinMaxLinearEquationSolverRequirements& setNoEndComponents(bool value = true) {
noEndComponents = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setNoZeroRewardEndComponents(bool value = true) {
noZeroRewardEndComponents = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setValidInitialScheduler(bool value = true) {
validInitialScheduler = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setGlobalLowerBound(bool value = true) {
globalLowerBound = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setGlobalUpperBound(bool value = true) {
globalUpperBound = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& set(Element const& element, bool value = true) {
switch (element) {
case Element::NoEndComponents: noEndComponents = value; break;
case Element::NoZeroRewardEndComponents: noZeroRewardEndComponents = value; break;
case Element::ValidInitialScheduler: validInitialScheduler = value; break;
case Element::GlobalLowerBound: globalLowerBound = value; break;
case Element::GlobalUpperBound: globalUpperBound = value; break;
}
return *this;
}
bool requires(Element const& element) {
switch (element) {
case Element::NoEndComponents: return noEndComponents; break;
case Element::NoZeroRewardEndComponents: return noZeroRewardEndComponents; break;
case Element::ValidInitialScheduler: return validInitialScheduler; break;
case Element::GlobalLowerBound: return globalLowerBound; break;
case Element::GlobalUpperBound: return globalUpperBound; break;
}
}
bool empty() const {
return !noEndComponents && !noZeroRewardEndComponents && !validInitialScheduler && !globalLowerBound && !globalUpperBound;
}
private:
bool noEndComponents;
bool noZeroRewardEndComponents;
bool validInitialScheduler;
bool globalLowerBound;
bool globalUpperBound;
};
/*!
* A class representing the interface that all min-max linear equation solvers shall implement.
*/

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

@ -0,0 +1,75 @@
#pragma once
namespace storm {
namespace solver {
class MinMaxLinearEquationSolverRequirements {
public:
enum class Element {
NoEndComponents, NoZeroRewardEndComponents, ValidInitialScheduler, GlobalLowerBound, GlobalUpperBound
};
MinMaxLinearEquationSolverRequirements() : noEndComponents(false), noZeroRewardEndComponents(false), validInitialScheduler(false), globalLowerBound(false), globalUpperBound(false) {
// Intentionally left empty.
}
MinMaxLinearEquationSolverRequirements& setNoEndComponents(bool value = true) {
noEndComponents = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setNoZeroRewardEndComponents(bool value = true) {
noZeroRewardEndComponents = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setValidInitialScheduler(bool value = true) {
validInitialScheduler = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setGlobalLowerBound(bool value = true) {
globalLowerBound = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setGlobalUpperBound(bool value = true) {
globalUpperBound = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& set(Element const& element, bool value = true) {
switch (element) {
case Element::NoEndComponents: noEndComponents = value; break;
case Element::NoZeroRewardEndComponents: noZeroRewardEndComponents = value; break;
case Element::ValidInitialScheduler: validInitialScheduler = value; break;
case Element::GlobalLowerBound: globalLowerBound = value; break;
case Element::GlobalUpperBound: globalUpperBound = value; break;
}
return *this;
}
bool requires(Element const& element) {
switch (element) {
case Element::NoEndComponents: return noEndComponents; break;
case Element::NoZeroRewardEndComponents: return noZeroRewardEndComponents; break;
case Element::ValidInitialScheduler: return validInitialScheduler; break;
case Element::GlobalLowerBound: return globalLowerBound; break;
case Element::GlobalUpperBound: return globalUpperBound; break;
}
}
bool empty() const {
return !noEndComponents && !noZeroRewardEndComponents && !validInitialScheduler && !globalLowerBound && !globalUpperBound;
}
private:
bool noEndComponents;
bool noZeroRewardEndComponents;
bool validInitialScheduler;
bool globalLowerBound;
bool globalUpperBound;
};
}
}
Write Preview
Loading…
Cancel
Save