Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseDtmcEliminationModelCheckerTest.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/logic/Formulas.h"
6#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
7#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
8#include "storm/models/sparse/StandardRewardModel.h"
9#include "storm/settings/SettingsManager.h"
10
11#include "storm-parsers/parser/AutoParser.h"
12#include "storm/settings/SettingMemento.h"
13#include "storm/settings/modules/GeneralSettings.h"
14
15TEST(SparseDtmcEliminationModelCheckerTest, Die) {
16 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(
17 STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew");
18
19 // A parser that we use for conveniently constructing the formulas.
20 storm::parser::FormulaParser formulaParser;
21
22 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
23
24 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
25
26 ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
27 ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
28
29 storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
30
31 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
32
33 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
34 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
35
36 EXPECT_NEAR(1.0 / 6.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
37
38 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
39
40 result = checker.check(*formula);
41 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
42
43 EXPECT_NEAR(1.0 / 6.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
44
45 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
46
47 result = checker.check(*formula);
48 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
49
50 EXPECT_NEAR(1.0 / 6.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
51
52 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
53
54 result = checker.check(*formula);
55 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
56
57 EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
58}
59
60TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
61 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
62 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", "");
63
64 // A parser that we use for conveniently constructing the formulas.
65 storm::parser::FormulaParser formulaParser;
66
67 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
68
69 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
70
71 ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
72 ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
73
74 storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
75
76 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
77
78 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
79 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
80
81 EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
82
83 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
84
85 result = checker.check(*formula);
86 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
87
88 EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
89
90 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
91
92 result = checker.check(*formula);
93 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
94
95 EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
96
97 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]");
98
99 result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formula).setOnlyInitialStatesRelevant(true));
100 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
101
102 EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
103
104 formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]");
105
106 result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formula).setOnlyInitialStatesRelevant(true));
107 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
108
109 EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
110}
111
112TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
113 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
114 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4_8.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4_8.lab", "",
115 STORM_TEST_RESOURCES_DIR "/rew/leader4_8.pick.trans.rew");
116
117 // A parser that we use for conveniently constructing the formulas.
118 storm::parser::FormulaParser formulaParser;
119
120 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
121 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
122
123 ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
124 ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
125
126 storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
127
128 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
129
130 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
131 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
132
133 EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
134
135 formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
136
137 result = checker.check(*formula);
138 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
139
140 EXPECT_NEAR(1.0448979, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
141}
TEST
TEST(SparseDtmcEliminationModelCheckerTest, Die)
Definition SparseDtmcEliminationModelCheckerTest.cpp:15
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::modelchecker::CheckTask::setOnlyInitialStatesRelevant
CheckTask< FormulaType, ValueType > & setOnlyInitialStatesRelevant(bool value=true)
Sets whether only initial states are relevant.
Definition CheckTask.h:211
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