Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StronglyConnectedComponentDecompositionTest.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/AutoParser.h"
5#include "storm/models/sparse/MarkovAutomaton.h"
6#include "storm/models/sparse/StandardRewardModel.h"
7#include "storm/storage/SparseMatrix.h"
8#include "storm/storage/StronglyConnectedComponentDecomposition.h"
9
10TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix) {
11 storm::storage::SparseMatrixBuilder<double> matrixBuilder(6, 6);
12 ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 0, 0.3));
13 ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 5, 0.7));
14 ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 2, 1.0));
15 ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 1, 0.4));
16 ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 2, 0.3));
17 ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 3, 0.3));
18 ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 4, 1.0));
19 ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.5));
20 ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 4, 0.5));
21 ASSERT_NO_THROW(matrixBuilder.addNextValue(5, 1, 1.0));
22
23 storm::storage::SparseMatrix<double> matrix;
24 ASSERT_NO_THROW(matrix = matrixBuilder.build());
25
26 storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
27 storm::storage::StronglyConnectedComponentDecompositionOptions options;
28
29 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(matrix, options));
30 ASSERT_EQ(4ul, sccDecomposition.size());
31
32 options.dropNaiveSccs();
33 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(matrix, options));
34 ASSERT_EQ(3ul, sccDecomposition.size());
35
36 options.onlyBottomSccs();
37 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(matrix, options));
38 ASSERT_EQ(1ul, sccDecomposition.size());
39}
40
41TEST(StronglyConnectedComponentDecomposition, FullSystem1) {
42 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
43 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", "");
44
45 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::sparse::MarkovAutomaton<double>>();
46
47 storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
48 storm::storage::StronglyConnectedComponentDecompositionOptions options;
49
50 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
51 ASSERT_EQ(5ul, sccDecomposition.size());
52
53 options.dropNaiveSccs();
54 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
55 ASSERT_EQ(2ul, sccDecomposition.size());
56
57 options.onlyBottomSccs();
58 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
59 ASSERT_EQ(2ul, sccDecomposition.size());
60
61 markovAutomaton = nullptr;
62}
63
64TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
65 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
66 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny2.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny2.lab", "", "");
67
68 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::sparse::MarkovAutomaton<double>>();
69
70 storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
71 storm::storage::StronglyConnectedComponentDecompositionOptions options;
72
73 options.dropNaiveSccs();
74 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
75 ASSERT_EQ(2ul, sccDecomposition.size());
76
77 // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way.
78 storm::storage::StateBlock const& scc1 = sccDecomposition[0];
79 storm::storage::StateBlock const& scc2 = sccDecomposition[1];
80
81 storm::storage::StateBlock correctScc1 = {1, 3, 8, 9, 10};
82 storm::storage::StateBlock correctScc2 = {4, 5, 6, 7};
83 ASSERT_TRUE(scc1 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) ||
84 scc1 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));
85 ASSERT_TRUE(scc2 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) ||
86 scc2 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));
87
88 options.onlyBottomSccs();
89 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
90 ASSERT_EQ(1ul, sccDecomposition.size());
91
92 markovAutomaton = nullptr;
93}
TEST
TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix)
Definition StronglyConnectedComponentDecompositionTest.cpp:10
storm::models::sparse::MarkovAutomaton
This class represents a Markov automaton.
Definition MarkovAutomaton.h:14
storm::parser::AutoParser::parseModel
static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel(std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
Checks the given files and parses the model within these files.
Definition AutoParser.cpp:25
storm::storage::Decomposition::size
std::size_t size() const
Retrieves the number of blocks of this decomposition.
Definition Decomposition.cpp:40
storm::storage::SparseMatrixBuilder
A class that can be used to build a sparse matrix by adding value by value.
Definition SparseMatrix.h:133
storm::storage::SparseMatrixBuilder::addNextValue
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
Definition SparseMatrix.cpp:156
storm::storage::SparseMatrixBuilder::build
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
Definition SparseMatrix.cpp:281
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:328
storm::storage::StateBlock::begin
iterator begin()
Returns an iterator to the states in this SCC.
Definition StateBlock.cpp:5
storm::storage::StateBlock::end
iterator end()
Returns an iterator that points one past the end of the states in this SCC.
Definition StateBlock.cpp:13
storm::storage::StronglyConnectedComponentDecomposition
This class represents the decomposition of a graph-like structure into its strongly connected compone...
Definition StronglyConnectedComponentDecomposition.h:100
storm_gtest.h
storm::storage::StronglyConnectedComponentDecompositionOptions::dropNaiveSccs
StronglyConnectedComponentDecompositionOptions & dropNaiveSccs(bool value=true)
Sets if trivial SCCs (i.e. SCCs consisting of just one state without a self-loop) are to be kept in t...
Definition StronglyConnectedComponentDecomposition.cpp:23
storm::storage::StronglyConnectedComponentDecompositionOptions::onlyBottomSccs
StronglyConnectedComponentDecompositionOptions & onlyBottomSccs(bool value=true)
Sets if only bottom SCCs, i.e. SCCs in which all states have no way of leaving the SCC),...
Definition StronglyConnectedComponentDecomposition.cpp:28