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