Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NondeterministicSparseTransitionParserTest.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/ExplicitModelParserOptions.h"
5#include "storm-parsers/parser/NondeterministicSparseTransitionParser.h"
6#include "storm/exceptions/FileIoException.h"
7#include "storm/exceptions/InvalidArgumentException.h"
8#include "storm/exceptions/WrongFormatException.h"
9#include "storm/storage/SparseMatrix.h"
10
11TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) {
12 // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
13 STORM_SILENT_ASSERT_THROW(
14 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"),
15 storm::exceptions::FileIoException);
16
17 storm::storage::SparseMatrix<double> nullInformation;
18 STORM_SILENT_ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(
19 STORM_TEST_RESOURCES_DIR "/nonExistingFile.not", nullInformation),
20 storm::exceptions::FileIoException);
21}
22
23TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
24 // Parse a nondeterministic transitions file and test the result.
25 storm::storage::SparseMatrix<double> result(
26 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_general.tra"));
27
28 // Test the row mapping, i.e. at which row which state starts.
29 ASSERT_EQ(6ul, result.getRowGroupCount());
30 ASSERT_EQ(7ul, result.getRowGroupIndices().size());
31 ASSERT_EQ(0ul, result.getRowGroupIndices()[0]);
32 ASSERT_EQ(4ul, result.getRowGroupIndices()[1]);
33 ASSERT_EQ(5ul, result.getRowGroupIndices()[2]);
34 ASSERT_EQ(7ul, result.getRowGroupIndices()[3]);
35 ASSERT_EQ(8ul, result.getRowGroupIndices()[4]);
36 ASSERT_EQ(9ul, result.getRowGroupIndices()[5]);
37 ASSERT_EQ(11ul, result.getRowGroupIndices()[6]);
38
39 // Test the transition matrix.
40 ASSERT_EQ(6ul, result.getColumnCount());
41 ASSERT_EQ(11ul, result.getRowCount());
42 ASSERT_EQ(22ul, result.getEntryCount());
43
44 // Test every entry of the matrix.
45 storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0);
46
47 ASSERT_EQ(0ul, cIter->getColumn());
48 ASSERT_EQ(0.9, cIter->getValue());
49 cIter++;
50 ASSERT_EQ(1ul, cIter->getColumn());
51 ASSERT_EQ(0.1, cIter->getValue());
52 cIter++;
53 ASSERT_EQ(1ul, cIter->getColumn());
54 ASSERT_EQ(0.2, cIter->getValue());
55 cIter++;
56 ASSERT_EQ(2ul, cIter->getColumn());
57 ASSERT_EQ(0.2, cIter->getValue());
58 cIter++;
59 ASSERT_EQ(3ul, cIter->getColumn());
60 ASSERT_EQ(0.2, cIter->getValue());
61 cIter++;
62 ASSERT_EQ(4ul, cIter->getColumn());
63 ASSERT_EQ(0.2, cIter->getValue());
64 cIter++;
65 ASSERT_EQ(5ul, cIter->getColumn());
66 ASSERT_EQ(0.2, cIter->getValue());
67 cIter++;
68 ASSERT_EQ(5ul, cIter->getColumn());
69 ASSERT_EQ(1, cIter->getValue());
70 cIter++;
71 ASSERT_EQ(0ul, cIter->getColumn());
72 ASSERT_EQ(0.1, cIter->getValue());
73 cIter++;
74 ASSERT_EQ(4ul, cIter->getColumn());
75 ASSERT_EQ(0.9, cIter->getValue());
76 cIter++;
77 ASSERT_EQ(2ul, cIter->getColumn());
78 ASSERT_EQ(1, cIter->getValue());
79 cIter++;
80 ASSERT_EQ(2ul, cIter->getColumn());
81 ASSERT_EQ(0.5, cIter->getValue());
82 cIter++;
83 ASSERT_EQ(3ul, cIter->getColumn());
84 ASSERT_EQ(0.5, cIter->getValue());
85 cIter++;
86 ASSERT_EQ(2ul, cIter->getColumn());
87 ASSERT_EQ(1, cIter->getValue());
88 cIter++;
89 ASSERT_EQ(2ul, cIter->getColumn());
90 ASSERT_EQ(0.001, cIter->getValue());
91 cIter++;
92 ASSERT_EQ(3ul, cIter->getColumn());
93 ASSERT_EQ(0.999, cIter->getValue());
94 cIter++;
95 ASSERT_EQ(1ul, cIter->getColumn());
96 ASSERT_EQ(0.7, cIter->getValue());
97 cIter++;
98 ASSERT_EQ(4ul, cIter->getColumn());
99 ASSERT_EQ(0.3, cIter->getValue());
100 cIter++;
101 ASSERT_EQ(1ul, cIter->getColumn());
102 ASSERT_EQ(0.2, cIter->getValue());
103 cIter++;
104 ASSERT_EQ(4ul, cIter->getColumn());
105 ASSERT_EQ(0.2, cIter->getValue());
106 cIter++;
107 ASSERT_EQ(5ul, cIter->getColumn());
108 ASSERT_EQ(0.6, cIter->getValue());
109 cIter++;
110 ASSERT_EQ(5ul, cIter->getColumn());
111 ASSERT_EQ(1, cIter->getValue());
112}
113
114TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
115 // Parse a nondeterministic transitions file and test the result.
116 storm::storage::SparseMatrix<double> modelInformation(
117 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_general.tra"));
118 storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(
119 STORM_TEST_RESOURCES_DIR "/rew/mdp_general.trans.rew", modelInformation));
120
121 // Test the transition matrix.
122 ASSERT_EQ(6ul, result.getColumnCount());
123 ASSERT_EQ(11ul, result.getRowCount());
124 ASSERT_EQ(17ul, result.getEntryCount());
125
126 // Test every entry of the matrix.
127 storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0);
128
129 ASSERT_EQ(0ul, cIter->getColumn());
130 ASSERT_EQ(1, cIter->getValue());
131 cIter++;
132 ASSERT_EQ(1ul, cIter->getColumn());
133 ASSERT_EQ(30, cIter->getValue());
134 cIter++;
135 ASSERT_EQ(1ul, cIter->getColumn());
136 ASSERT_EQ(15.2, cIter->getValue());
137 cIter++;
138 ASSERT_EQ(2ul, cIter->getColumn());
139 ASSERT_EQ(75, cIter->getValue());
140 cIter++;
141 ASSERT_EQ(5ul, cIter->getColumn());
142 ASSERT_EQ(2.45, cIter->getValue());
143 cIter++;
144 ASSERT_EQ(5ul, cIter->getColumn());
145 ASSERT_EQ(1, cIter->getValue());
146 cIter++;
147 ASSERT_EQ(0ul, cIter->getColumn());
148 ASSERT_EQ(0.114, cIter->getValue());
149 cIter++;
150 ASSERT_EQ(4ul, cIter->getColumn());
151 ASSERT_EQ(90, cIter->getValue());
152 cIter++;
153 ASSERT_EQ(2ul, cIter->getColumn());
154 ASSERT_EQ(1, cIter->getValue());
155 cIter++;
156 ASSERT_EQ(2ul, cIter->getColumn());
157 ASSERT_EQ(55, cIter->getValue());
158 cIter++;
159 ASSERT_EQ(3ul, cIter->getColumn());
160 ASSERT_EQ(87, cIter->getValue());
161 cIter++;
162 ASSERT_EQ(2ul, cIter->getColumn());
163 ASSERT_EQ(13, cIter->getValue());
164 cIter++;
165 ASSERT_EQ(3ul, cIter->getColumn());
166 ASSERT_EQ(999, cIter->getValue());
167 cIter++;
168 ASSERT_EQ(1ul, cIter->getColumn());
169 ASSERT_EQ(0.7, cIter->getValue());
170 cIter++;
171 ASSERT_EQ(4ul, cIter->getColumn());
172 ASSERT_EQ(0.3, cIter->getValue());
173 cIter++;
174 ASSERT_EQ(1ul, cIter->getColumn());
175 ASSERT_EQ(0.1, cIter->getValue());
176 cIter++;
177 ASSERT_EQ(5ul, cIter->getColumn());
178 ASSERT_EQ(6, cIter->getValue());
179}
180
181TEST(NondeterministicSparseTransitionParserTest, Whitespaces) {
182 // Test the resilience of the parser against whitespaces.
183 // Do so by comparing the hashes of the transition matices and the rowMapping vectors element by element.
184 storm::storage::SparseMatrix<double> correctResult(
185 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_general.tra"));
186 storm::storage::SparseMatrix<double> whitespaceResult =
187 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_whitespaces.tra");
188 ASSERT_EQ(correctResult.hash(), whitespaceResult.hash());
189 ASSERT_EQ(correctResult.getRowGroupIndices().size(), whitespaceResult.getRowGroupIndices().size());
190 for (uint_fast64_t i = 0; i < correctResult.getRowGroupIndices().size(); i++) {
191 ASSERT_EQ(correctResult.getRowGroupIndices()[i], whitespaceResult.getRowGroupIndices()[i]);
192 }
193
194 // Do the same (minus the unused rowMapping) for the corresponding transition rewards file (with and without whitespaces)
195 uint_fast64_t correctHash = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(
196 STORM_TEST_RESOURCES_DIR "/rew/mdp_general.trans.rew", correctResult)
197 .hash();
198 ASSERT_EQ(correctHash, storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(
199 STORM_TEST_RESOURCES_DIR "/rew/mdp_whitespaces.trans.rew", whitespaceResult)
200 .hash());
201}
202
203TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) {
204 // Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception.
205 STORM_SILENT_ASSERT_THROW(
206 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_mixedStateOrder.tra"),
207 storm::exceptions::InvalidArgumentException);
208
209 storm::storage::SparseMatrix<double> modelInformation =
210 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_general.tra");
211 STORM_SILENT_ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(
212 STORM_TEST_RESOURCES_DIR "/rew/mdp_mixedStateOrder.trans.rew", modelInformation),
213 storm::exceptions::InvalidArgumentException);
214}
215
216TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
217 storm::parser::ExplicitModelParserOptions options;
218 options.fixDeadlocks = true;
219
220 // Parse a transitions file with the fixDeadlocks flag set and test if it works.
221 storm::storage::SparseMatrix<double> result(
222 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_deadlock.tra", options));
223
224 ASSERT_EQ(8ul, result.getRowGroupIndices().size());
225 ASSERT_EQ(9ul, result.getRowGroupIndices()[5]);
226 ASSERT_EQ(10ul, result.getRowGroupIndices()[6]);
227 ASSERT_EQ(12ul, result.getRowGroupIndices()[7]);
228
229 ASSERT_EQ(7ul, result.getColumnCount());
230 ASSERT_EQ(12ul, result.getRowCount());
231 ASSERT_EQ(23ul, result.getEntryCount());
232
233 storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(8);
234
235 ASSERT_EQ(1ul, cIter->getColumn());
236 ASSERT_EQ(0.7, cIter->getValue());
237 cIter++;
238 ASSERT_EQ(4ul, cIter->getColumn());
239 ASSERT_EQ(0.3, cIter->getValue());
240 cIter++;
241 ASSERT_EQ(5ul, cIter->getColumn());
242 ASSERT_EQ(1, cIter->getValue());
243 cIter++;
244 ASSERT_EQ(1ul, cIter->getColumn());
245 ASSERT_EQ(0.2, cIter->getValue());
246 cIter++;
247 ASSERT_EQ(4ul, cIter->getColumn());
248 ASSERT_EQ(0.2, cIter->getValue());
249 cIter++;
250 ASSERT_EQ(5ul, cIter->getColumn());
251 ASSERT_EQ(0.6, cIter->getValue());
252 cIter++;
253 ASSERT_EQ(5ul, cIter->getColumn());
254 ASSERT_EQ(1, cIter->getValue());
255}
256
257TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) {
258 // Try to parse a transitions file containing a deadlock state with the fixDeadlocks flag unset. This should throw an exception.
259 storm::parser::ExplicitModelParserOptions options;
260 options.fixDeadlocks = false;
261
262 STORM_SILENT_ASSERT_THROW(
263 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_deadlock.tra", options),
264 storm::exceptions::WrongFormatException);
265}
266
267TEST(NondeterministicSparseTransitionParserTest, DoubledLines) {
268 // There is a redundant line in the transition file. As the transition already exists this should throw an exception.
269 STORM_SILENT_ASSERT_THROW(
270 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_doubledLines.tra"),
271 storm::exceptions::InvalidArgumentException);
272}
273
274TEST(NondeterministicSparseTransitionParserTest, RewardForNonExistentTransition) {
275 // First parse a transition file. Then parse a transition reward file for the resulting transition matrix.
276 storm::storage::SparseMatrix<double> transitionResult =
277 storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_general.tra");
278
279 // There is a reward for a transition that does not exist in the transition matrix.
280 STORM_SILENT_ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(
281 STORM_TEST_RESOURCES_DIR "/rew/mdp_rewardForNonExTrans.trans.rew", transitionResult),
282 storm::exceptions::WrongFormatException);
283}
TEST
TEST(NondeterministicSparseTransitionParserTest, NonExistingFile)
Definition NondeterministicSparseTransitionParserTest.cpp:11
storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions
static storm::storage::SparseMatrix< ValueType > parseNondeterministicTransitions(std::string const &filename, ExplicitModelParserOptions const &options=ExplicitModelParserOptions())
Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entrie...
Definition NondeterministicSparseTransitionParser.cpp:19
storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards
static storm::storage::SparseMatrix< ValueType > parseNondeterministicTransitionRewards(std::string const &filename, storm::storage::SparseMatrix< MatrixValueType > const &modelInformation)
Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entrie...
Definition NondeterministicSparseTransitionParser.cpp:27
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::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::hash
std::size_t hash() const
Calculates a hash value over all values contained in the matrix.
Definition SparseMatrix.cpp:2473
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