Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MaximalEndComponentDecompositionTest.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/PrismParser.h"
6#include "storm/builder/ExplicitModelBuilder.h"
7#include "storm/models/sparse/MarkovAutomaton.h"
8#include "storm/models/sparse/Mdp.h"
9#include "storm/models/sparse/StandardRewardModel.h"
10#include "storm/storage/MaximalEndComponentDecomposition.h"
11#include "storm/storage/SymbolicModelDescription.h"
12
13TEST(MaximalEndComponentDecomposition, FullSystem1) {
14 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
15 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", "");
16
17 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::sparse::MarkovAutomaton<double>>();
18
19 storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
20 ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));
21
22 ASSERT_EQ(2ul, mecDecomposition.size());
23
24 // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way.
25 storm::storage::MaximalEndComponent const& mec1 = mecDecomposition[0];
26 if (mec1.containsState(3)) {
27 ASSERT_TRUE(mec1.containsState(8));
28 ASSERT_TRUE(mec1.containsState(9));
29 ASSERT_TRUE(mec1.containsState(10));
30 ASSERT_FALSE(mec1.containsState(0));
31 ASSERT_FALSE(mec1.containsState(1));
32 ASSERT_FALSE(mec1.containsState(2));
33 ASSERT_FALSE(mec1.containsState(4));
34 ASSERT_FALSE(mec1.containsState(5));
35 ASSERT_FALSE(mec1.containsState(6));
36 ASSERT_FALSE(mec1.containsState(7));
37 } else if (mec1.containsState(4)) {
38 ASSERT_TRUE(mec1.containsState(5));
39 ASSERT_TRUE(mec1.containsState(6));
40 ASSERT_TRUE(mec1.containsState(7));
41 ASSERT_FALSE(mec1.containsState(0));
42 ASSERT_FALSE(mec1.containsState(1));
43 ASSERT_FALSE(mec1.containsState(2));
44 ASSERT_FALSE(mec1.containsState(3));
45 ASSERT_FALSE(mec1.containsState(8));
46 ASSERT_FALSE(mec1.containsState(9));
47 ASSERT_FALSE(mec1.containsState(10));
48 } else {
49 // This case must never happen as the only two existing MECs contain either 3 or 4.
50 ASSERT_TRUE(false);
51 }
52
53 storm::storage::MaximalEndComponent const& mec2 = mecDecomposition[1];
54 if (mec2.containsState(3)) {
55 ASSERT_TRUE(mec2.containsState(8));
56 ASSERT_TRUE(mec2.containsState(9));
57 ASSERT_TRUE(mec2.containsState(10));
58 ASSERT_FALSE(mec2.containsState(0));
59 ASSERT_FALSE(mec2.containsState(1));
60 ASSERT_FALSE(mec2.containsState(2));
61 ASSERT_FALSE(mec2.containsState(4));
62 ASSERT_FALSE(mec2.containsState(5));
63 ASSERT_FALSE(mec2.containsState(6));
64 ASSERT_FALSE(mec2.containsState(7));
65 } else if (mec2.containsState(4)) {
66 ASSERT_TRUE(mec2.containsState(5));
67 ASSERT_TRUE(mec2.containsState(6));
68 ASSERT_TRUE(mec2.containsState(7));
69 ASSERT_FALSE(mec2.containsState(0));
70 ASSERT_FALSE(mec2.containsState(1));
71 ASSERT_FALSE(mec2.containsState(2));
72 ASSERT_FALSE(mec2.containsState(3));
73 ASSERT_FALSE(mec2.containsState(8));
74 ASSERT_FALSE(mec2.containsState(9));
75 ASSERT_FALSE(mec2.containsState(10));
76 } else {
77 // This case must never happen as the only two existing MECs contain either 3 or 4.
78 ASSERT_TRUE(false);
79 }
80}
81
82TEST(MaximalEndComponentDecomposition, FullSystem2) {
83 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
84 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny2.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny2.lab", "", "");
85
86 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::sparse::MarkovAutomaton<double>>();
87
88 storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
89 ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));
90
91 ASSERT_EQ(1ul, mecDecomposition.size());
92
93 // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way.
94 storm::storage::MaximalEndComponent const& mec1 = mecDecomposition[0];
95 if (mec1.containsState(4)) {
96 ASSERT_TRUE(mec1.containsState(5));
97 ASSERT_TRUE(mec1.containsState(6));
98 ASSERT_TRUE(mec1.containsState(7));
99 ASSERT_FALSE(mec1.containsState(0));
100 ASSERT_FALSE(mec1.containsState(1));
101 ASSERT_FALSE(mec1.containsState(2));
102 ASSERT_FALSE(mec1.containsState(3));
103 ASSERT_FALSE(mec1.containsState(8));
104 ASSERT_FALSE(mec1.containsState(9));
105 ASSERT_FALSE(mec1.containsState(10));
106 } else {
107 // This case must never happen as the only two existing MECs contain 4.
108 ASSERT_TRUE(false);
109 }
110}
111
112TEST(MaximalEndComponentDecomposition, Subsystem) {
113 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
114 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", "");
115
116 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::sparse::MarkovAutomaton<double>>();
117
118 storm::storage::BitVector subsystem(markovAutomaton->getNumberOfStates(), true);
119 subsystem.set(7, false);
120
121 storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
122 ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton, subsystem));
123
124 ASSERT_EQ(1ul, mecDecomposition.size());
125
126 storm::storage::MaximalEndComponent const& mec1 = mecDecomposition[0];
127
128 if (mec1.containsState(3)) {
129 ASSERT_TRUE(mec1.containsState(8));
130 ASSERT_TRUE(mec1.containsState(9));
131 ASSERT_TRUE(mec1.containsState(10));
132 ASSERT_FALSE(mec1.containsState(0));
133 ASSERT_FALSE(mec1.containsState(1));
134 ASSERT_FALSE(mec1.containsState(2));
135 ASSERT_FALSE(mec1.containsState(4));
136 ASSERT_FALSE(mec1.containsState(5));
137 ASSERT_FALSE(mec1.containsState(6));
138 ASSERT_FALSE(mec1.containsState(7));
139 } else {
140 // This case must never happen as the only two existing MEC contains 3.
141 ASSERT_TRUE(false);
142 }
143}
144
145TEST(MaximalEndComponentDecomposition, Example1) {
146#ifndef STORM_HAVE_Z3
147 GTEST_SKIP() << "Z3 not available.";
148#endif
149 std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm";
150 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath);
151 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
152
153 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
154 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
155
156 storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(*mdp);
157
158 EXPECT_EQ(2ull, mecDecomposition.size());
159
160 ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2});
161 EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{3});
162
163 ASSERT_TRUE(mecDecomposition[1].getStateSet() == storm::storage::MaximalEndComponent::set_type{0});
164 EXPECT_TRUE(mecDecomposition[1].getChoicesForState(0) == storm::storage::MaximalEndComponent::set_type{0});
165}
166
167TEST(MaximalEndComponentDecomposition, Example2) {
168#ifndef STORM_HAVE_Z3
169 GTEST_SKIP() << "Z3 not available.";
170#endif
171 std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example2.nm";
172 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath);
173 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
174
175 std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
176 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
177
178 storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(*mdp);
179
180 EXPECT_EQ(2ull, mecDecomposition.size());
181
182 ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2});
183 EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{4});
184
185 ASSERT_TRUE((mecDecomposition[1].getStateSet() == storm::storage::MaximalEndComponent::set_type{0, 1}));
186 EXPECT_TRUE((mecDecomposition[1].getChoicesForState(0) == storm::storage::MaximalEndComponent::set_type{0, 1}));
187 EXPECT_TRUE((mecDecomposition[1].getChoicesForState(1) == storm::storage::MaximalEndComponent::set_type{3}));
188}
TEST
TEST(MaximalEndComponentDecomposition, FullSystem1)
Definition MaximalEndComponentDecompositionTest.cpp:13
storm::builder::ExplicitModelBuilder::build
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
Definition ExplicitModelBuilder.cpp:92
storm::models::sparse::MarkovAutomaton
This class represents a Markov automaton.
Definition MarkovAutomaton.h:14
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.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::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::storage::Decomposition::size
std::size_t size() const
Retrieves the number of blocks of this decomposition.
Definition Decomposition.cpp:40
storm::storage::MaximalEndComponentDecomposition
This class represents the decomposition of a nondeterministic model into its maximal end components.
Definition MaximalEndComponentDecomposition.h:16
storm::storage::MaximalEndComponent
This class represents a maximal end-component of a nondeterministic model.
Definition MaximalEndComponent.h:17
storm::storage::MaximalEndComponent::set_type
storm::storage::FlatSet< sparse::state_type > set_type
Definition MaximalEndComponent.h:19
storm::storage::MaximalEndComponent::containsState
bool containsState(uint_fast64_t state) const
Retrieves whether the given state is contained in this MEC.
Definition MaximalEndComponent.cpp:74
storm::storage::SymbolicModelDescription::asPrismProgram
storm::prism::Program const & asPrismProgram() const
Definition SymbolicModelDescription.cpp:112
storm::storage::SymbolicModelDescription::preprocess
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
Definition SymbolicModelDescription.cpp:162
storm_gtest.h