From f9f845bb792dafee8f70603306b6e24f77e9f461 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 3 Dec 2019 13:46:51 +0100 Subject: [PATCH] Separated LRA tests from CTMC tests and added a testcase for LRA Rewards --- .../examples/testfiles/ctmc/lrarewards.sm | 11 + .../csl/CtmcCslModelCheckerTest.cpp | 14 - .../csl/LraCtmcCslModelCheckerTest.cpp | 400 ++++++++++++++++++ 3 files changed, 411 insertions(+), 14 deletions(-) create mode 100644 resources/examples/testfiles/ctmc/lrarewards.sm create mode 100755 src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp diff --git a/resources/examples/testfiles/ctmc/lrarewards.sm b/resources/examples/testfiles/ctmc/lrarewards.sm new file mode 100644 index 000000000..cdbcd2ea9 --- /dev/null +++ b/resources/examples/testfiles/ctmc/lrarewards.sm @@ -0,0 +1,11 @@ +ctmc + +module main + s : [0..3]; + [] s < 3 -> 3/2: (s'=s+1); + [] s > 0 -> 3: (s'=s-1); +endmodule + +rewards + true: s; +endrewards diff --git a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp index 98a91f945..1adc011b5 100755 --- a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp @@ -302,7 +302,6 @@ namespace { formulasString += "; P=? [ !\"minimum\" U>=1 \"minimum\"]"; formulasString += "; P=? [ \"minimum\" U>=1 !\"minimum\"]"; formulasString += "; R=? [C<=100]"; - formulasString += "; LRA=? [\"minimum\"]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", formulasString); auto model = std::move(modelFormulas.first); @@ -333,9 +332,6 @@ namespace { result = checker->check(this->env(), tasks[6]); EXPECT_NEAR(this->parseNumber("0.8602815057967503"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[7]); - EXPECT_NEAR(this->parseNumber("0.99999766034263426"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } @@ -345,7 +341,6 @@ namespace { formulasString += "; P=? [ !\"down\" U<=10000 \"fail_io\"]"; formulasString += "; P=? [ !\"down\" U<=10000 \"fail_sensors\"]"; formulasString += "; R{\"up\"}=? [C<=10000]"; - formulasString += "; LRA=? [\"fail_sensors\"]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString); auto model = std::move(modelFormulas.first); @@ -371,13 +366,10 @@ namespace { result = checker->check(this->env(), tasks[4]); EXPECT_NEAR(this->parseNumber("2.7745274082080154"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("0.93458866427696596"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } TYPED_TEST(CtmcCslModelCheckerTest, Polling) { std::string formulasString = "P=?[ F<=10 \"target\"]"; - formulasString += "; LRA=?[\"target\"]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString); auto model = std::move(modelFormulas.first); @@ -391,8 +383,6 @@ namespace { result = checker->check(this->env(), tasks[0]); EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("0.20079750055570736"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } @@ -403,7 +393,6 @@ namespace { formulasString += "; R=? [I=10]"; formulasString += "; R=? [C<=10]"; formulasString += "; R=? [F \"first_queue_full\"&\"second_queue_full\"]"; - formulasString += "; LRA=? [\"first_queue_full\"]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", formulasString); auto model = std::move(modelFormulas.first); @@ -431,9 +420,6 @@ namespace { result = checker->check(this->env(), tasks[5]); EXPECT_NEAR(this->parseNumber("262.85103824276308"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[6]); - EXPECT_NEAR(this->parseNumber("0.9100373532"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } TYPED_TEST(CtmcCslModelCheckerTest, simple2) { diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp new file mode 100755 index 000000000..629684560 --- /dev/null +++ b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp @@ -0,0 +1,400 @@ +#include "test/storm_gtest.h" +#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-conv/api/storm-conv.h" +#include "storm-parsers/api/properties.h" +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/symbolic/Ctmc.h" +#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/environment/solver/NativeSolverEnvironment.h" +#include "storm/environment/solver/GmmxxSolverEnvironment.h" +#include "storm/environment/solver/EigenSolverEnvironment.h" +#include "storm/environment/solver/LongRunAverageSolverEnvironment.h" + +namespace { + + enum class CtmcEngine {PrismSparse, JaniSparse, JaniHybrid}; + + class GBSparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + return env; + } + }; + + class GBJaniSparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::JaniSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + return env; + } + }; + + class GBJaniHybridCuddGmmxxGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const CtmcEngine engine = CtmcEngine::JaniHybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + env.solver().lra().setPrecision(storm::utility::convertNumber(1e-8)); // Need to increase precision because eq sys yields incorrect results + return env; + } + }; + + class GBJaniHybridSylvanGmmxxGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const CtmcEngine engine = CtmcEngine::JaniHybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + env.solver().lra().setPrecision(storm::utility::convertNumber(1e-8)); // Need to increase precision because eq sys yields incorrect results + return env; + } + }; + + class GBSparseEigenDGmresEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres); + env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + return env; + } + }; + + class GBSparseEigenRationalLUEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + return env; + } + }; + + class GBSparseNativeSorEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); + env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR); + env.solver().native().setSorOmega(storm::utility::convertNumber(0.7)); // LRA computation fails for 0.9 + env.solver().native().setPrecision(storm::utility::convertNumber(1e-9)); + env.solver().native().setRelativeTerminationCriterion(false); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations); + return env; + } + }; + + class DistrSparseGmmxxGmresIluEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations); + env.solver().lra().setPrecision(storm::utility::convertNumber(1e-8)); // Need to increase precision because eq sys yields incorrect results + return env; + } + }; + + class DistrSparseEigenDoubleLUEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres); + env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu); + env.solver().eigen().setPrecision(storm::utility::convertNumber(1e-8)); + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations); + return env; + } + }; + + class ValueIterationSparseEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models + static const CtmcEngine engine = CtmcEngine::PrismSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().lra().setDetLraMethod(storm::solver::LraMethod::ValueIteration); + return env; + } + }; + + template + class LraCtmcCslModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Ctmc SparseModelType; + typedef typename storm::models::symbolic::Ctmc SymbolicModelType; + + LraCtmcCslModelCheckerTest() : _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; } + bool isSymbolicModel() const { return std::is_same::value; } + CtmcEngine getEngine() const { return TestType::engine; } + + 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, true); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + if (TestType::engine == CtmcEngine::PrismSparse) { + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + } else if (TestType::engine == CtmcEngine::JaniSparse) { + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + janiData.first.substituteFunctions(); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSparseModel(janiData.first, result.second)->template as(); + } + return result; + } + + 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, true); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + if (TestType::engine == CtmcEngine::JaniHybrid) { + auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + janiData.first.substituteFunctions(); + result.second = storm::api::extractFormulasFromProperties(janiData.second); + result.first = storm::api::buildSymbolicModel(janiData.first, 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 == CtmcEngine::PrismSparse || TestType::engine == CtmcEngine::JaniSparse) { + 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 == CtmcEngine::JaniHybrid) { + return std::make_shared>(*model); + } + 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 { + return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); + } + } + }; + + typedef ::testing::Types< + GBSparseGmmxxGmresIluEnvironment, + GBJaniSparseGmmxxGmresIluEnvironment, + GBJaniHybridCuddGmmxxGmresEnvironment, + GBJaniHybridSylvanGmmxxGmresEnvironment, + GBSparseEigenDGmresEnvironment, + GBSparseEigenRationalLUEnvironment, + GBSparseNativeSorEnvironment, + DistrSparseGmmxxGmresIluEnvironment, + DistrSparseEigenDoubleLUEnvironment, + ValueIterationSparseEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(LraCtmcCslModelCheckerTest, TestingTypes,); + + TYPED_TEST(LraCtmcCslModelCheckerTest, Cluster) { + std::string formulasString = "LRA=? [\"minimum\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(276ul, model->getNumberOfStates()); + EXPECT_EQ(1120ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.99999766034263426"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + } + + TYPED_TEST(LraCtmcCslModelCheckerTest, Embedded) { + std::string formulasString = "LRA=? [\"fail_sensors\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(3478ul, model->getNumberOfStates()); + EXPECT_EQ(14639ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.93458866427696596"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(LraCtmcCslModelCheckerTest, Polling) { + std::string formulasString = "LRA=?[\"target\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(22ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.20079750055570736"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + } + + TYPED_TEST(LraCtmcCslModelCheckerTest, Tandem) { + std::string formulasString = "LRA=? [\"first_queue_full\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(66ul, model->getNumberOfStates()); + EXPECT_EQ(189ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.9100373532"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + + TYPED_TEST(LraCtmcCslModelCheckerTest, Rewards) { + std::string formulasString = "R=? [ LRA ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/lrarewards.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(4ul, model->getNumberOfStates()); + EXPECT_EQ(6ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("11/15"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + +}