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