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