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

finished rational search for MinMax solver, preparing rational search for NativeLinearEquationSolver

tempestpy_adaptions
dehnert 7 years ago
parent
0c8866203c
commit
df05711f3e
15 changed files with 119 additions and 90 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. 3
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  2. 2
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  3. 4
      src/storm/settings/modules/NativeEquationSolverSettings.cpp
  4. 2
      src/storm/settings/modules/NativeEquationSolverSettings.h
  5. 5
      src/storm/solver/AbstractEquationSolver.cpp
  6. 1
      src/storm/solver/EigenLinearEquationSolver.cpp
  7. 46
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  8. 69
      src/storm/solver/NativeLinearEquationSolver.cpp
  9. 20
      src/storm/solver/NativeLinearEquationSolver.h
  10. 5
      src/storm/utility/KwekMehlhorn.h
  11. 2
      src/storm/utility/vector.h
  12. 8
      src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  13. 6
      src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  14. 16
      src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  15. 20
      src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

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

@ -116,6 +116,7 @@ namespace storm {
requirements.clearValidInitialScheduler();
}
requirements.clearBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
}
@ -358,6 +359,7 @@ namespace storm {
requireInitialScheduler = true;
requirements.clearValidInitialScheduler();
}
requirements.clearLowerBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
}
@ -420,6 +422,7 @@ namespace storm {
solver->setInitialScheduler(std::move(initialScheduler.get()));
}
solver->setLowerBound(storm::utility::zero<ValueType>());
solver->setRequirementsChecked();
solver->solveEquations(dir, x, explicitRepresentation.second);

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

@ -1253,11 +1253,13 @@ namespace storm {
// Check for requirements of the solver.
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
requirements.clearLowerBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
std::vector<ValueType> sspResult(numberOfSspStates);
goal.restrictRelevantValues(statesNotContainedInAnyMec);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, sspMatrix);
solver->setLowerBound(storm::utility::zero<ValueType>());
solver->setRequirementsChecked();
solver->solveEquations(sspResult, b);

4
src/storm/settings/modules/NativeEquationSolverSettings.cpp
View File

@ -25,7 +25,7 @@ namespace storm {
const std::string NativeEquationSolverSettings::powerMethodMultiplicationStyleOptionName = "powmult";
NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) {
std::vector<std::string> methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power" };
std::vector<std::string> methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "ratsearch" };
this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("jacobi").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build());
@ -61,6 +61,8 @@ namespace storm {
return NativeEquationSolverSettings::LinearEquationMethod::WalkerChae;
} else if (linearEquationSystemTechniqueAsString == "power") {
return NativeEquationSolverSettings::LinearEquationMethod::Power;
} else if (linearEquationSystemTechniqueAsString == "ratsearch") {
return NativeEquationSolverSettings::LinearEquationMethod::RationalSearch;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}

2
src/storm/settings/modules/NativeEquationSolverSettings.h
View File

@ -15,7 +15,7 @@ namespace storm {
class NativeEquationSolverSettings : public ModuleSettings {
public:
// An enumeration of all available methods for solving linear equations.
enum class LinearEquationMethod { Jacobi, GaussSeidel, SOR, WalkerChae, Power };
enum class LinearEquationMethod { Jacobi, GaussSeidel, SOR, WalkerChae, Power, RationalSearch };
// An enumeration of all available convergence criteria.
enum class ConvergenceCriterion { Absolute, Relative };

5
src/storm/solver/AbstractEquationSolver.cpp
View File

@ -7,6 +7,7 @@
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/UnmetRequirementException.h"
@ -160,9 +161,9 @@ namespace storm {
if (this->hasLowerBound(BoundType::Local)) {
lowerBoundsVector = this->getLowerBounds();
} else {
STORM_LOG_THROW(this->hasLowerBound(BoundType::Global), storm::exceptions::UnmetRequirementException, "Cannot create lower bounds vector without lower bound.");
ValueType lowerBound = this->hasLowerBound(BoundType::Global) ? this->getLowerBound() : storm::utility::zero<ValueType>();
for (auto& e : lowerBoundsVector) {
e = this->getLowerBound();
e = lowerBound;
}
}
}

1
src/storm/solver/EigenLinearEquationSolver.cpp
View File

@ -358,6 +358,7 @@ namespace storm {
StormEigen::SparseLU<StormEigen::SparseMatrix<storm::RationalNumber>, StormEigen::COLAMDOrdering<int>> solver;
solver.compute(*eigenA);
solver._solve_impl(eigenB, eigenX);
return solver.info() == StormEigen::ComputationInfo::Success;
}

46
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View File

@ -232,7 +232,7 @@ namespace storm {
this->schedulerChoices = std::move(scheduler);
}
if(!this->isCachingEnabled()) {
if (!this->isCachingEnabled()) {
clearCache();
}
@ -328,8 +328,6 @@ namespace storm {
linearEquationSolver.multiplyAndReduce(dir, this->A->getRowGroupIndices(), *currentX, &b, *newX);
}
std::cout << "position 4: " << (*currentX)[4] << " vs " << (*newX)[4] << std::endl;
// Determine whether the method converged.
if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative)) {
status = Status::Converged;
@ -403,6 +401,11 @@ namespace storm {
this->startMeasureProgress();
ValueIterationResult result = performValueIteration(dir, currentX, newX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), guarantee, 0);
// Swap the result into the output x.
if (currentX == auxiliaryRowGroupVector.get()) {
std::swap(x, *currentX);
}
reportStatus(result.status, result.iterations);
// If requested, we store the scheduler for retrieval.
@ -644,10 +647,7 @@ namespace storm {
// If the value does not match the one in the values vector, the given vector is not a solution.
if (!comparator.isEqual(groupValue, *valueIt)) {
std::cout << "offending group " << group << " : " << groupValue << " vs " << *valueIt << std::endl;
return false;
} else if (group == 1) {
std::cout << "val for group 1 is " << groupValue << " vs 227630345357/3221225472" << std::endl;
}
}
@ -659,18 +659,12 @@ namespace storm {
template<typename RationalType, typename ImpreciseType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::sharpen(storm::OptimizationDirection dir, uint64_t precision, storm::storage::SparseMatrix<RationalType> const& A, std::vector<ImpreciseType> const& x, std::vector<RationalType> const& b, std::vector<RationalType>& tmp) {
std::cout << "pre sharpen x[0] " << x[0] << ", is smaller? " << (x[0] < storm::utility::convertNumber<ImpreciseType>(std::string("227630345357/3221225472"))) << " with diff " << (x[0] - storm::utility::convertNumber<ImpreciseType>(std::string("227630345357/3221225472"))) << std::endl;
storm::utility::kwek_mehlhorn::sharpen(precision, x, tmp);
for (uint64_t p = 0; p <= precision; ++p) {
storm::utility::kwek_mehlhorn::sharpen(p, x, tmp);
std::cout << "post sharpen x[0] " << tmp[0] << ", is smaller? " << (tmp[0] < storm::utility::convertNumber<RationalType>(std::string("227630345357/3221225472"))) << " with diff " << (tmp[0] - storm::utility::convertNumber<RationalType>(std::string("227630345357/3221225472"))) << std::endl;
if (std::is_same<RationalType, ImpreciseType>::value) {
std::cout << "sharpen smaller? " << (tmp[0] < storm::utility::convertNumber<RationalType>(x[0])) << std::endl;
}
if (IterativeMinMaxLinearEquationSolver<RationalType>::isSolution(dir, A, tmp, b)) {
return true;
if (IterativeMinMaxLinearEquationSolver<RationalType>::isSolution(dir, A, tmp, b)) {
return true;
}
}
return false;
}
@ -811,7 +805,7 @@ namespace storm {
template<typename RationalType, typename ImpreciseType>
struct TemporaryHelper {
static std::vector<RationalType>* getFreeRational(std::vector<RationalType>& rationalX, std::vector<ImpreciseType>*& currentX, std::vector<ImpreciseType>*& newX) {
static std::vector<RationalType>* getTemporary(std::vector<RationalType>& rationalX, std::vector<ImpreciseType>*& currentX, std::vector<ImpreciseType>*& newX) {
return &rationalX;
}
@ -822,7 +816,7 @@ namespace storm {
template<typename RationalType>
struct TemporaryHelper<RationalType, RationalType> {
static std::vector<RationalType>* getFreeRational(std::vector<RationalType>& rationalX, std::vector<RationalType>*& currentX, std::vector<RationalType>*& newX) {
static std::vector<RationalType>* getTemporary(std::vector<RationalType>& rationalX, std::vector<RationalType>*& currentX, std::vector<RationalType>*& newX) {
return newX;
}
@ -869,17 +863,17 @@ namespace storm {
uint64_t p = storm::utility::convertNumber<uint64_t>(storm::utility::ceil(storm::utility::log10<ValueType>(storm::utility::one<ValueType>() / precision)));
// Make sure that currentX and rationalX are not aliased.
std::vector<RationalType>* freeRational = TemporaryHelper<RationalType, ImpreciseType>::getFreeRational(rationalX, currentX, newX);
std::vector<RationalType>* temporaryRational = TemporaryHelper<RationalType, ImpreciseType>::getTemporary(rationalX, currentX, newX);
// Sharpen solution and place it in rationalX.
bool foundSolution = sharpen(dir, p, rationalA, *currentX, rationalB, *freeRational);
// Sharpen solution and place it in the temporary rational.
bool foundSolution = sharpen(dir, p, rationalA, *currentX, rationalB, *temporaryRational);
// After sharpen, if a solution was found, it is contained in the free rational.
if (foundSolution) {
status = Status::Converged;
TemporaryHelper<RationalType, ImpreciseType>::swapSolutions(rationalX, freeRational, x, currentX, newX);
TemporaryHelper<RationalType, ImpreciseType>::swapSolutions(rationalX, temporaryRational, x, currentX, newX);
} else {
// Increase the precision.
precision = precision / 100;
@ -897,11 +891,7 @@ namespace storm {
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsRationalSearch(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
if (this->getSettings().getForceSoundness()) {
return solveEquationsRationalSearchHelper<ValueType>(dir, x, b);
} else {
return solveEquationsRationalSearchHelper<double>(dir, x, b);
}
return solveEquationsRationalSearchHelper<double>(dir, x, b);
}
template<typename ValueType>

69
src/storm/solver/NativeLinearEquationSolver.cpp
View File

@ -30,6 +30,8 @@ namespace storm {
method = SolutionMethod::WalkerChae;
} else if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power) {
method = SolutionMethod::Power;
} else if (methodAsSetting == storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::RationalSearch) {
method = SolutionMethod::RationalSearch;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected solution technique is invalid for this solver.");
}
@ -80,8 +82,8 @@ namespace storm {
template<typename ValueType>
void NativeLinearEquationSolverSettings<ValueType>::setForceSoundness(bool value) {
forceSoundness = value;
if (forceSoundness) {
STORM_LOG_WARN_COND(method != SolutionMethod::Power, "To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'.");
if (forceSoundness && method != SolutionMethod::Power && method != SolutionMethod::RationalSearch) {
STORM_LOG_WARN("To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'.");
method = SolutionMethod::Power;
}
}
@ -389,55 +391,72 @@ namespace storm {
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsPower(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Power)");
if (!this->cachedRowVector) {
this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
}
typename NativeLinearEquationSolver<ValueType>::PowerIterationResult NativeLinearEquationSolver<ValueType>::performPowerIteration(std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX, std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations) const {
std::vector<ValueType>* currentX = &x;
this->createLowerBoundsVector(*currentX);
std::vector<ValueType>* nextX = this->cachedRowVector.get();
bool useGaussSeidelMultiplication = this->getSettings().getPowerMethodMultiplicationStyle() == storm::solver::MultiplicationStyle::GaussSeidel;
std::vector<ValueType>* originalX = currentX;
bool converged = false;
bool terminate = this->terminateNow(*currentX, SolverGuarantee::LessOrEqual);
uint64_t iterations = 0;
this->startMeasureProgress();
bool terminate = this->terminateNow(*currentX, guarantee);
uint64_t iterations = currentIterations;
while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
if (useGaussSeidelMultiplication) {
*nextX = *currentX;
this->multiplier.multAddGaussSeidelBackward(*this->A, *nextX, &b);
*newX = *currentX;
this->multiplier.multAddGaussSeidelBackward(*this->A, *newX, &b);
} else {
this->multiplier.multAdd(*this->A, *currentX, &b, *nextX);
this->multiplier.multAdd(*this->A, *currentX, &b, *newX);
}
// Now check for termination.
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *nextX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
terminate = this->terminateNow(*currentX, SolverGuarantee::LessOrEqual);
// Potentially show progress.
this->showProgressIterative(iterations);
// Set up next iteration.
std::swap(currentX, nextX);
std::swap(currentX, newX);
++iterations;
}
// Swap the pointers so that the output is always in currentX.
if (originalX == newX) {
std::swap(currentX, newX);
}
return PowerIterationResult(iterations - currentIterations, converged ? Status::Converged : (terminate ? Status::TerminatedEarly : Status::MaximalIterationsExceeded));
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsPower(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Power)");
// Prepare the solution vectors.
if (!this->cachedRowVector) {
this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
}
std::vector<ValueType>* currentX = &x;
this->createLowerBoundsVector(*currentX);
std::vector<ValueType>* newX = this->cachedRowVector.get();
// Forward call to power iteration implementation.
this->startMeasureProgress();
PowerIterationResult result = this->performPowerIteration(currentX, newX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, 0);
// Swap the result in place.
if (currentX == this->cachedRowVector.get()) {
std::swap(x, *nextX);
std::swap(x, *newX);
}
if (!this->isCachingEnabled()) {
clearCache();
}
this->logIterations(converged, terminate, iterations);
this->logIterations(result.status == Status::Converged, result.status == Status::TerminatedEarly, result.iterations);
return converged;
return result.status == Status::Converged || result.status == Status::TerminatedEarly;
}
template<typename ValueType>

20
src/storm/solver/NativeLinearEquationSolver.h
View File

@ -14,7 +14,7 @@ namespace storm {
class NativeLinearEquationSolverSettings {
public:
enum class SolutionMethod {
Jacobi, GaussSeidel, SOR, WalkerChae, Power
Jacobi, GaussSeidel, SOR, WalkerChae, Power, RationalSearch
};
NativeLinearEquationSolverSettings();
@ -76,6 +76,24 @@ namespace storm {
virtual bool internalSolveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
private:
enum class Status {
Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
};
struct PowerIterationResult {
PowerIterationResult(uint64_t iterations, Status status) : iterations(iterations), status(status) {
// Intentionally left empty.
}
uint64_t iterations;
Status status;
};
template <typename ValueTypePrime>
friend class NativeLinearEquationSolver;
PowerIterationResult performPowerIteration(std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX, std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee, uint64_t currentIterations) const;
void logIterations(bool converged, bool terminate, uint64_t iterations) const;
virtual uint64_t getMatrixRowCount() const override;

5
src/storm/utility/KwekMehlhorn.h
View File

@ -62,11 +62,6 @@ namespace storm {
ImpreciseType fraction = input[index] - integer;
auto rational = findRational<RationalType>(precision, fraction);
output[index] = storm::utility::convertNumber<RationalType>(integer) + rational;
STORM_LOG_ASSERT(storm::utility::isZero(fraction) || !storm::utility::isZero(rational), "Found zero rational for non-zero fraction " << fraction << ".");
STORM_LOG_ASSERT(rational >= storm::utility::zero<RationalType>(), "Expected non-negative rational.");
if (std::is_same<RationalType, ImpreciseType>::value) {
STORM_LOG_ASSERT(output[index] >= input[index], "Sharpen decreased value from " << input[index] << " to " << output[index] << ".");
}
}
}

2
src/storm/utility/vector.h
View File

@ -798,7 +798,6 @@ namespace storm {
} else {
T diff = val1 - val2;
if (storm::utility::abs(diff) > precision) {
std::cout << "diff " << storm::utility::abs(diff) << " vs precision " << precision << std::endl;
return false;
}
}
@ -843,7 +842,6 @@ namespace storm {
auto rightIt = vectorRight.begin();
for (; leftIt != leftIte; ++leftIt, ++rightIt) {
if (!equalModuloPrecision(*leftIt, *rightIt, precision, relativeError)) {
std::cout << "offending position " << std::distance(vectorLeft.begin(), leftIt) << std::endl;
return false;
}
}

8
src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

@ -116,8 +116,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
@ -214,8 +214,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {

6
src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -86,7 +86,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", "");
@ -108,7 +108,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
@ -130,7 +130,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666665777564049, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(14.666663348674774, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {

16
src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
View File

@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(7.3333329195156693, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333329195156693, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -112,8 +112,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(7.3333329195156693, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333329195156693, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -209,8 +209,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333328887820244, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {

20
src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -14,7 +14,7 @@
#include "storm/settings/modules/NativeEquationSolverSettings.h"
#include "storm/parser/AutoParser.h"
TEST(SparseMdpPrctlModelCheckerTest, Dice) {
TEST(NativeMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
// A parser that we use for conveniently constructing the formulas.
@ -76,14 +76,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", "");
@ -98,14 +98,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333329195156693, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333328887820244, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333316743373871, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
@ -120,17 +120,17 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666665839031339, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(14.666658997535706, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666665777564049, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(14.666663348674774, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew");
// A parser that we use for conveniently constructing the formulas.
@ -188,7 +188,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(4.2857120959008661, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
TEST(NativeMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
@ -338,7 +338,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
}
}
TEST(SparseMdpPrctlModelCheckerTest, LRA) {
TEST(NativeMdpPrctlModelCheckerTest, LRA) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;

Write Preview
Loading…
Cancel
Save