Storm
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 "storm-parsers/parser/AutoParser.h"
3#include "storm/models/sparse/MarkovAutomaton.h"
4#include "storm/models/sparse/StandardRewardModel.h"
5#include "storm/storage/SparseMatrix.h"
6#include "storm/storage/StronglyConnectedComponentDecomposition.h"
7#include "test/storm_gtest.h"
8
9TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix) {
10 storm::storage::SparseMatrixBuilder<double> matrixBuilder(6, 6);
11 ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 0, 0.3));
12 ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 5, 0.7));
13 ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 2, 1.0));
14 ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 1, 0.4));
15 ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 2, 0.3));
16 ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 3, 0.3));
17 ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 4, 1.0));
18 ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.5));
19 ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 4, 0.5));
20 ASSERT_NO_THROW(matrixBuilder.addNextValue(5, 1, 1.0));
21
22 storm::storage::SparseMatrix<double> matrix;
23 ASSERT_NO_THROW(matrix = matrixBuilder.build());
24
25 storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
26 storm::storage::StronglyConnectedComponentDecompositionOptions options;
27
28 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(matrix, options));
29 ASSERT_EQ(4ul, sccDecomposition.size());
30
31 options.dropNaiveSccs();
32 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(matrix, options));
33 ASSERT_EQ(3ul, sccDecomposition.size());
34
35 options.onlyBottomSccs();
36 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(matrix, options));
37 ASSERT_EQ(1ul, sccDecomposition.size());
38}
39
40TEST(StronglyConnectedComponentDecomposition, FullSystem1) {
41 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
42 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", "");
43
44 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::sparse::MarkovAutomaton<double>>();
45
46 storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
47 storm::storage::StronglyConnectedComponentDecompositionOptions options;
48
49 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
50 ASSERT_EQ(5ul, sccDecomposition.size());
51
52 options.dropNaiveSccs();
53 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
54 ASSERT_EQ(2ul, sccDecomposition.size());
55
56 options.onlyBottomSccs();
57 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
58 ASSERT_EQ(2ul, sccDecomposition.size());
59
60 markovAutomaton = nullptr;
61}
62
63TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
64 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
65 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny2.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny2.lab", "", "");
66
67 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::sparse::MarkovAutomaton<double>>();
68
69 storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
70 storm::storage::StronglyConnectedComponentDecompositionOptions options;
71
72 options.dropNaiveSccs();
73 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
74 ASSERT_EQ(2ul, sccDecomposition.size());
75
76 // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way.
77 storm::storage::StateBlock const& scc1 = sccDecomposition[0];
78 storm::storage::StateBlock const& scc2 = sccDecomposition[1];
79
80 storm::storage::StateBlock correctScc1 = {1, 3, 8, 9, 10};
81 storm::storage::StateBlock correctScc2 = {4, 5, 6, 7};
82 ASSERT_TRUE(scc1 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) ||
83 scc1 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));
84 ASSERT_TRUE(scc2 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) ||
85 scc2 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));
86
87 options.onlyBottomSccs();
88 ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(markovAutomaton->getTransitionMatrix(), options));
89 ASSERT_EQ(1ul, sccDecomposition.size());
90
91 markovAutomaton = nullptr;
92}
TEST
TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix)
Definition StronglyConnectedComponentDecompositionTest.cpp:9
storm::models::sparse::MarkovAutomaton
This class represents a Markov automaton.
Definition MarkovAutomaton.h:16
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:137
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:332
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