Storm 1.14.0.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 "storm/environment/Environment.h"
3#include "test/storm_gtest.h"
4
5#include "storm-pars/utility/parametric.h"
6#include "storm-parsers/parser/FormulaParser.h"
7#include "storm-parsers/parser/PrismParser.h"
8#include "storm/adapters/RationalFunctionAdapter.h"
9#include "storm/builder/DdPrismModelBuilder.h"
10#include "storm/logic/Formulas.h"
11#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
12#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
13#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
14#include "storm/models/symbolic/Dtmc.h"
15#include "storm/storage/SymbolicModelDescription.h"
16
17TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
18#ifdef STORM_HAVE_SYLVAN
19 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
20 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
21
22 // A parser that we use for conveniently constructing the formulas.
23 storm::parser::FormulaParser formulaParser;
24
25 // Build the die model with its reward model.
26 typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>::Options options;
27 options.buildAllRewardModels = false;
28 options.rewardModelsToBuild.insert("coin_flips");
29 std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> model =
30 storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>().build(storm::Environment(), program, options);
31 EXPECT_EQ(13ul, model->getNumberOfStates());
32 EXPECT_EQ(20ul, model->getNumberOfTransitions());
33 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
34
35 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
36 std::set<storm::RationalFunctionVariable> variables = model->getParameters();
37 ASSERT_EQ(1ull, variables.size());
38 instantiation.emplace(*variables.begin(), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/2")));
39
40 std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> dtmc =
41 model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>();
42
43 storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> checker(*dtmc);
44
45 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
46
47 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
48 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
49 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult1 =
50 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
51
52 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult1.sum(), instantiation),
53 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
54
55 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
56
57 result = checker.check(*formula);
58 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
59 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult2 =
60 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
61
62 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult2.sum(), instantiation),
63 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
64
65 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
66
67 result = checker.check(*formula);
68 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
69 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult3 =
70 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
71
72 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult3.sum(), instantiation),
73 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
74
75 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
76
77 result = checker.check(*formula);
78 result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
79 storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>& quantitativeResult4 =
80 result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
81
82 EXPECT_EQ(storm::utility::parametric::evaluate<storm::RationalFunctionCoefficient>(quantitativeResult4.sum(), instantiation),
83 storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("11/3")));
84#else
85 GTEST_SKIP() << "Library Sylvan not available.";
86#endif
87}
TEST
TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan)
Definition SymbolicParametricDtmcPrctlModelCheckerTest.cpp:17
storm::builder::DdPrismModelBuilder::build
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > build(storm::Environment const &env, storm::prism::Program const &program, Options const &options=Options())
Translates the given program into a symbolic model (i.e.
Definition DdPrismModelBuilder.cpp:1565
storm::modelchecker::CheckResult::asSymbolicQuantitativeCheckResult
SymbolicQuantitativeCheckResult< Type, ValueType > & asSymbolicQuantitativeCheckResult()
Definition CheckResult.cpp:156
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::utility::parametric::evaluate
double evaluate(storm::RationalFunction const &function, Valuation< storm::RationalFunction > const &valuation)
Definition parametric.cpp:21
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:143
storm::RationalFunction
carl::RationalFunction< Polynomial, true > RationalFunction
Definition RationalFunctionForward.h:41
storm_gtest.h