Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
IntervalEndComponentPreserverTest.cpp
Go to the documentation of this file.
1#include <carl/formula/Constraint.h>
2#include <memory>
3#include <string>
4#include "gtest/gtest.h"
5#include "storm-config.h"
6#include "storm-pars/api/region.h"
7#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h"
8#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
9#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"
10#include "storm-pars/storage/ParameterRegion.h"
11#include "storm-pars/transformer/BinaryDtmcTransformer.h"
12#include "storm-pars/transformer/IntervalEndComponentPreserver.h"
13#include "storm-pars/transformer/RobustParameterLifter.h"
14#include "storm-parsers/parser/AutoParser.h"
15#include "storm-parsers/parser/FormulaParser.h"
16#include "storm/adapters/RationalFunctionAdapter.h"
17#include "storm/adapters/RationalFunctionForward.h"
18#include "storm/adapters/RationalNumberAdapter.h"
19#include "storm/adapters/RationalNumberForward.h"
20#include "storm/api/bisimulation.h"
21#include "storm/api/builder.h"
22#include "storm/environment/Environment.h"
23#include "storm/environment/solver/MinMaxSolverEnvironment.h"
24#include "storm/environment/solver/SolverEnvironment.h"
25#include "storm/modelchecker/CheckTask.h"
26#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
27#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
28#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
29#include "storm/models/sparse/Dtmc.h"
30#include "storm/models/sparse/Model.h"
31#include "storm/solver/IterativeMinMaxLinearEquationSolver.h"
32#include "storm/solver/MinMaxLinearEquationSolver.h"
33#include "storm/solver/OptimizationDirection.h"
34#include "storm/storage/SparseMatrix.h"
35#include "storm/storage/bisimulation/BisimulationType.h"
36#include "storm/storage/prism/Program.h"
37#include "storm/utility/prism.h"
38#include "storm/utility/vector.h"
39#include "test/storm_gtest.h"
40
41#include "storm-parsers/api/storm-parsers.h"
42#include "storm/utility/constants.h"
43#include "storm/utility/logging.h"
44#include "storm/utility/macros.h"
45
46class IntervalEndComponentPreserverTest : public ::testing::Test {
47 protected:
48 void SetUp() override {
49#ifndef STORM_HAVE_Z3
50 GTEST_SKIP() << "Z3 not available.";
51#endif
52 }
53};
54
55TEST_F(IntervalEndComponentPreserverTest, Simple) {
56 storm::storage::SparseMatrixBuilder<storm::Interval> builder(3, 3);
57 // 0 1 2
58 // ---- group 0/2 ----
59 // 0 ( [0, 1] [0, 1] 0 ) 0
60 // ---- group 1/2 ----
61 // 1 ( 0 0 [1, 1] ) 1
62 // ---- group 2/2 ----
63 // 2 ( 0 0 0 ) 2
64 // 0 1 2
65 builder.addNextValue(0, 0, storm::Interval(0, 1));
66 builder.addNextValue(0, 1, storm::Interval(0, 1));
67 builder.addNextValue(1, 2, storm::Interval(1, 1));
68 storm::storage::SparseMatrix<storm::Interval> matrix = builder.build();
69
70 std::vector<storm::Interval> vector = {storm::Interval(0, 0), storm::Interval(1, 1), storm::Interval(0, 0)};
71
72 storm::transformer::IntervalEndComponentPreserver preserver;
73 auto newMatrix = preserver.eliminateMECs(matrix, vector);
74
75 // Should be this now
76 // 0 1 2 3
77 // ---- group 0/3 ----
78 // 0 ( 0 [0, 1] 0 [0, 1] ) 0
79 // ---- group 1/3 ----
80 // 1 ( 0 0 [1, 1] 0 ) 1
81 // ---- group 2/3 ----
82 // 2 ( 0 0 0 0 ) 2
83 // ---- group 3/3 ----
84 // 3 ( 0 0 0 0 ) 3
85 // 0 1 2 3
86
87 ASSERT_EQ(newMatrix->getRowCount(), 4);
88 ASSERT_EQ(newMatrix->getColumnCount(), 4);
89 ASSERT_EQ(newMatrix->getEntryCount(), 3);
90
91 ASSERT_EQ(newMatrix->getRow(0).getNumberOfEntries(), 2);
92 ASSERT_EQ(newMatrix->getRow(0).begin()->getColumn(), 1);
93 ASSERT_EQ(newMatrix->getRow(0).begin()->getValue(), storm::Interval(0, 1));
94 ASSERT_EQ((newMatrix->getRow(0).begin() + 1)->getColumn(), 3);
95 ASSERT_EQ((newMatrix->getRow(0).begin() + 1)->getValue(), storm::Interval(0, 1));
96
97 ASSERT_EQ(newMatrix->getRow(1).getNumberOfEntries(), 1);
98 ASSERT_EQ(newMatrix->getRow(1).begin()->getColumn(), 2);
99 ASSERT_EQ(newMatrix->getRow(1).begin()->getValue(), storm::Interval(1, 1));
100
101 ASSERT_EQ(newMatrix->getRow(2).getNumberOfEntries(), 0);
102 ASSERT_EQ(newMatrix->getRow(3).getNumberOfEntries(), 0);
103}
TEST_F
TEST_F(IntervalEndComponentPreserverTest, Simple)
Definition IntervalEndComponentPreserverTest.cpp:55
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::transformer::IntervalEndComponentPreserver::eliminateMECs
std::optional< storage::SparseMatrix< Interval > > eliminateMECs(storm::storage::SparseMatrix< Interval > const &matrix, std::vector< Interval > const &vector)
Definition IntervalEndComponentPreserver.cpp:19
storm::Interval
carl::Interval< double > Interval
Interval type.
Definition RationalNumberForward.h:37
storm_gtest.h