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

fixed some issue in sylvan sharpen and forward minmax bounds to linear equation solver

tempestpy_adaptions
dehnert 7 years ago
parent
f2e581b3df
commit
45a4b63a2e
7 changed files with 114 additions and 21 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. 2
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
  2. 44
      src/storm/solver/SymbolicEquationSolver.cpp
  3. 27
      src/storm/solver/SymbolicEquationSolver.h
  4. 26
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
  5. 6
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
  6. 10
      src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
  7. 20
      src/test/storm/storage/SylvanDdTest.cpp

2
resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
View File

@ -606,7 +606,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_sharpen, MTBDD, a, size_t, p)
MTBDD result = mtbdd_storm_rational_number(storm_double_sharpen(mtbdd_getdouble(a), p));
return result;
} else if (mtbddnode_gettype(na) == srn_type) {
return mtbdd_storm_rational_number(storm_rational_number_sharpen((storm_rational_number_ptr)mtbdd_getstorm_rational_function_ptr(a), p));
return mtbdd_storm_rational_number(storm_rational_number_sharpen((storm_rational_number_ptr)mtbdd_getstorm_rational_number_ptr(a), p));
} else {
printf("ERROR: Unsupported value type in sharpen.\n");
assert(0);

44
src/storm/solver/SymbolicEquationSolver.cpp
View File

@ -62,7 +62,47 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getLowerBounds() const {
bool SymbolicEquationSolver<DdType, ValueType>::hasLowerBound() const {
return static_cast<bool>(lowerBound);
}
template<storm::dd::DdType DdType, typename ValueType>
ValueType const& SymbolicEquationSolver<DdType, ValueType>::getLowerBound() const {
return lowerBound.get();
}
template<storm::dd::DdType DdType, typename ValueType>
bool SymbolicEquationSolver<DdType, ValueType>::hasLowerBounds() const {
return static_cast<bool>(lowerBounds);
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> const& SymbolicEquationSolver<DdType, ValueType>::getLowerBounds() const {
return lowerBounds.get();
}
template<storm::dd::DdType DdType, typename ValueType>
bool SymbolicEquationSolver<DdType, ValueType>::hasUpperBound() const {
return static_cast<bool>(upperBound);
}
template<storm::dd::DdType DdType, typename ValueType>
ValueType const& SymbolicEquationSolver<DdType, ValueType>::getUpperBound() const {
return upperBound.get();
}
template<storm::dd::DdType DdType, typename ValueType>
bool SymbolicEquationSolver<DdType, ValueType>::hasUpperBounds() const {
return static_cast<bool>(upperBounds);
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> const& SymbolicEquationSolver<DdType, ValueType>::getUpperBounds() const {
return upperBounds.get();
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getLowerBoundsVector() const {
STORM_LOG_THROW(lowerBound || lowerBounds, storm::exceptions::UnmetRequirementException, "Requiring lower bounds, but did not get any.");
if (lowerBounds) {
return lowerBounds.get();
@ -72,7 +112,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getUpperBounds() const {
storm::dd::Add<DdType, ValueType> SymbolicEquationSolver<DdType, ValueType>::getUpperBoundsVector() const {
STORM_LOG_THROW(upperBound || upperBounds, storm::exceptions::UnmetRequirementException, "Requiring upper bounds, but did not get any.");
if (upperBounds) {
return upperBounds.get();

27
src/storm/solver/SymbolicEquationSolver.h
View File

@ -14,22 +14,31 @@ namespace storm {
SymbolicEquationSolver() = default;
SymbolicEquationSolver(storm::dd::Bdd<DdType> const& allRows);
void setLowerBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds);
void setLowerBound(ValueType const& lowerBound);
void setUpperBounds(storm::dd::Add<DdType, ValueType> const& upperBounds);
void setUpperBound(ValueType const& lowerBound);
void setBounds(ValueType const& lowerBound, ValueType const& upperBound);
void setBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds, storm::dd::Add<DdType, ValueType> const& upperBounds);
virtual void setLowerBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds);
virtual void setLowerBound(ValueType const& lowerBound);
virtual void setUpperBounds(storm::dd::Add<DdType, ValueType> const& upperBounds);
virtual void setUpperBound(ValueType const& lowerBound);
virtual void setBounds(ValueType const& lowerBound, ValueType const& upperBound);
virtual void setBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds, storm::dd::Add<DdType, ValueType> const& upperBounds);
bool hasLowerBound() const;
ValueType const& getLowerBound() const;
bool hasLowerBounds() const;
storm::dd::Add<DdType, ValueType> const& getLowerBounds() const;
bool hasUpperBound() const;
ValueType const& getUpperBound() const;
bool hasUpperBounds() const;
storm::dd::Add<DdType, ValueType> const& getUpperBounds() const;
/*!
* Retrieves a vector of lower bounds for all values (if any lower bounds are known).
*/
storm::dd::Add<DdType, ValueType> getLowerBounds() const;
storm::dd::Add<DdType, ValueType> getLowerBoundsVector() const;
/*!
* Retrieves a vector of upper bounds for all values (if any lower bounds are known).
*/
storm::dd::Add<DdType, ValueType> getUpperBounds() const;
storm::dd::Add<DdType, ValueType> getUpperBoundsVector() const;
protected:
storm::dd::DdManager<DdType>& getDdManager() const;

26
src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
View File

@ -226,7 +226,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
template<typename ImpreciseType>
typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
return solveEquationsRationalSearchHelper<ValueType, ValueType>(dir, *this, *this, b, this->getLowerBounds(), b);
return solveEquationsRationalSearchHelper<ValueType, ValueType>(dir, *this, *this, b, this->getLowerBoundsVector(), b);
}
template<storm::dd::DdType DdType, typename ValueType>
@ -236,7 +236,7 @@ namespace storm {
storm::dd::Add<DdType, storm::RationalNumber> rationalB = b.template toValueType<storm::RationalNumber>();
SymbolicMinMaxLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver(this->A.template toValueType<storm::RationalNumber>(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables, this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique<GeneralSymbolicLinearEquationSolverFactory<DdType, storm::RationalNumber>>());
storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(dir, rationalSolver, *this, rationalB, this->getLowerBounds(), b);
storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(dir, rationalSolver, *this, rationalB, this->getLowerBoundsVector(), b);
return rationalResult.template toValueType<ValueType>();
}
@ -248,7 +248,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> rationalResult;
storm::dd::Add<DdType, ImpreciseType> impreciseX;
try {
impreciseX = this->getLowerBounds().template toValueType<ImpreciseType>();
impreciseX = this->getLowerBoundsVector().template toValueType<ImpreciseType>();
storm::dd::Add<DdType, ImpreciseType> impreciseB = b.template toValueType<ImpreciseType>();
SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType> impreciseSolver(this->A.template toValueType<ImpreciseType>(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables, this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique<GeneralSymbolicLinearEquationSolverFactory<DdType, ImpreciseType>>());
@ -276,7 +276,7 @@ namespace storm {
if (this->hasInitialScheduler()) {
localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
} else {
localX = this->getLowerBounds();
localX = this->getLowerBoundsVector();
}
ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations());
@ -294,6 +294,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsWithScheduler(storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory->create(this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
this->forwardBounds(*solver);
storm::dd::Add<DdType, ValueType> diagonal = (storm::utility::dd::getRowColumnDiagonal<DdType>(x.getDdManager(), this->rowColumnMetaVariablePairs) && this->allRows).template toAdd<ValueType>();
return solveEquationsWithScheduler(*solver, scheduler, x, b, diagonal);
}
@ -327,6 +328,7 @@ namespace storm {
// Initialize linear equation solver.
std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> linearEquationSolver = linearEquationSolverFactory->create(this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
this->forwardBounds(*linearEquationSolver);
// Iteratively solve and improve the scheduler.
while (!converged && iterations < this->settings.getMaximalNumberOfIterations()) {
@ -452,6 +454,22 @@ namespace storm {
SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getSettings() const {
return settings;
}
template<storm::dd::DdType DdType, typename ValueType>
void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::forwardBounds(storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>& solver) const {
if (this->hasLowerBound()) {
solver.setLowerBound(this->getLowerBound());
}
if (this->hasLowerBounds()) {
solver.setLowerBounds(this->getLowerBounds());
}
if (this->hasUpperBound()) {
solver.setUpperBound(this->getUpperBound());
}
if (this->hasUpperBounds()) {
solver.setUpperBounds(this->getUpperBounds());
}
}
template<storm::dd::DdType DdType, typename ValueType>
MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {

6
src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
View File

@ -213,6 +213,12 @@ namespace storm {
// A scheduler that specifies with which schedulers to start.
boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
private:
/*!
* Forwards the known bounds of this solver to the given linear equation solver.
*/
void forwardBounds(storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>& solver) const;
};
template<storm::dd::DdType DdType, typename ValueType>

10
src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
View File

@ -185,7 +185,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsPower(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
PowerIterationResult result = performPowerIteration(this->getLowerBounds(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations());
PowerIterationResult result = performPowerIteration(this->getLowerBoundsVector(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations());
if (result.status == SolverStatus::Converged) {
STORM_LOG_INFO("Iterative solver (power iteration) converged in " << result.iterations << " iterations.");
@ -195,7 +195,7 @@ namespace storm {
return result.values;
}
template<storm::dd::DdType DdType, typename ValueType>
bool SymbolicNativeLinearEquationSolver<DdType, ValueType>::isSolutionFixedPoint(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
storm::dd::Add<DdType, ValueType> xAsColumn = x.swapVariables(this->rowColumnMetaVariablePairs);
@ -273,7 +273,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
template<typename ImpreciseType>
typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
return solveEquationsRationalSearchHelper<ValueType, ValueType>(*this, *this, b, this->getLowerBounds(), b);
return solveEquationsRationalSearchHelper<ValueType, ValueType>(*this, *this, b, this->getLowerBoundsVector(), b);
}
template<storm::dd::DdType DdType, typename ValueType>
@ -283,7 +283,7 @@ namespace storm {
storm::dd::Add<DdType, storm::RationalNumber> rationalB = b.template toValueType<storm::RationalNumber>();
SymbolicNativeLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver(this->A.template toValueType<storm::RationalNumber>(), this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(rationalSolver, *this, rationalB, this->getLowerBounds(), b);
storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(rationalSolver, *this, rationalB, this->getLowerBoundsVector(), b);
return rationalResult.template toValueType<ValueType>();
}
@ -295,7 +295,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> rationalResult;
storm::dd::Add<DdType, ImpreciseType> impreciseX;
try {
impreciseX = this->getLowerBounds().template toValueType<ImpreciseType>();
impreciseX = this->getLowerBoundsVector().template toValueType<ImpreciseType>();
storm::dd::Add<DdType, ImpreciseType> impreciseB = b.template toValueType<ImpreciseType>();
SymbolicNativeLinearEquationSolver<DdType, ImpreciseType> impreciseSolver(this->A.template toValueType<ImpreciseType>(), this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);

20
src/test/storm/storage/SylvanDdTest.cpp
View File

@ -855,6 +855,26 @@ TEST(SylvanDd, AddSharpenTest) {
ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("19/10")), sharpened.getValue(metaVariableToValueMap));
}
TEST(SylvanDd, AddRationalSharpenTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> dd = manager->template getAddOne<storm::RationalNumber>();
ASSERT_NO_THROW(dd.setValue(x.first, 4, storm::utility::convertNumber<storm::RationalNumber>(1.89999999)));
ASSERT_EQ(2ul, dd.getLeafCount());
storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> sharpened = dd.sharpenKwekMehlhorn(1);
std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
metaVariableToValueMap.emplace(x.first, 4);
sharpened = dd.sharpenKwekMehlhorn(1);
ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("9/5")), sharpened.getValue(metaVariableToValueMap));
sharpened = dd.sharpenKwekMehlhorn(2);
ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("19/10")), sharpened.getValue(metaVariableToValueMap));
}
TEST(SylvanDd, AddToRationalTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);

Write Preview
Loading…
Cancel
Save