Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DeterministicModelBisimulationDecompositionTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm-parsers/parser/AutoParser.h"
3#include "storm-parsers/parser/FormulaParser.h"
4#include "storm/models/sparse/Dtmc.h"
5#include "storm/models/sparse/StandardRewardModel.h"
6#include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
7#include "test/storm_gtest.h"
8
9TEST(DeterministicModelBisimulationDecomposition, Die) {
10 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
11 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", "");
12
13 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
14 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
15
16 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim(*dtmc);
17 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
18 std::shared_ptr<storm::models::sparse::Model<double>> result;
19 ASSERT_NO_THROW(result = bisim.getQuotient());
20
21 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
22 EXPECT_EQ(13ul, result->getNumberOfStates());
23 EXPECT_EQ(20ul, result->getNumberOfTransitions());
24
25#ifdef WINDOWS
26 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options;
27#else
28 typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options;
29#endif
30 options.respectedAtomicPropositions = std::set<std::string>({"one"});
31
32 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim2(*dtmc, options);
33 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
34 ASSERT_NO_THROW(result = bisim2.getQuotient());
35
36 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
37 EXPECT_EQ(5ul, result->getNumberOfStates());
38 EXPECT_EQ(8ul, result->getNumberOfTransitions());
39
40 options.setType(storm::storage::BisimulationType::Weak);
41
42 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
43 ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
44 ASSERT_NO_THROW(result = bisim3.getQuotient());
45
46 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
47 EXPECT_EQ(5ul, result->getNumberOfStates());
48 EXPECT_EQ(8ul, result->getNumberOfTransitions());
49
50 storm::parser::FormulaParser formulaParser;
51 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
52
53 typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options2(*dtmc, *formula);
54
55 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim4(*dtmc, options2);
56 ASSERT_NO_THROW(bisim4.computeBisimulationDecomposition());
57 ASSERT_NO_THROW(result = bisim4.getQuotient());
58 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
59 EXPECT_EQ(5ul, result->getNumberOfStates());
60 EXPECT_EQ(8ul, result->getNumberOfTransitions());
61}
62
63TEST(DeterministicModelBisimulationDecomposition, Crowds) {
64 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
65 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", "");
66
67 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
68 std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
69
70 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim(*dtmc);
71 std::shared_ptr<storm::models::sparse::Model<double>> result;
72 ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
73 ASSERT_NO_THROW(result = bisim.getQuotient());
74
75 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
76 EXPECT_EQ(334ul, result->getNumberOfStates());
77 EXPECT_EQ(546ul, result->getNumberOfTransitions());
78
79#ifdef WINDOWS
80 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options;
81#else
82 typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options;
83#endif
84 options.respectedAtomicPropositions = std::set<std::string>({"observe0Greater1"});
85
86 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim2(*dtmc, options);
87 ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
88 ASSERT_NO_THROW(result = bisim2.getQuotient());
89
90 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
91 EXPECT_EQ(65ul, result->getNumberOfStates());
92 EXPECT_EQ(105ul, result->getNumberOfTransitions());
93
94 options.setType(storm::storage::BisimulationType::Weak);
95
96 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim3(*dtmc, options);
97 ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
98 ASSERT_NO_THROW(result = bisim3.getQuotient());
99
100 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
101 EXPECT_EQ(43ul, result->getNumberOfStates());
102 EXPECT_EQ(83ul, result->getNumberOfTransitions());
103
104 storm::parser::FormulaParser formulaParser;
105 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
106
107 typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options3(*dtmc, *formula);
108
109 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim5(*dtmc, options3);
110 ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition());
111 ASSERT_NO_THROW(result = bisim5.getQuotient());
112
113 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
114 EXPECT_EQ(64ul, result->getNumberOfStates());
115 EXPECT_EQ(104ul, result->getNumberOfTransitions());
116
117 formula = formulaParser.parseSingleFormulaFromString("P=? [true U<=50 \"observe0Greater1\"] ");
118
119 typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>::Options options4(*dtmc, *formula);
120
121 storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>> bisim6(*dtmc, options4);
122 ASSERT_NO_THROW(bisim6.computeBisimulationDecomposition());
123 ASSERT_NO_THROW(result = bisim6.getQuotient());
124
125 EXPECT_EQ(storm::models::ModelType::Dtmc, result->getType());
126 EXPECT_EQ(65ul, result->getNumberOfStates());
127 EXPECT_EQ(105ul, result->getNumberOfTransitions());
128}
TEST
TEST(DeterministicModelBisimulationDecomposition, Die)
Definition DeterministicModelBisimulationDecompositionTest.cpp:9
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::storage::BisimulationDecomposition::getQuotient
std::shared_ptr< ModelType > getQuotient() const
Retrieves the quotient of the model under the computed bisimulation.
Definition BisimulationDecomposition.cpp:292
storm::storage::BisimulationDecomposition::computeBisimulationDecomposition
void computeBisimulationDecomposition()
Computes the decomposition of the model into bisimulation equivalence classes.
Definition BisimulationDecomposition.cpp:208
storm::storage::DeterministicModelBisimulationDecomposition
This class represents the decomposition of a deterministic model into its bisimulation quotient.
Definition DeterministicModelBisimulationDecomposition.h:14
storm_gtest.h