Storm 1.14.0.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/ExplicitModelParserOptions.h"
7#include "storm-parsers/parser/MarkovAutomatonParser.h"
8#include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h"
9#include "storm-parsers/util/cstring.h"
10#include "storm/exceptions/FileIoException.h"
11#include "storm/exceptions/WrongFormatException.h"
12
13TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile) {
14 // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
15 STORM_SILENT_ASSERT_THROW(
16 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"),
17 storm::exceptions::FileIoException);
18}
19
20TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
21 // The file that will be used for the test.
22 std::string filename = STORM_TEST_RESOURCES_DIR "/tra/ma_general.tra";
23
24 // Execute the parser.
25 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
26 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
27
28 // Build the actual transition matrix.
29 storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0, 0));
30
31 // Test all sizes and counts.
32 ASSERT_EQ(6ul, transitionMatrix.getColumnCount());
33 ASSERT_EQ(7ul, transitionMatrix.getRowCount());
34 ASSERT_EQ(12ul, transitionMatrix.getEntryCount());
35 ASSERT_EQ(6ul, transitionMatrix.getRowGroupCount());
36 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices().size());
37 ASSERT_EQ(7ul, result.markovianChoices.size());
38 ASSERT_EQ(6ul, result.markovianStates.size());
39 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
40 ASSERT_EQ(6ul, result.exitRates.size());
41
42 // Test the general structure of the transition system (that will be an Markov automaton).
43
44 // Test the mapping between states and transition matrix rows.
45 ASSERT_EQ(0ul, transitionMatrix.getRowGroupIndices()[0]);
46 ASSERT_EQ(1ul, transitionMatrix.getRowGroupIndices()[1]);
47 ASSERT_EQ(2ul, transitionMatrix.getRowGroupIndices()[2]);
48 ASSERT_EQ(3ul, transitionMatrix.getRowGroupIndices()[3]);
49 ASSERT_EQ(4ul, transitionMatrix.getRowGroupIndices()[4]);
50 ASSERT_EQ(6ul, transitionMatrix.getRowGroupIndices()[5]);
51 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices()[6]);
52
53 // Test the Markovian states.
54 ASSERT_TRUE(result.markovianStates.get(0));
55 ASSERT_FALSE(result.markovianStates.get(1));
56 ASSERT_TRUE(result.markovianStates.get(2));
57 ASSERT_FALSE(result.markovianStates.get(3));
58 ASSERT_FALSE(result.markovianStates.get(4));
59 ASSERT_FALSE(result.markovianStates.get(5));
60
61 // Test the exit rates. These have to be 0 for all non-Markovian states.
62 ASSERT_EQ(2, result.exitRates[0]);
63 ASSERT_EQ(0, result.exitRates[1]);
64 ASSERT_EQ(15, result.exitRates[2]);
65 ASSERT_EQ(0, result.exitRates[3]);
66 ASSERT_EQ(0, result.exitRates[4]);
67 ASSERT_EQ(0, result.exitRates[5]);
68
69 // Finally, test the transition matrix itself.
70 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
71
72 ASSERT_EQ(2, cIter->getValue());
73 cIter++;
74 ASSERT_EQ(1, cIter->getValue());
75 cIter++;
76 ASSERT_EQ(1, cIter->getValue());
77 cIter++;
78 ASSERT_EQ(2, cIter->getValue());
79 cIter++;
80 ASSERT_EQ(4, cIter->getValue());
81 cIter++;
82 ASSERT_EQ(8, cIter->getValue());
83 cIter++;
84 ASSERT_EQ(0.5, cIter->getValue());
85 cIter++;
86 ASSERT_EQ(0.5, cIter->getValue());
87 cIter++;
88 ASSERT_EQ(1, cIter->getValue());
89 cIter++;
90 ASSERT_EQ(0.5, cIter->getValue());
91 cIter++;
92 ASSERT_EQ(0.5, cIter->getValue());
93 cIter++;
94 ASSERT_EQ(1, cIter->getValue());
95 cIter++;
96 ASSERT_EQ(transitionMatrix.end(), cIter);
97}
98
99TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
100 // The file that will be used for the test.
101 std::string filename = STORM_TEST_RESOURCES_DIR "/tra/ma_whitespaces.tra";
102
103 // Execute the parser.
104 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
105 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
106
107 // Build the actual transition matrix.
108 storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build());
109
110 // Test all sizes and counts.
111 ASSERT_EQ(6ul, transitionMatrix.getColumnCount());
112 ASSERT_EQ(7ul, transitionMatrix.getRowCount());
113 ASSERT_EQ(12ul, transitionMatrix.getEntryCount());
114 ASSERT_EQ(6ul, transitionMatrix.getRowGroupCount());
115 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices().size());
116 ASSERT_EQ(7ul, result.markovianChoices.size());
117 ASSERT_EQ(6ul, result.markovianStates.size());
118 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
119 ASSERT_EQ(6ul, result.exitRates.size());
120
121 // Test the general structure of the transition system (that will be an Markov automaton).
122
123 // Test the mapping between states and transition matrix rows.
124 ASSERT_EQ(0ul, transitionMatrix.getRowGroupIndices()[0]);
125 ASSERT_EQ(1ul, transitionMatrix.getRowGroupIndices()[1]);
126 ASSERT_EQ(2ul, transitionMatrix.getRowGroupIndices()[2]);
127 ASSERT_EQ(3ul, transitionMatrix.getRowGroupIndices()[3]);
128 ASSERT_EQ(4ul, transitionMatrix.getRowGroupIndices()[4]);
129 ASSERT_EQ(6ul, transitionMatrix.getRowGroupIndices()[5]);
130 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices()[6]);
131
132 // Test the Markovian states.
133 ASSERT_TRUE(result.markovianStates.get(0));
134 ASSERT_FALSE(result.markovianStates.get(1));
135 ASSERT_TRUE(result.markovianStates.get(2));
136 ASSERT_FALSE(result.markovianStates.get(3));
137 ASSERT_FALSE(result.markovianStates.get(4));
138 ASSERT_FALSE(result.markovianStates.get(5));
139
140 // Test the exit rates. These have to be 0 for all non-Markovian states.
141 ASSERT_EQ(2, result.exitRates[0]);
142 ASSERT_EQ(0, result.exitRates[1]);
143 ASSERT_EQ(15, result.exitRates[2]);
144 ASSERT_EQ(0, result.exitRates[3]);
145 ASSERT_EQ(0, result.exitRates[4]);
146 ASSERT_EQ(0, result.exitRates[5]);
147
148 // Finally, test the transition matrix itself.
149 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
150
151 ASSERT_EQ(2, cIter->getValue());
152 cIter++;
153 ASSERT_EQ(1, cIter->getValue());
154 cIter++;
155 ASSERT_EQ(1, cIter->getValue());
156 cIter++;
157 ASSERT_EQ(2, cIter->getValue());
158 cIter++;
159 ASSERT_EQ(4, cIter->getValue());
160 cIter++;
161 ASSERT_EQ(8, cIter->getValue());
162 cIter++;
163 ASSERT_EQ(0.5, cIter->getValue());
164 cIter++;
165 ASSERT_EQ(0.5, cIter->getValue());
166 cIter++;
167 ASSERT_EQ(1, cIter->getValue());
168 cIter++;
169 ASSERT_EQ(0.5, cIter->getValue());
170 cIter++;
171 ASSERT_EQ(0.5, cIter->getValue());
172 cIter++;
173 ASSERT_EQ(1, cIter->getValue());
174 cIter++;
175 ASSERT_EQ(transitionMatrix.end(), cIter);
176}
177
178TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
179 storm::parser::ExplicitModelParserOptions options;
180 options.fixDeadlocks = true;
181
182 // Parse a Markov Automaton transition file with the fixDeadlocks flag set and test if it works.
183 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
184 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra", options);
185
186 // Test if the result is consistent with the parsed Markov Automaton.
187 storm::storage::SparseMatrix<double> resultMatrix(result.transitionMatrixBuilder.build());
188 ASSERT_EQ(7ul, resultMatrix.getColumnCount());
189 ASSERT_EQ(13ul, resultMatrix.getEntryCount());
190 ASSERT_EQ(7ul, resultMatrix.getRowGroupCount());
191 ASSERT_EQ(8ul, resultMatrix.getRowGroupIndices().size());
192 ASSERT_EQ(8ul, result.markovianChoices.size());
193 ASSERT_EQ(7ul, result.markovianStates.size());
194 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
195 ASSERT_EQ(7ul, result.exitRates.size());
196}
197
198TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {
199 // Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocks flag unset. This should throw an exception.
200 storm::parser::ExplicitModelParserOptions options;
201 options.fixDeadlocks = false;
202
203 STORM_SILENT_ASSERT_THROW(
204 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra", options),
205 storm::exceptions::WrongFormatException);
206}
TEST
TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile)
Definition MarkovAutomatonSparseTransitionParserTest.cpp:13
storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions
static Result parseMarkovAutomatonTransitions(std::string const &filename, ExplicitModelParserOptions const &options=ExplicitModelParserOptions())
Parses the given file under the assumption that it contains a Markov automaton specified in the appro...
Definition MarkovAutomatonSparseTransitionParser.cpp:286
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:691
storm::storage::BitVector::size
size_t size() const
Retrieves the number of bits this bit vector can store.
Definition BitVector.cpp:737
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:269
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:329
storm::storage::SparseMatrix::getEntryCount
index_type getEntryCount() const
Returns the number of entries in the matrix.
Definition SparseMatrix.cpp:670
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:2185
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:2207
storm::storage::SparseMatrix::getRowGroupCount
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
Definition SparseMatrix.cpp:725
storm::storage::SparseMatrix::getColumnCount
index_type getColumnCount() const
Returns the number of columns of the matrix.
Definition SparseMatrix.cpp:665
storm::storage::SparseMatrix::const_iterator
std::vector< MatrixEntry< index_type, value_type > >::const_iterator const_iterator
Definition SparseMatrix.h:340
storm::storage::SparseMatrix::getRowGroupIndices
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
Definition SparseMatrix.cpp:771
storm::storage::SparseMatrix::getRowCount
index_type getRowCount() const
Returns the number of rows of the matrix.
Definition SparseMatrix.cpp:660
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:14
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