Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MarkovAutomatonSparseTransitionParserTest.cpp
Go to the documentation of this file.
1/*
2 * MarkovAutomatonParserTest.cpp
3 *
4 * Created on: 03.12.2013
5 * Author: Manuel Sascha Weiand
6 */
7
8#include "storm-config.h"
9#include "storm/settings/SettingsManager.h"
10#include "storm/settings/modules/BuildSettings.h"
11#include "test/storm_gtest.h"
12
13#include <vector>
14
15#include "storm-parsers/parser/MarkovAutomatonParser.h"
16#include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h"
17#include "storm-parsers/util/cstring.h"
18#include "storm/exceptions/FileIoException.h"
19#include "storm/exceptions/WrongFormatException.h"
20#include "storm/settings/SettingMemento.h"
21
22#define STATE_COUNT 6ul
23#define CHOICE_COUNT 7ul
24
25TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile) {
26 // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
27 STORM_SILENT_ASSERT_THROW(
28 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"),
29 storm::exceptions::FileIoException);
30}
31
32TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
33 // The file that will be used for the test.
34 std::string filename = STORM_TEST_RESOURCES_DIR "/tra/ma_general.tra";
35
36 // Execute the parser.
37 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
38 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
39
40 // Build the actual transition matrix.
41 storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0, 0));
42
43 // Test all sizes and counts.
44 ASSERT_EQ(STATE_COUNT, transitionMatrix.getColumnCount());
45 ASSERT_EQ(CHOICE_COUNT, transitionMatrix.getRowCount());
46 ASSERT_EQ(12ul, transitionMatrix.getEntryCount());
47 ASSERT_EQ(6ul, transitionMatrix.getRowGroupCount());
48 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices().size());
49 ASSERT_EQ(CHOICE_COUNT, result.markovianChoices.size());
50 ASSERT_EQ(STATE_COUNT, result.markovianStates.size());
51 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
52 ASSERT_EQ(STATE_COUNT, result.exitRates.size());
53
54 // Test the general structure of the transition system (that will be an Markov automaton).
55
56 // Test the mapping between states and transition matrix rows.
57 ASSERT_EQ(0ul, transitionMatrix.getRowGroupIndices()[0]);
58 ASSERT_EQ(1ul, transitionMatrix.getRowGroupIndices()[1]);
59 ASSERT_EQ(2ul, transitionMatrix.getRowGroupIndices()[2]);
60 ASSERT_EQ(3ul, transitionMatrix.getRowGroupIndices()[3]);
61 ASSERT_EQ(4ul, transitionMatrix.getRowGroupIndices()[4]);
62 ASSERT_EQ(6ul, transitionMatrix.getRowGroupIndices()[5]);
63 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices()[6]);
64
65 // Test the Markovian states.
66 ASSERT_TRUE(result.markovianStates.get(0));
67 ASSERT_FALSE(result.markovianStates.get(1));
68 ASSERT_TRUE(result.markovianStates.get(2));
69 ASSERT_FALSE(result.markovianStates.get(3));
70 ASSERT_FALSE(result.markovianStates.get(4));
71 ASSERT_FALSE(result.markovianStates.get(5));
72
73 // Test the exit rates. These have to be 0 for all non-Markovian states.
74 ASSERT_EQ(2, result.exitRates[0]);
75 ASSERT_EQ(0, result.exitRates[1]);
76 ASSERT_EQ(15, result.exitRates[2]);
77 ASSERT_EQ(0, result.exitRates[3]);
78 ASSERT_EQ(0, result.exitRates[4]);
79 ASSERT_EQ(0, result.exitRates[5]);
80
81 // Finally, test the transition matrix itself.
82 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
83
84 ASSERT_EQ(2, cIter->getValue());
85 cIter++;
86 ASSERT_EQ(1, cIter->getValue());
87 cIter++;
88 ASSERT_EQ(1, cIter->getValue());
89 cIter++;
90 ASSERT_EQ(2, cIter->getValue());
91 cIter++;
92 ASSERT_EQ(4, cIter->getValue());
93 cIter++;
94 ASSERT_EQ(8, cIter->getValue());
95 cIter++;
96 ASSERT_EQ(0.5, cIter->getValue());
97 cIter++;
98 ASSERT_EQ(0.5, cIter->getValue());
99 cIter++;
100 ASSERT_EQ(1, cIter->getValue());
101 cIter++;
102 ASSERT_EQ(0.5, cIter->getValue());
103 cIter++;
104 ASSERT_EQ(0.5, cIter->getValue());
105 cIter++;
106 ASSERT_EQ(1, cIter->getValue());
107 cIter++;
108 ASSERT_EQ(transitionMatrix.end(), cIter);
109}
110
111TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
112 // The file that will be used for the test.
113 std::string filename = STORM_TEST_RESOURCES_DIR "/tra/ma_whitespaces.tra";
114
115 // Execute the parser.
116 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
117 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(filename);
118
119 // Build the actual transition matrix.
120 storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build());
121
122 // Test all sizes and counts.
123 ASSERT_EQ(STATE_COUNT, transitionMatrix.getColumnCount());
124 ASSERT_EQ(CHOICE_COUNT, transitionMatrix.getRowCount());
125 ASSERT_EQ(12ul, transitionMatrix.getEntryCount());
126 ASSERT_EQ(6ul, transitionMatrix.getRowGroupCount());
127 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices().size());
128 ASSERT_EQ(CHOICE_COUNT, result.markovianChoices.size());
129 ASSERT_EQ(STATE_COUNT, result.markovianStates.size());
130 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
131 ASSERT_EQ(STATE_COUNT, result.exitRates.size());
132
133 // Test the general structure of the transition system (that will be an Markov automaton).
134
135 // Test the mapping between states and transition matrix rows.
136 ASSERT_EQ(0ul, transitionMatrix.getRowGroupIndices()[0]);
137 ASSERT_EQ(1ul, transitionMatrix.getRowGroupIndices()[1]);
138 ASSERT_EQ(2ul, transitionMatrix.getRowGroupIndices()[2]);
139 ASSERT_EQ(3ul, transitionMatrix.getRowGroupIndices()[3]);
140 ASSERT_EQ(4ul, transitionMatrix.getRowGroupIndices()[4]);
141 ASSERT_EQ(6ul, transitionMatrix.getRowGroupIndices()[5]);
142 ASSERT_EQ(7ul, transitionMatrix.getRowGroupIndices()[6]);
143
144 // Test the Markovian states.
145 ASSERT_TRUE(result.markovianStates.get(0));
146 ASSERT_FALSE(result.markovianStates.get(1));
147 ASSERT_TRUE(result.markovianStates.get(2));
148 ASSERT_FALSE(result.markovianStates.get(3));
149 ASSERT_FALSE(result.markovianStates.get(4));
150 ASSERT_FALSE(result.markovianStates.get(5));
151
152 // Test the exit rates. These have to be 0 for all non-Markovian states.
153 ASSERT_EQ(2, result.exitRates[0]);
154 ASSERT_EQ(0, result.exitRates[1]);
155 ASSERT_EQ(15, result.exitRates[2]);
156 ASSERT_EQ(0, result.exitRates[3]);
157 ASSERT_EQ(0, result.exitRates[4]);
158 ASSERT_EQ(0, result.exitRates[5]);
159
160 // Finally, test the transition matrix itself.
161 storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
162
163 ASSERT_EQ(2, cIter->getValue());
164 cIter++;
165 ASSERT_EQ(1, cIter->getValue());
166 cIter++;
167 ASSERT_EQ(1, cIter->getValue());
168 cIter++;
169 ASSERT_EQ(2, cIter->getValue());
170 cIter++;
171 ASSERT_EQ(4, cIter->getValue());
172 cIter++;
173 ASSERT_EQ(8, cIter->getValue());
174 cIter++;
175 ASSERT_EQ(0.5, cIter->getValue());
176 cIter++;
177 ASSERT_EQ(0.5, cIter->getValue());
178 cIter++;
179 ASSERT_EQ(1, cIter->getValue());
180 cIter++;
181 ASSERT_EQ(0.5, cIter->getValue());
182 cIter++;
183 ASSERT_EQ(0.5, cIter->getValue());
184 cIter++;
185 ASSERT_EQ(1, cIter->getValue());
186 cIter++;
187 ASSERT_EQ(transitionMatrix.end(), cIter);
188}
189
190TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
191 // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
192 std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(false);
193
194 // Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works.
195 typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result =
196 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra");
197
198 // Test if the result is consistent with the parsed Markov Automaton.
199 storm::storage::SparseMatrix<double> resultMatrix(result.transitionMatrixBuilder.build());
200 ASSERT_EQ(STATE_COUNT + 1, resultMatrix.getColumnCount());
201 ASSERT_EQ(13ul, resultMatrix.getEntryCount());
202 ASSERT_EQ(7ul, resultMatrix.getRowGroupCount());
203 ASSERT_EQ(8ul, resultMatrix.getRowGroupIndices().size());
204 ASSERT_EQ(CHOICE_COUNT + 1, result.markovianChoices.size());
205 ASSERT_EQ(STATE_COUNT + 1, result.markovianStates.size());
206 ASSERT_EQ(2ul, result.markovianStates.getNumberOfSetBits());
207 ASSERT_EQ(STATE_COUNT + 1, result.exitRates.size());
208}
209
210TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {
211 // Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
212 std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(true);
213
214 STORM_SILENT_ASSERT_THROW(
215 storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra"),
216 storm::exceptions::WrongFormatException);
217}
TEST
TEST(MarkovAutomatonSparseTransitionParserTest, NonExistingFile)
Definition MarkovAutomatonSparseTransitionParserTest.cpp:25
storm::parser::MarkovAutomatonSparseTransitionParser
A class providing the functionality to parse the transitions of a Markov automaton.
Definition MarkovAutomatonSparseTransitionParser.h:18
storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions
static Result parseMarkovAutomatonTransitions(std::string const &filename)
Parses the given file under the assumption that it contains a Markov automaton specified in the appro...
Definition MarkovAutomatonSparseTransitionParser.cpp:305
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::BitVector::size
size_t size() const
Retrieves the number of bits this bit vector can store.
Definition BitVector.cpp:774
storm::storage::BitVector::getNumberOfSetBits
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
Definition BitVector.cpp:711
storm::storage::BitVector::get
bool get(uint_fast64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
Definition BitVector.cpp:268
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::end
const_iterator end(index_type row) const
Retrieves an iterator that points past the end of the given row.
Definition SparseMatrix.cpp:2405
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::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
storm::parser::MarkovAutomatonSparseTransitionParser::Result::markovianChoices
storm::storage::BitVector markovianChoices
A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic.
Definition MarkovAutomatonSparseTransitionParser.h:66
storm::parser::MarkovAutomatonSparseTransitionParser::Result::markovianStates
storm::storage::BitVector markovianStates
A bit vector indicating which states possess a Markovian choice.
Definition MarkovAutomatonSparseTransitionParser.h:69
storm::parser::MarkovAutomatonSparseTransitionParser::Result::exitRates
std::vector< ValueType > exitRates
A vector that stores the exit rates for each state. For all states that do not possess Markovian choi...
Definition MarkovAutomatonSparseTransitionParser.h:72
storm::parser::MarkovAutomatonSparseTransitionParser::Result::transitionMatrixBuilder
storm::storage::SparseMatrixBuilder< ValueType > transitionMatrixBuilder
A matrix representing the transitions of the model.
Definition MarkovAutomatonSparseTransitionParser.h:63