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