From 66d1c828c647a9869d9e6a04cd6672f17d3ab7fa Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 23 Nov 2017 21:49:07 +0100 Subject: [PATCH] added parametric model checking tests --- .../ParametricDtmcPrctlModelCheckerTest.cpp | 106 ++++++++++++++++++ ...licParametricDtmcPrctlModelCheckerTest.cpp | 76 +++++++++++++ 2 files changed, 182 insertions(+) create mode 100644 src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp create mode 100644 src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp diff --git a/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..cf30285c5 --- /dev/null +++ b/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,106 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/parser/AutoParser.h" +#include "storm/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm/environment/solver/SolverEnvironment.h" +namespace { + + class EigenEnvironment { + public: + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); + return env; + } + }; + + class EliminationEnvironment { + public: + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination); + return env; + } + }; + + template + class ParametricDtmcPrctlModelCheckerTest : public ::testing::Test { + public: + ParametricDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + storm::RationalFunctionCoefficient parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + EigenEnvironment, + EliminationEnvironment + > TestingTypes; + + TYPED_TEST_CASE(ParametricDtmcPrctlModelCheckerTest, TestingTypes); + TYPED_TEST(ParametricDtmcPrctlModelCheckerTest, Die) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm"); + storm::generator::NextStateGeneratorOptions options; + options.setBuildAllLabels().setBuildAllRewardModels(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); + + // A parser that we use for conveniently constructing the formulas. + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); + + std::map instantiation; + std::set variables = storm::models::sparse::getProbabilityParameters(*dtmc); + ASSERT_EQ(variables.size(), 1ull); + instantiation.emplace(*variables.begin(), this->parseNumber("1/2")); + + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult1[0].evaluate(instantiation)); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult2[0].evaluate(instantiation)); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult3[0].evaluate(instantiation)); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_EQ(this->parseNumber("11/3"), quantitativeResult4[0].evaluate(instantiation)); + } +} diff --git a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..31c5d7436 --- /dev/null +++ b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,76 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/utility/solver.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "storm/solver/SymbolicEliminationLinearEquationSolver.h" +#include "storm/parser/PrismParser.h" +#include "storm/builder/DdPrismModelBuilder.h" +#include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/models/symbolic/Dtmc.h" +#include "storm/settings/SettingsManager.h" + +#include "storm/environment/solver/SolverEnvironment.h" + +TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm"); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + // Build the die model with its reward model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("coin_flips"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::map instantiation; + std::set variables = model->getParameters(); + ASSERT_EQ(1ull, variables.size()); + instantiation.emplace(*variables.begin(), storm::utility::convertNumber(std::string("1/2"))); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult1.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult2.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult3.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("1/6"))); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_EQ(storm::utility::convertNumber(quantitativeResult4.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("11/3"))); +}