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