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