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

Towards allowing CLN numbers for RationalNumbers again.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
bdcd181458
commit
dd7dc4b797
12 changed files with 21 additions and 18 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. 4
      src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp
  2. 2
      src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
  3. 2
      src/storm-pomdp/storage/BeliefManager.h
  4. 2
      src/storm/abstraction/AbstractionInformation.cpp
  5. 2
      src/storm/environment/solver/LongRunAverageSolverEnvironment.cpp
  6. 2
      src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp
  7. 4
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  8. 4
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
  9. 4
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp
  10. 7
      src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp
  11. 4
      src/storm/solver/GlpkLpSolver.cpp
  12. 2
      src/storm/storage/expressions/SimpleValuation.cpp

4
src/storm-pomdp-cli/settings/modules/BeliefExplorationSettings.cpp
View File

@ -136,7 +136,7 @@ namespace storm {
template<typename ValueType>
void BeliefExplorationSettings::setValuesInOptionsStruct(storm::pomdp::modelchecker::ApproximatePOMDPModelCheckerOptions<ValueType>& options) const {
options.refine = isRefineSet();
options.refinePrecision = getRefinePrecision();
options.refinePrecision = storm::utility::convertNumber<ValueType>(getRefinePrecision());
if (isRefineStepLimitSet()) {
options.refineStepLimit = getRefineStepLimit();
} else {
@ -158,7 +158,7 @@ namespace storm {
options.obsThresholdInit = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdInit());
options.obsThresholdIncrementFactor = storm::utility::convertNumber<ValueType>(getObservationScoreThresholdFactor());
options.numericPrecision = getNumericPrecision();
options.numericPrecision = storm::utility::convertNumber<ValueType>(getNumericPrecision());
if (storm::NumberTraits<ValueType>::IsExact) {
if (isNumericPrecisionSetFromDefault()) {
STORM_LOG_WARN_COND(storm::utility::isZero(options.numericPrecision), "Setting numeric precision to zero because exact arithmethic is used.");

2
src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
View File

@ -39,7 +39,7 @@ namespace storm {
ApproximatePOMDPModelchecker<PomdpModelType, BeliefValueType>::Result::diff(bool relative) const {
ValueType diff = upperBound - lowerBound;
if (diff < storm::utility::zero<ValueType>()) {
STORM_LOG_WARN_COND(diff >= 1e-6, "Upper bound '" << upperBound << "' is smaller than lower bound '" << lowerBound << "': Difference is " << diff << ".");
STORM_LOG_WARN_COND(diff >= storm::utility::convertNumber<ValueType>(1e-6), "Upper bound '" << upperBound << "' is smaller than lower bound '" << lowerBound << "': Difference is " << diff << ".");
diff = storm::utility::zero<ValueType >();
}
if (relative && !storm::utility::isZero(upperBound)) {

2
src/storm-pomdp/storage/BeliefManager.h
View File

@ -310,7 +310,7 @@ namespace storm {
BeliefValueType x = resolution;
for (auto const& entry : belief) {
qsRow.push_back(storm::utility::floor(x)); // v
sorted_diffs.emplace(toOriginalIndicesMap.size(), x - qsRow.back()); // x-v
sorted_diffs.emplace(toOriginalIndicesMap.size(), ValueType(x - qsRow.back())); // x-v
toOriginalIndicesMap.push_back(entry.first);
x -= entry.second * resolution;
}

2
src/storm/abstraction/AbstractionInformation.cpp
View File

@ -465,7 +465,7 @@ namespace storm {
std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> AbstractionInformation<DdType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> result;
storm::dd::Add<DdType, double> lowerChoiceAsAdd = choice.template toAdd<double>();
storm::dd::Add<DdType, ValueType> lowerChoiceAsAdd = choice.template toAdd<ValueType>();
for (auto const& successorValuePair : lowerChoiceAsAdd) {
uint_fast64_t updateIndex = this->decodeAux(successorValuePair.first, 0, this->getAuxVariableCount());

2
src/storm/environment/solver/LongRunAverageSolverEnvironment.cpp
View File

@ -18,7 +18,7 @@ namespace storm {
if (lraSettings.isMaximalIterationCountSet()) {
maxIters = lraSettings.getMaximalIterationCount();
}
aperiodicFactor = lraSettings.getAperiodicFactor();
aperiodicFactor = storm::utility::convertNumber<storm::RationalNumber>(lraSettings.getAperiodicFactor());
}
LongRunAverageSolverEnvironment::~LongRunAverageSolverEnvironment() {

2
src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp
View File

@ -13,7 +13,7 @@ namespace storm {
maMethodSetFromDefault = tbSettings.isMaMethodSetFromDefaultValue();
precision = storm::utility::convertNumber<storm::RationalNumber>(tbSettings.getPrecision());
relative = tbSettings.isRelativePrecision();
unifPlusKappa = tbSettings.getUnifPlusKappa();
unifPlusKappa = storm::utility::convertNumber<storm::RationalNumber>(tbSettings.getUnifPlusKappa());
}
TimeBoundedSolverEnvironment::~TimeBoundedSolverEnvironment() {

4
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -60,7 +60,7 @@ namespace storm {
using detail::PreviousExplicitResult;
template<storm::dd::DdType Type, typename ModelType>
GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : options(options), smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()), debug(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isDebugSet()) {
GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, GameBasedMdpModelCheckerOptions const& options, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : options(options), smtSolverFactory(smtSolverFactory), comparator(storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getRelativeTerminationCriterion()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()), debug(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isDebugSet()) {
if (model.hasUndefinedConstants()) {
auto undefinedConstants = model.getUndefinedConstants();
@ -1119,7 +1119,7 @@ namespace storm {
}
if (sanityCheck) {
storm::utility::ConstantsComparator<ValueType> sanityComparator( 1e-6, true);
storm::utility::ConstantsComparator<ValueType> sanityComparator( storm::utility::convertNumber<ValueType>(1e-6), true);
///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should
///////// still be the lower ones.

4
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
View File

@ -663,7 +663,7 @@ namespace storm {
// The issue has to be for some normal vector with a negative entry. Otherwise, the intersection with the downward closure wouldn't be empty
bool normalVectorContainsNegative = false;
for (auto const& hi : h.normalVector()) {
if (hi < storm::utility::zero<ValueType>()) {
if (hi < storm::utility::zero<GeometryValueType>()) {
normalVectorContainsNegative = true;
break;
}
@ -743,7 +743,7 @@ namespace storm {
if (objectiveHelper[objIndex].minimizing()) {
inducedValue = -inducedValue;
}
inducedPoint.push_back(inducedValue);
inducedPoint.push_back(storm::utility::convertNumber<GeometryValueType>(inducedValue));
// If this objective has weight zero, the lp solution is not necessarily correct
if (!storm::utility::isZero(currentWeightVector[objIndex])) {
ValueType lpValue = lpModel->getContinuousValue(currentObjectiveVariables[objIndex]);

4
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp
View File

@ -476,7 +476,7 @@ namespace storm {
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::negateMinObjectives(std::vector<GeometryValueType>& vector) const {
for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
if (objectiveHelper[objIndex].minimizing()) {
vector[objIndex] *= -storm::utility::one<ModelValueType>();
vector[objIndex] *= -storm::utility::one<GeometryValueType>();
}
}
}
@ -484,7 +484,7 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::initializeFacets(Environment const& env) {
for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
std::vector<GeometryValueType> weightVector(objectives.size(), storm::utility::zero<ModelValueType>());
std::vector<GeometryValueType> weightVector(objectives.size(), storm::utility::zero<GeometryValueType>());
weightVector[objIndex] = storm::utility::one<GeometryValueType>();
std::vector<GeometryValueType> point;
if (wvChecker) {

7
src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp
View File

@ -152,9 +152,12 @@ namespace storm {
}
prec *= factor;
if (relative) {
return std::make_pair<ValueType, ValueType>(value * (1/(prec + 1)), value * (1 + prec/(prec +1)));
ValueType one = storm::utility::one<ValueType>();
ValueType lower = value * (one / (prec + one));
ValueType upper = value * (one + prec / (prec + one));
return std::make_pair(lower, upper);
} else {
return std::make_pair<ValueType, ValueType>(value - prec, value + prec);
return std::pair<ValueType, ValueType>(value - prec, value + prec);
}
}

4
src/storm/solver/GlpkLpSolver.cpp
View File

@ -512,9 +512,9 @@ namespace storm {
ValueType GlpkLpSolver<ValueType>::getMILPGap(bool relative) const {
STORM_LOG_ASSERT(this->isOptimal(), "Asked for the MILP gap although there is no (bounded) solution.");
if (relative) {
return this->actualRelativeMILPGap;
return storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap);
} else {
return storm::utility::abs<ValueType>(this->actualRelativeMILPGap * getObjectiveValue());
return storm::utility::abs<ValueType>(storm::utility::convertNumber<ValueType>(this->actualRelativeMILPGap) * getObjectiveValue());
}
}

2
src/storm/storage/expressions/SimpleValuation.cpp
View File

@ -152,7 +152,7 @@ namespace storm {
} else if (variable.second.isIntegerType()) {
result[variable.first.getName()] = this->getIntegerValue(variable.first);
} else if (variable.second.isRationalType()) {
result[variable.first.getName()] = this->getRationalValue(variable.first);
result[variable.first.getName()] = storm::utility::convertNumber<storm::RationalNumber>(this->getRationalValue(variable.first));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
}

Write Preview
Loading…
Cancel
Save