Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MarkovAutomatonSparseTransitionParserTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include <vector>
5
6#include "storm-parsers/parser/MarkovAutomatonParser.h"
7#include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h"
8#include "storm-parsers/util/cstring.h"
9#include "storm/exceptions/FileIoException.h"
10#include "storm/exceptions/WrongFormatException.h"
11#include "storm/settings/SettingMemento.h"
12#include "storm/settings/SettingsManager.h"
13#include "storm/settings/modules/BuildSettings.h"
14
15TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile) {
16 // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
17 STORM_SILENT_ASSERT_THROW(
18 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"),
19 storm::exceptions::FileIoException);
20}
21
22TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
23 // The file that will be used for the test.
24 std::string filename = STORM_TEST_RESOURCES_DIR "/tra/ma_general.tra";
25
26 // Execute the parser.
27 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
28 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
29
30 // Build the actual transition matrix.
31 storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0, 0));
32
33 // Test all sizes and counts.
34 ASSERT_EQ(6ul, transitionMatrix.getColumnCount());
35 ASSERT_EQ(7ul, transitionMatrix.getRowCount());
36 ASSERT_EQ(12ul, transitionMatrix.getEntryCount());
37 ASSERT_EQ(6ul, transitionMatrix.getRowGroupCount());
38 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices().size());
39 ASSERT_EQ(7ul, result.markovianChoices.size());
40 ASSERT_EQ(6ul, result.markovianStates.size());
41 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
42 ASSERT_EQ(6ul, result.exitRates.size());
43
44 // Test the general structure of the transition system (that will be an Markov automaton).
45
46 // Test the mapping between states and transition matrix rows.
47 ASSERT_EQ(0ul, transitionMatrix.getRowGroupIndices()[0]);
48 ASSERT_EQ(1ul, transitionMatrix.getRowGroupIndices()[1]);
49 ASSERT_EQ(2ul, transitionMatrix.getRowGroupIndices()[2]);
50 ASSERT_EQ(3ul, transitionMatrix.getRowGroupIndices()[3]);
51 ASSERT_EQ(4ul, transitionMatrix.getRowGroupIndices()[4]);
52 ASSERT_EQ(6ul, transitionMatrix.getRowGroupIndices()[5]);
53 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices()[6]);
54
55 // Test the Markovian states.
56 ASSERT_TRUE(result.markovianStates.get(0));
57 ASSERT_FALSE(result.markovianStates.get(1));
58 ASSERT_TRUE(result.markovianStates.get(2));
59 ASSERT_FALSE(result.markovianStates.get(3));
60 ASSERT_FALSE(result.markovianStates.get(4));
61 ASSERT_FALSE(result.markovianStates.get(5));
62
63 // Test the exit rates. These have to be 0 for all non-Markovian states.
64 ASSERT_EQ(2, result.exitRates[0]);
65 ASSERT_EQ(0, result.exitRates[1]);
66 ASSERT_EQ(15, result.exitRates[2]);
67 ASSERT_EQ(0, result.exitRates[3]);
68 ASSERT_EQ(0, result.exitRates[4]);
69 ASSERT_EQ(0, result.exitRates[5]);
70
71 // Finally, test the transition matrix itself.
72 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
73
74 ASSERT_EQ(2, cIter->getValue());
75 cIter++;
76 ASSERT_EQ(1, cIter->getValue());
77 cIter++;
78 ASSERT_EQ(1, cIter->getValue());
79 cIter++;
80 ASSERT_EQ(2, cIter->getValue());
81 cIter++;
82 ASSERT_EQ(4, cIter->getValue());
83 cIter++;
84 ASSERT_EQ(8, cIter->getValue());
85 cIter++;
86 ASSERT_EQ(0.5, cIter->getValue());
87 cIter++;
88 ASSERT_EQ(0.5, cIter->getValue());
89 cIter++;
90 ASSERT_EQ(1, cIter->getValue());
91 cIter++;
92 ASSERT_EQ(0.5, cIter->getValue());
93 cIter++;
94 ASSERT_EQ(0.5, cIter->getValue());
95 cIter++;
96 ASSERT_EQ(1, cIter->getValue());
97 cIter++;
98 ASSERT_EQ(transitionMatrix.end(), cIter);
99}
100
101TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
102 // The file that will be used for the test.
103 std::string filename = STORM_TEST_RESOURCES_DIR "/tra/ma_whitespaces.tra";
104
105 // Execute the parser.
106 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
107 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
108
109 // Build the actual transition matrix.
110 storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build());
111
112 // Test all sizes and counts.
113 ASSERT_EQ(6ul, transitionMatrix.getColumnCount());
114 ASSERT_EQ(7ul, transitionMatrix.getRowCount());
115 ASSERT_EQ(12ul, transitionMatrix.getEntryCount());
116 ASSERT_EQ(6ul, transitionMatrix.getRowGroupCount());
117 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices().size());
118 ASSERT_EQ(7ul, result.markovianChoices.size());
119 ASSERT_EQ(6ul, result.markovianStates.size());
120 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
121 ASSERT_EQ(6ul, result.exitRates.size());
122
123 // Test the general structure of the transition system (that will be an Markov automaton).
124
125 // Test the mapping between states and transition matrix rows.
126 ASSERT_EQ(0ul, transitionMatrix.getRowGroupIndices()[0]);
127 ASSERT_EQ(1ul, transitionMatrix.getRowGroupIndices()[1]);
128 ASSERT_EQ(2ul, transitionMatrix.getRowGroupIndices()[2]);
129 ASSERT_EQ(3ul, transitionMatrix.getRowGroupIndices()[3]);
130 ASSERT_EQ(4ul, transitionMatrix.getRowGroupIndices()[4]);
131 ASSERT_EQ(6ul, transitionMatrix.getRowGroupIndices()[5]);
132 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices()[6]);
133
134 // Test the Markovian states.
135 ASSERT_TRUE(result.markovianStates.get(0));
136 ASSERT_FALSE(result.markovianStates.get(1));
137 ASSERT_TRUE(result.markovianStates.get(2));
138 ASSERT_FALSE(result.markovianStates.get(3));
139 ASSERT_FALSE(result.markovianStates.get(4));
140 ASSERT_FALSE(result.markovianStates.get(5));
141
142 // Test the exit rates. These have to be 0 for all non-Markovian states.
143 ASSERT_EQ(2, result.exitRates[0]);
144 ASSERT_EQ(0, result.exitRates[1]);
145 ASSERT_EQ(15, result.exitRates[2]);
146 ASSERT_EQ(0, result.exitRates[3]);
147 ASSERT_EQ(0, result.exitRates[4]);
148 ASSERT_EQ(0, result.exitRates[5]);
149
150 // Finally, test the transition matrix itself.
151 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
152
153 ASSERT_EQ(2, cIter->getValue());
154 cIter++;
155 ASSERT_EQ(1, cIter->getValue());
156 cIter++;
157 ASSERT_EQ(1, cIter->getValue());
158 cIter++;
159 ASSERT_EQ(2, cIter->getValue());
160 cIter++;
161 ASSERT_EQ(4, cIter->getValue());
162 cIter++;
163 ASSERT_EQ(8, cIter->getValue());
164 cIter++;
165 ASSERT_EQ(0.5, cIter->getValue());
166 cIter++;
167 ASSERT_EQ(0.5, cIter->getValue());
168 cIter++;
169 ASSERT_EQ(1, cIter->getValue());
170 cIter++;
171 ASSERT_EQ(0.5, cIter->getValue());
172 cIter++;
173 ASSERT_EQ(0.5, cIter->getValue());
174 cIter++;
175 ASSERT_EQ(1, cIter->getValue());
176 cIter++;
177 ASSERT_EQ(transitionMatrix.end(), cIter);
178}
179
180TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
181 // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
182 std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(false);
183
184 // Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works.
185 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
186 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra");
187
188 // Test if the result is consistent with the parsed Markov Automaton.
189 storm::storage::SparseMatrix<double> resultMatrix(result.transitionMatrixBuilder.build());
190 ASSERT_EQ(7ul, resultMatrix.getColumnCount());
191 ASSERT_EQ(13ul, resultMatrix.getEntryCount());
192 ASSERT_EQ(7ul, resultMatrix.getRowGroupCount());
193 ASSERT_EQ(8ul, resultMatrix.getRowGroupIndices().size());
194 ASSERT_EQ(8ul, result.markovianChoices.size());
195 ASSERT_EQ(7ul, result.markovianStates.size());
196 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
197 ASSERT_EQ(7ul, result.exitRates.size());
198}
199
200TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {
201 // Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
202 std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(true);
203
204 STORM_SILENT_ASSERT_THROW(
205 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra"),
206 storm::exceptions::WrongFormatException);
207}
TEST
TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile)
Definition MarkovAutomatonSparseTransitionParserTest.cpp:15
storm::parser::MarkovAutomatonSparseTransitionParser
A class providing the functionality to parse the transitions of a Markov automaton.
Definition MarkovAutomatonSparseTransitionParser.h:18
storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions
static Result parseMarkovAutomatonTransitions(std::string const &filename)
Parses the given file under the assumption that it contains a Markov automaton specified in the appro...
Definition MarkovAutomatonSparseTransitionParser.cpp:305
storm::settings::modules::BuildSettings::overrideDontFixDeadlocksSet
std::unique_ptr< storm::settings::SettingMemento > overrideDontFixDeadlocksSet(bool stateToSet)
Overrides the option to not fix deadlocks by setting it to the specified value.
Definition BuildSettings.cpp:140
storm::storage::BitVector::getNumberOfSetBits
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
Definition BitVector.cpp:689
storm::storage::BitVector::size
size_t size() const
Retrieves the number of bits this bit vector can store.
Definition BitVector.cpp:731
storm::storage::BitVector::get
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
Definition BitVector.cpp:267
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:328
storm::storage::SparseMatrix::getEntryCount
index_type getEntryCount() const
Returns the number of entries in the matrix.
Definition SparseMatrix.cpp:671
storm::storage::SparseMatrix::begin
const_iterator begin(index_type row) const
Retrieves an iterator that points to the beginning of the given row.
Definition SparseMatrix.cpp:2184
storm::storage::SparseMatrix::end
const_iterator end(index_type row) const
Retrieves an iterator that points past the end of the given row.
Definition SparseMatrix.cpp:2206
storm::storage::SparseMatrix::getRowGroupCount
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
Definition SparseMatrix.cpp:721
storm::storage::SparseMatrix::getColumnCount
index_type getColumnCount() const
Returns the number of columns of the matrix.
Definition SparseMatrix.cpp:666
storm::storage::SparseMatrix::const_iterator
std::vector< MatrixEntry< index_type, value_type > >::const_iterator const_iterator
Definition SparseMatrix.h:339
storm::storage::SparseMatrix::getRowGroupIndices
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
Definition SparseMatrix.cpp:767
storm::storage::SparseMatrix::getRowCount
index_type getRowCount() const
Returns the number of rows of the matrix.
Definition SparseMatrix.cpp:661
storm::settings::mutableBuildSettings
storm::settings::modules::BuildSettings & mutableBuildSettings()
Retrieves the build settings in a mutable form.
Definition SettingsManager.cpp:670
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:26
storm::parser::MarkovAutomatonSparseTransitionParser::Result::markovianChoices
storm::storage::BitVector markovianChoices
A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic.
Definition MarkovAutomatonSparseTransitionParser.h:66
storm::parser::MarkovAutomatonSparseTransitionParser::Result::markovianStates
storm::storage::BitVector markovianStates
A bit vector indicating which states possess a Markovian choice.
Definition MarkovAutomatonSparseTransitionParser.h:69
storm::parser::MarkovAutomatonSparseTransitionParser::Result::exitRates
std::vector< ValueType > exitRates
A vector that stores the exit rates for each state. For all states that do not possess Markovian choi...
Definition MarkovAutomatonSparseTransitionParser.h:72
storm::parser::MarkovAutomatonSparseTransitionParser::Result::transitionMatrixBuilder
storm::storage::SparseMatrixBuilder< ValueType > transitionMatrixBuilder
A matrix representing the transitions of the model.
Definition MarkovAutomatonSparseTransitionParser.h:63