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