From 1f4c0325be6b9d9103cd98a87e68c2fa161bf34b Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 25 Jun 2018 11:22:52 +0200 Subject: [PATCH] test cases for ctmcs and markov automata --- resources/examples/testfiles/ctmc/simple2.sm | 28 ++ resources/examples/testfiles/ma/simple2.ma | 40 +++ .../modelchecker/CtmcCslModelCheckerTest.cpp | 23 ++ .../MarkovAutomatonCslModelCheckerTest.cpp | 264 ++++++++++++++++++ 4 files changed, 355 insertions(+) create mode 100644 resources/examples/testfiles/ctmc/simple2.sm create mode 100644 resources/examples/testfiles/ma/simple2.ma create mode 100644 src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp diff --git a/resources/examples/testfiles/ctmc/simple2.sm b/resources/examples/testfiles/ctmc/simple2.sm new file mode 100644 index 000000000..5fcc0dcab --- /dev/null +++ b/resources/examples/testfiles/ctmc/simple2.sm @@ -0,0 +1,28 @@ + +ctmc + + +module main + + s : [0..4]; // current state: + + + <> s=0 -> 4 : (s'=1) + 4 : (s'=2); + <> s=1 -> 0.3 : (s'=2) + 0.7 : (s'=1); + <> s=2 -> 0.5 : (s'=2) + 0.5 : (s'=3); + <> s=3 -> 1 : (s'=4); + <> s=4 -> 1 : (s'=3); + +endmodule + +rewards "rew1" + s=0 : 7; + [] s=2 : 1; +endrewards + + +rewards "rew2" + s=0 : 7; + [] s=2 : 1; + [] s=4 : 100; +endrewards diff --git a/resources/examples/testfiles/ma/simple2.ma b/resources/examples/testfiles/ma/simple2.ma new file mode 100644 index 000000000..95e0059b7 --- /dev/null +++ b/resources/examples/testfiles/ma/simple2.ma @@ -0,0 +1,40 @@ + +ma + + +module main + + s : [0..4]; // current state: + + + <> s=0 -> 4 : (s'=1) + 4 : (s'=2); + [alpha] s=1 -> 1 : (s'=0); + [beta] s=1 -> 0.3 : (s'=2) + 0.7 : (s'=1); + [gamma] s=2 -> 1 : (s'=1); + [delta] s=2 -> 0.5 : (s'=2) + 0.5 : (s'=3); + <> s=3 -> 1 : (s'=4); + [lambda] s=4 -> 1 : (s'=3); + +endmodule + +rewards "rew0" + [delta] s=2 : 1; +endrewards + +rewards "rew1" + s=0 : 7; + [delta] s=2 : 1; +endrewards + + +rewards "rew2" + s=0 : 7; + [delta] s=2 : 1; + [lambda] s=4 : 100; +endrewards + +rewards "rew3" + s=0 : 7; + [delta] s=2 : 1; + [gamma] s=4 : 100; +endrewards diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index 1b83be1c6..11d7d48a4 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -140,6 +140,7 @@ namespace { 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; } + storm::settings::modules::CoreSettings::Engine getEngine() const { return TestType::engine; } template typename std::enable_if::value, std::pair, std::vector>>>::type @@ -362,7 +363,29 @@ namespace { result = checker->check(this->env(), tasks[6]); EXPECT_NEAR(this->parseNumber("0.9100373532"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(CtmcCslModelCheckerTest, simple2) { + std::string formulasString = "R{\"rew1\"}=? [ C ]"; + formulasString += "; R{\"rew2\"}=? [ C ]"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/simple2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // Total reward formulas are currently not supported for non-sparse models. + if (this->isSparseModel()) { + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("23/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result), this->precision())); + } } } \ No newline at end of file diff --git a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp new file mode 100644 index 000000000..4bbf93b75 --- /dev/null +++ b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp @@ -0,0 +1,264 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "test/storm_gtest.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/MarkovAutomaton.h" +#include "storm/models/symbolic/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/logic/Formulas.h" +#include "storm/storage/jani/Property.h" +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace { + class SparseDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::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 + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().minMax().setRelativeTerminationCriterion(false); + return env; + } + }; + class SparseRationalPolicyIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + return env; + } + }; + class SparseRationalRationalSearchEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); + return env; + } + }; + + template + class MarkovAutomatonCslModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::MarkovAutomaton SparseModelType; + typedef typename storm::models::symbolic::MarkovAutomaton SymbolicModelType; + + MarkovAutomatonCslModelCheckerTest() : _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; } + + 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); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, 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); + 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(); + 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 == storm::settings::modules::CoreSettings::Engine::Sparse) { + return std::make_shared>(*model); + } + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + return std::make_shared>(*model); + } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { + return std::make_shared>(*model); + } + } + + 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< + SparseDoubleValueIterationEnvironment, + SparseDoubleIntervalIterationEnvironment, + SparseRationalPolicyIterationEnvironment, + SparseRationalRationalSearchEnvironment, + > TestingTypes; + + TYPED_TEST_CASE(MarkovAutomatonCslModelCheckerTest, TestingTypes); + + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, server) { + std::string formulasString = "Tmax=? [F \"error\"]"; + formulasString += "; Pmax=? [F \"processB\"]"; + formulasString += "; Pmax=? [F<1 \"error\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/server.ma", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(6ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("11/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("2/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.455504"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + } + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple) { + std::string formulasString = "Pmin=? [F<1 s>2]"; + formulasString += "; Pmax=? [F<1.3 s=3]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple.ma", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.6321205588"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("0.727468207"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple2) { + std::string formulasString = "R{\"rew0\"}max=? [C]"; + formulasString += "; R{\"rew0\"}min=? [C]"; + formulasString += "; R{\"rew1\"}max=? [C]"; + formulasString += "; R{\"rew1\"}min=? [C]"; + formulasString += "; R{\"rew2\"}max=? [C]"; + formulasString += "; R{\"rew2\"}min=? [C]"; + formulasString += "; R{\"rew3\"}min=? [C]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple2.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); + 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]); + 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))); + + } +} \ No newline at end of file