Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SymbolicParametricDtmcPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-pars/utility/parametric.h"
5#include "storm-parsers/parser/FormulaParser.h"
6#include "storm-parsers/parser/PrismParser.h"
7#include "storm/adapters/RationalFunctionAdapter.h"
8#include "storm/builder/DdPrismModelBuilder.h"
9#include "storm/logic/Formulas.h"
10#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
11#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
12#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
13#include "storm/models/symbolic/Dtmc.h"
14#include "storm/storage/SymbolicModelDescription.h"
15
16TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
17#ifdef STORM_HAVE_SYLVAN
18 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
19 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
20
21 // A parser that we use for conveniently constructing the formulas.
22 storm::parser::FormulaParser formulaParser;
23
24 // Build the die model with its reward model.
25 typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>::Options options;
26 options.buildAllRewardModels = false;
27 options.rewardModelsToBuild.insert("coin_flips");
28 std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> model =
29 storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>().build(program, options);
30 EXPECT_EQ(13ul, model->getNumberOfStates());
31 EXPECT_EQ(20ul, model->getNumberOfTransitions());
32 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
33
34 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
35 std::set<storm::RationalFunctionVariable> variables = model->getParameters();
36 ASSERT_EQ(1ull, variables.size());
37 instantiation.emplace(*variables.begin(), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/2")));
38
39 std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> dtmc =
40 model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>();
41
42 storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> checker(*dtmc);
43
44 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
45
46 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
47 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
48 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult1 =
49 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
50
51 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult1.sum(), instantiation),
52 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
53
54 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
55
56 result = checker.check(*formula);
57 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
58 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult2 =
59 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
60
61 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult2.sum(), instantiation),
62 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
63
64 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
65
66 result = checker.check(*formula);
67 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
68 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult3 =
69 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
70
71 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult3.sum(), instantiation),
72 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
73
74 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
75
76 result = checker.check(*formula);
77 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
78 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult4 =
79 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
80
81 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult4.sum(), instantiation),
82 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("11/3")));
83#else
84 GTEST_SKIP() << "Library Sylvan not available.";
85#endif
86}
TEST
TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan)
Definition SymbolicParametricDtmcPrctlModelCheckerTest.cpp:16
storm::builder::DdPrismModelBuilder::build
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > build(storm::prism::Program const &program, Options const &options=Options())
Translates the given program into a symbolic model (i.e.
Definition DdPrismModelBuilder.cpp:1573
storm::modelchecker::CheckResult::asSymbolicQuantitativeCheckResult
SymbolicQuantitativeCheckResult< Type, ValueType > & asSymbolicQuantitativeCheckResult()
Definition CheckResult.cpp:147
storm::models::symbolic::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::parser::FormulaParser::parseSingleFormulaFromString
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
Definition FormulaParser.cpp:55
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::storage::SymbolicModelDescription::asPrismProgram
storm::prism::Program const & asPrismProgram() const
Definition SymbolicModelDescription.cpp:112
storm::storage::SymbolicModelDescription::preprocess
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
Definition SymbolicModelDescription.cpp:162
storm_gtest.h