From 1a4d4fd5a78becf88cd14d330c7dba042f0c42e1 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 22 Oct 2014 18:56:12 +0200 Subject: [PATCH] Added a test I used for finding the SCC Bug. Former-commit-id: 5936e79d04cb72fa389fd12d68030b850a514c45 --- ...glyConnectedComponentDecompositionTest.cpp | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp index a5872a921..48ece1776 100644 --- a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -1,9 +1,40 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/AutoParser.h" +#include "src/storage/SparseMatrix.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/models/MarkovAutomaton.h" + +TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix) { + storm::storage::SparseMatrixBuilder matrixBuilder(6, 6); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 0, 0.3)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 5, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 2, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 1, 0.4)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 2, 0.3)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 3, 0.3)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 4, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 4, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(5, 1, 1.0)); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + storm::storage::BitVector allBits(6, true); + + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, false, false)); + ASSERT_EQ(4, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, false)); + ASSERT_EQ(3, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, true)); + ASSERT_EQ(1, sccDecomposition.size()); +} + TEST(StronglyConnectedComponentDecomposition, FullSystem1) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");