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