diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp new file mode 100644 index 000000000..79b635845 --- /dev/null +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -0,0 +1,208 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + +#include "storm/models/sparse/Smg.h" +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/logic/Formulas.h" +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace { + + enum class SmgEngine {PrismSparse}; + + class SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel); + env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx); + return env; + } + }; + + class SparseDoubleValueIterationGmmxxRegularMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular); + env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx); + return env; + } + }; + + class SparseDoubleValueIterationNativeGaussSeidelMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel); + env.solver().multiplier().setType(storm::solver::MultiplierType::Native); + return env; + } + }; + + class SparseDoubleValueIterationNativeRegularMultEnvironment { + public: + static const SmgEngine engine = SmgEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Smg ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular); + env.solver().multiplier().setType(storm::solver::MultiplierType::Native); + return env; + } + }; + + template + class SmgRpatlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Smg SparseModelType; + + SmgRpatlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} + bool isSparseModel() const { return std::is_same::value; } + + template + typename std::enable_if::value, std::pair, std::vector>>>::type + buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + if (TestType::engine == SmgEngine::PrismSparse) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + } + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == SmgEngine::PrismSparse) { + return std::make_shared>(*model); + } else { + STORM_LOG_ERROR("TestType::engine must be PrismSparse!"); + return nullptr; + } + } + +/* bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQualitativeCheckResult().forallTrue(); + }*/ + + ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); + } + + private: + storm::Environment _environment; + + std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { + if (isSparseModel()) { + return std::make_unique(model->template as()->getInitialStates()); + } else { + STORM_LOG_ERROR("Smg Rpatl Model must be a Sparse Model!"); + return nullptr; + } + } + }; + + typedef ::testing::Types< + SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment, + SparseDoubleValueIterationGmmxxRegularMultEnvironment, + SparseDoubleValueIterationNativeGaussSeidelMultEnvironment, + SparseDoubleValueIterationNativeRegularMultEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(SmgRpatlModelCheckerTest, TestingTypes,); + + TYPED_TEST(SmgRpatlModelCheckerTest, Walker) { + std::string formulasString = "<> Pmax=? [X \"s2\"]"; + formulasString += "; <> Pmin=? [X \"s2\"]"; + + // TODO: bounded eventually causes wrong compuations for native multipliers + // TODO: do some more checks for comutation +/* formulasString += "; <> Pmax=? [F \"s3\"]"; + formulasString += "; <> Pmin=? [F \"s3\"]"; + + formulasString += "; <> Pmax=? [F [3,4] \"s4\"]"; + formulasString += "; <> Pmax=? [F [3,5] \"s4\"]";*/ + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/walker.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(12ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Smg); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + +/* result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.345454"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("0.576"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision());*/ + } + + // TODO: create more test cases +}