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