From eaacc6c0ace372e6b4808050c3b69202b8be6800 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 26 Feb 2020 20:51:10 +0100 Subject: [PATCH] Included the hybrid engine in the MA test. --- .../MarkovAutomatonCslModelCheckerTest.cpp | 85 +++++++++++++------ 1 file changed, 60 insertions(+), 25 deletions(-) diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp index 056c47ba8..b10ed1081 100755 --- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp @@ -13,9 +13,11 @@ #include "storm/models/symbolic/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" +#include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/results/QuantitativeCheckResult.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/environment/solver/TopologicalSolverEnvironment.h" #include "storm/settings/modules/CoreSettings.h" @@ -25,7 +27,7 @@ namespace { - enum class MaEngine {PrismSparse, JaniSparse, JitSparse}; + enum class MaEngine {PrismSparse, JaniSparse, JitSparse, JaniHybrid}; class SparseDoubleValueIterationEnvironment { @@ -70,6 +72,20 @@ namespace { return env; } }; + class JaniHybridDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const MaEngine engine = MaEngine::JaniHybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::MarkovAutomaton 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)); + return env; + } + }; class SparseDoubleIntervalIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models @@ -150,8 +166,9 @@ namespace { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); program = storm::utility::prism::preprocess(program, constantDefinitionString); - result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); - result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSymbolicModel(janiData.first, result.second)->template as(); return result; } @@ -169,16 +186,18 @@ namespace { if (TestType::engine == MaEngine::PrismSparse || TestType::engine == MaEngine::JaniSparse || TestType::engine == MaEngine::JitSparse) { return std::make_shared>(*model); } + return nullptr; } template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { -// if (TestType::engine == MaEngine::Hybrid) { -// return std::make_shared>(*model); + if (TestType::engine == MaEngine::JaniHybrid) { + return std::make_shared>(*model); // } else if (TestType::engine == MaEngine::Dd) { // return std::make_shared>(*model); -// } + } + return nullptr; } bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { @@ -200,8 +219,7 @@ namespace { if (isSparseModel()) { return std::make_unique(model->template as()->getInitialStates()); } else { - // return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); - return nullptr; + return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); } } }; @@ -210,6 +228,7 @@ namespace { SparseDoubleValueIterationEnvironment, JaniSparseDoubleValueIterationEnvironment, JitSparseDoubleValueIterationEnvironment, + JaniHybridDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseRationalPolicyIterationEnvironment, SparseRationalRationalSearchEnvironment @@ -275,6 +294,9 @@ namespace { formulasString += "; R{\"rew2\"}max=? [C]"; formulasString += "; R{\"rew2\"}min=? [C]"; formulasString += "; R{\"rew3\"}min=? [C]"; + formulasString += "; LRAmin=? [s=0 | s=3]"; // 0 + formulasString += "; R{\"rew3\"}max=?[ LRA ]"; // 407 + formulasString += "; R{\"rew3\"}min=?[ LRA ]"; // 27 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple2.ma", formulasString); auto model = std::move(modelFormulas.first); @@ -285,26 +307,39 @@ namespace { auto checker = this->createModelChecker(model); std::unique_ptr result; - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("2"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); + if (TypeParam::engine != MaEngine::JaniHybrid) { + // Total Reward Formulas are not supported in the hybrid engine (for now). + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("2"), 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_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[6]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + } + + result = checker->check(this->env(), tasks[7]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[2]); - EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); - - result = checker->check(this->env(), tasks[3]); - EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[4]); - EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); - - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[8]); + EXPECT_NEAR(this->parseNumber("407"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[6]); - EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + result = checker->check(this->env(), tasks[9]); + EXPECT_NEAR(this->parseNumber("27"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } }