Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DeterministicSparseTransitionParserTest.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/DeterministicSparseTransitionParser.h"
5#include "storm-parsers/parser/ExplicitModelParserOptions.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(DeterministicSparseTransitionParserTest, 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::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"),
15 storm::exceptions::FileIoException);
16
17 storm::storage::SparseMatrix<double> nullMatrix;
18 STORM_SILENT_ASSERT_THROW(
19 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not", nullMatrix),
20 storm::exceptions::FileIoException);
21}
22
23TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
24 // Parse a deterministic transitions file and test the resulting matrix.
25 storm::storage::SparseMatrix<double> transitionMatrix =
26 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_general.tra");
27
28 ASSERT_EQ(8ul, transitionMatrix.getColumnCount());
29 ASSERT_EQ(17ul, transitionMatrix.getEntryCount());
30
31 // Test every entry of the matrix.
32 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
33
34 ASSERT_EQ(1ul, cIter->getColumn());
35 ASSERT_EQ(1, cIter->getValue());
36 cIter++;
37 ASSERT_EQ(2ul, cIter->getColumn());
38 ASSERT_EQ(0.5, cIter->getValue());
39 cIter++;
40 ASSERT_EQ(3ul, cIter->getColumn());
41 ASSERT_EQ(0.5, cIter->getValue());
42 cIter++;
43 ASSERT_EQ(3ul, cIter->getColumn());
44 ASSERT_EQ(0.4, cIter->getValue());
45 cIter++;
46 ASSERT_EQ(4ul, cIter->getColumn());
47 ASSERT_EQ(0.4, cIter->getValue());
48 cIter++;
49 ASSERT_EQ(5ul, cIter->getColumn());
50 ASSERT_EQ(0.2, cIter->getValue());
51 cIter++;
52 ASSERT_EQ(3ul, cIter->getColumn());
53 ASSERT_EQ(1, cIter->getValue());
54 cIter++;
55 ASSERT_EQ(3ul, cIter->getColumn());
56 ASSERT_EQ(1, cIter->getValue());
57 cIter++;
58 ASSERT_EQ(3ul, cIter->getColumn());
59 ASSERT_EQ(0.1, cIter->getValue());
60 cIter++;
61 ASSERT_EQ(4ul, cIter->getColumn());
62 ASSERT_EQ(0.1, cIter->getValue());
63 cIter++;
64 ASSERT_EQ(5ul, cIter->getColumn());
65 ASSERT_EQ(0.1, cIter->getValue());
66 cIter++;
67 ASSERT_EQ(6ul, cIter->getColumn());
68 ASSERT_EQ(0.7, cIter->getValue());
69 cIter++;
70 ASSERT_EQ(0ul, cIter->getColumn());
71 ASSERT_EQ(0.9, cIter->getValue());
72 cIter++;
73 ASSERT_EQ(5ul, cIter->getColumn());
74 ASSERT_EQ(0, cIter->getValue());
75 cIter++;
76 ASSERT_EQ(6ul, cIter->getColumn());
77 ASSERT_EQ(0.1, cIter->getValue());
78 cIter++;
79 ASSERT_EQ(6ul, cIter->getColumn());
80 ASSERT_EQ(0.224653, cIter->getValue());
81 cIter++;
82 ASSERT_EQ(7ul, cIter->getColumn());
83 ASSERT_EQ(0.775347, cIter->getValue());
84}
85
86TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
87 // First parse a transition file. Then parse a transition reward file for the resulting transition matrix.
88 storm::storage::SparseMatrix<double> transitionMatrix =
89 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_general.tra");
90
91 storm::storage::SparseMatrix<double> rewardMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(
92 STORM_TEST_RESOURCES_DIR "/rew/dtmc_general.trans.rew", transitionMatrix);
93
94 ASSERT_EQ(8ul, rewardMatrix.getColumnCount());
95 ASSERT_EQ(17ul, rewardMatrix.getEntryCount());
96
97 // Test every entry of the matrix.
98 storm::storage::SparseMatrix<double>::const_iterator cIter = rewardMatrix.begin(0);
99
100 ASSERT_EQ(1ul, cIter->getColumn());
101 ASSERT_EQ(10, cIter->getValue());
102 cIter++;
103 ASSERT_EQ(2ul, cIter->getColumn());
104 ASSERT_EQ(5, cIter->getValue());
105 cIter++;
106 ASSERT_EQ(3ul, cIter->getColumn());
107 ASSERT_EQ(5.5, cIter->getValue());
108 cIter++;
109 ASSERT_EQ(3ul, cIter->getColumn());
110 ASSERT_EQ(21.4, cIter->getValue());
111 cIter++;
112 ASSERT_EQ(4ul, cIter->getColumn());
113 ASSERT_EQ(4, cIter->getValue());
114 cIter++;
115 ASSERT_EQ(5ul, cIter->getColumn());
116 ASSERT_EQ(2, cIter->getValue());
117 cIter++;
118 ASSERT_EQ(3ul, cIter->getColumn());
119 ASSERT_EQ(1, cIter->getValue());
120 cIter++;
121 ASSERT_EQ(3ul, cIter->getColumn());
122 ASSERT_EQ(1, cIter->getValue());
123 cIter++;
124 ASSERT_EQ(3ul, cIter->getColumn());
125 ASSERT_EQ(0.1, cIter->getValue());
126 cIter++;
127 ASSERT_EQ(4ul, cIter->getColumn());
128 ASSERT_EQ(1.1, cIter->getValue());
129 cIter++;
130 ASSERT_EQ(5ul, cIter->getColumn());
131 ASSERT_EQ(9.5, cIter->getValue());
132 cIter++;
133 ASSERT_EQ(6ul, cIter->getColumn());
134 ASSERT_EQ(6.7, cIter->getValue());
135 cIter++;
136 ASSERT_EQ(0ul, cIter->getColumn());
137 ASSERT_EQ(1, cIter->getValue());
138 cIter++;
139 ASSERT_EQ(5ul, cIter->getColumn());
140 ASSERT_EQ(0, cIter->getValue());
141 cIter++;
142 ASSERT_EQ(6ul, cIter->getColumn());
143 ASSERT_EQ(12, cIter->getValue());
144 cIter++;
145 ASSERT_EQ(6ul, cIter->getColumn());
146 ASSERT_EQ(35.224653, cIter->getValue());
147 cIter++;
148 ASSERT_EQ(7ul, cIter->getColumn());
149 ASSERT_EQ(9.875347, cIter->getValue());
150}
151
152TEST(DeterministicSparseTransitionParserTest, Whitespaces) {
153 // Test the resilience of the parser against whitespaces.
154 // Do so by comparing the hash of the matrix resulting from the file without whitespaces with the hash of the matrix resulting from the file with
155 // whitespaces.
156 uint_fast64_t correctHash =
157 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_general.tra").hash();
158 storm::storage::SparseMatrix<double> transitionMatrix =
159 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_whitespaces.tra");
160 ASSERT_EQ(correctHash, transitionMatrix.hash());
161
162 // Do the same for the corresponding transition rewards file (with and without whitespaces)
163 correctHash = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(
164 STORM_TEST_RESOURCES_DIR "/rew/dtmc_general.trans.rew", transitionMatrix)
165 .hash();
166 ASSERT_EQ(correctHash, storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(
167 STORM_TEST_RESOURCES_DIR "/rew/dtmc_whitespaces.trans.rew", transitionMatrix)
168 .hash());
169}
170
171TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) {
172 // Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception.
173 STORM_SILENT_ASSERT_THROW(
174 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_mixedStateOrder.tra"),
175 storm::exceptions::InvalidArgumentException);
176
177 storm::storage::SparseMatrix<double> transitionMatrix =
178 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_general.tra");
179 STORM_SILENT_ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(
180 STORM_TEST_RESOURCES_DIR "/rew/dtmc_mixedStateOrder.trans.rew", transitionMatrix),
181 storm::exceptions::InvalidArgumentException);
182}
183
184TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
185 storm::parser::ExplicitModelParserOptions options;
186 options.fixDeadlocks = true;
187
188 // Parse a transitions file with the fixDeadlocks flag set and test if it works.
189 storm::storage::SparseMatrix<double> transitionMatrix =
190 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_deadlock.tra", options);
191
192 ASSERT_EQ(9ul, transitionMatrix.getColumnCount());
193 ASSERT_EQ(18ul, transitionMatrix.getEntryCount());
194
195 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(7);
196 ASSERT_EQ(7ul, cIter->getColumn());
197 ASSERT_EQ(1, cIter->getValue());
198 cIter++;
199 ASSERT_EQ(6ul, cIter->getColumn());
200 ASSERT_EQ(0.224653, cIter->getValue());
201 cIter++;
202 ASSERT_EQ(7ul, cIter->getColumn());
203 ASSERT_EQ(0.775347, cIter->getValue());
204}
205
206TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {
207 // Try to parse a transitions file containing a deadlock state with the fixDeadlocks flag unset. This should throw an exception.
208 storm::parser::ExplicitModelParserOptions options;
209 options.fixDeadlocks = false;
210
211 STORM_SILENT_ASSERT_THROW(
212 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_deadlock.tra", options),
213 storm::exceptions::WrongFormatException);
214}
215
216TEST(DeterministicSparseTransitionParserTest, DoubledLines) {
217 // There is a redundant line in the transition file. As the transition already exists this should throw an exception.
218 // Note: If two consecutive lines are doubled no exception is thrown.
219 STORM_SILENT_ASSERT_THROW(
220 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_doubledLines.tra"),
221 storm::exceptions::InvalidArgumentException);
222}
223
224TEST(DeterministicSparseTransitionParserTest, RewardForNonExistentTransition) {
225 // First parse a transition file. Then parse a transition reward file for the resulting transition matrix.
226 storm::storage::SparseMatrix<double> transitionMatrix =
227 storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_general.tra");
228
229 // There is a reward for a transition that does not exist in the transition matrix.
230 STORM_SILENT_ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(
231 STORM_TEST_RESOURCES_DIR "/rew/dtmc_rewardForNonExTrans.trans.rew", transitionMatrix),
232 storm::exceptions::WrongFormatException);
233}
TEST
TEST(DeterministicSparseTransitionParserTest, NonExistingFile)
Definition DeterministicSparseTransitionParserTest.cpp:11
storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions
static storm::storage::SparseMatrix< ValueType > parseDeterministicTransitions(std::string const &filename, ExplicitModelParserOptions const &options=ExplicitModelParserOptions())
Load a deterministic transition system from file and create a sparse adjacency matrix whose entries r...
Definition DeterministicSparseTransitionParser.cpp:20
storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards
static storm::storage::SparseMatrix< ValueType > parseDeterministicTransitionRewards(std::string const &filename, storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix)
Load the transition rewards for a deterministic transition system from file and create a sparse adjac...
Definition DeterministicSparseTransitionParser.cpp:28
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::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_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:14