Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExplicitDtmcPrctlModelCheckerTest.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/AutoParser.h"
5#include "storm-parsers/parser/FormulaParser.h"
6#include "storm-parsers/parser/PrismParser.h"
7#include "storm/builder/ExplicitModelBuilder.h"
8#include "storm/environment/solver/SolverEnvironment.h"
9#include "storm/logic/Formulas.h"
10#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
11#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
12#include "storm/models/sparse/StandardRewardModel.h"
13#include "storm/settings/SettingsManager.h"
14#include "storm/settings/modules/GeneralSettings.h"
15#include "storm/storage/expressions/ExpressionManager.h"
16
17TEST(ExplicitDtmcPrctlModelCheckerTest, Die) {
18 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(
19 STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew");
20
21 storm::Environment env;
22 double const precision = 1e-6;
23 // Increase precision a little to get more accurate results
24 env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
25
26 // A parser that we use for conveniently constructing the formulas.
27
28 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
29 storm::parser::FormulaParser formulaParser(expManager);
30
31 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
32
33 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
34
35 ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
36 ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
37
38 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
39
40 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
41
42 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
43 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
44
45 EXPECT_NEAR(1.0 / 6.0, quantitativeResult1[0], precision);
46
47 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
48
49 result = checker.check(env, *formula);
50 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
51
52 EXPECT_NEAR(1.0 / 6.0, quantitativeResult2[0], precision);
53
54 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
55
56 result = checker.check(env, *formula);
57 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
58
59 EXPECT_NEAR(1.0 / 6.0, quantitativeResult3[0], precision);
60
61 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
62
63 result = checker.check(env, *formula);
64 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
65
66 EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], precision);
67}
68
69TEST(ExplicitDtmcPrctlModelCheckerTest, Crowds) {
70 storm::Environment env;
71 double const precision = 1e-6;
72 // Increase precision a little to get more accurate results
73 env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
74
75 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
76 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", "");
77
78 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
79
80 // A parser that we use for conveniently constructing the formulas.
81
82 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
83 storm::parser::FormulaParser formulaParser(expManager);
84
85 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
86
87 ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
88 ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
89
90 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
91
92 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
93
94 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
95 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
96
97 EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], precision);
98
99 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
100
101 result = checker.check(env, *formula);
102 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
103
104 EXPECT_NEAR(0.1522194965, quantitativeResult2[0], precision);
105
106 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
107
108 result = checker.check(env, *formula);
109 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
110
111 EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], precision);
112}
113
114TEST(ExplicitDtmcPrctlModelCheckerTest, SynchronousLeader) {
115 storm::Environment env;
116 double const precision = 1e-6;
117 // Increase precision a little to get more accurate results
118 env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
119
120 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
121 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4_8.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4_8.lab", "",
122 STORM_TEST_RESOURCES_DIR "/rew/leader4_8.pick.trans.rew");
123
124 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
125
126 // A parser that we use for conveniently constructing the formulas.
127
128 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
129 storm::parser::FormulaParser formulaParser(expManager);
130
131 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
132
133 ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
134 ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
135
136 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
137
138 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
139
140 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
141 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
142
143 EXPECT_NEAR(1.0, quantitativeResult1[0], precision);
144
145 formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
146
147 result = checker.check(env, *formula);
148 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
149
150 EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], precision);
151
152 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
153
154 result = checker.check(env, *formula);
155 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
156
157 EXPECT_NEAR(1.0448979591836789, quantitativeResult3[0], precision);
158}
TEST
TEST(ExplicitDtmcPrctlModelCheckerTest, Die)
Definition ExplicitDtmcPrctlModelCheckerTest.cpp:17
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:26
storm::SolverEnvironment::setLinearEquationSolverPrecision
void setLinearEquationSolverPrecision(boost::optional< storm::RationalNumber > const &newPrecision, boost::optional< bool > const &relativePrecision=boost::none)
Definition SolverEnvironment.cpp:211
storm::modelchecker::AbstractModelChecker::check
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
Definition AbstractModelChecker.cpp:49
storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
Definition CheckResult.cpp:94
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::parser::AutoParser::parseModel
static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel(std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="", ExplicitModelParserOptions const &options=ExplicitModelParserOptions())
Checks the given files and parses the model within these files.
Definition AutoParser.cpp:20
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::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:143
storm_gtest.h