Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
OrderTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h"
5#include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h"
6#include "storm-pars/modelchecker/region/monotonicity/LocalMonotonicityResult.h"
7#include "storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h"
8#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h"
9#include "storm-pars/modelchecker/region/monotonicity/Order.h"
10#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h"
11#include "storm/storage/BitVector.h"
12#include "storm/storage/StronglyConnectedComponentDecomposition.h"
13#include "storm/utility/graph.h"
14
15TEST(OrderTest, Simple) {
16 auto numberOfStates = 7;
17 auto above = storm::storage::BitVector(numberOfStates);
18 above.set(0);
19 auto below = storm::storage::BitVector(numberOfStates);
20 below.set(1);
21 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
22 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
23 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
24 storm::storage::StronglyConnectedComponentDecompositionOptions options;
25 options.forceTopologicalSort();
26 auto matrix = matrixBuilder.build();
27 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
28 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
29 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
30 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 1));
31 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 0));
32 EXPECT_EQ(nullptr, order.getNode(2));
33
34 order.add(2);
35 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 2));
36 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(2, 0));
37 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(2, 1));
38 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 2));
39
40 order.add(3);
41 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 3));
42 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3, 2));
43
44 order.addToNode(4, order.getNode(2));
45 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2, 4));
46 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(4, 2));
47 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 4));
48 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4, 0));
49 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(4, 1));
50 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 4));
51 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4, 3));
52 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3, 4));
53
54 order.addBetween(5, order.getNode(0), order.getNode(3));
55
56 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(5, 0));
57 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 5));
58 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5, 3));
59 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 5));
60 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5, 1));
61 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 5));
62 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5, 2));
63 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 5));
64 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5, 4));
65 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4, 5));
66
67 order.addBetween(6, order.getNode(5), order.getNode(3));
68 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 0));
69 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 6));
70 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6, 1));
71 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 6));
72 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6, 2));
73 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 6));
74 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6, 3));
75 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 6));
76 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6, 4));
77 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6, 4));
78 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 5));
79 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5, 6));
80
81 order.addRelationNodes(order.getNode(6), order.getNode(4));
82 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6, 4));
83 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4, 6));
84}
85
86TEST(OrderTest, copy_order) {
87 auto numberOfStates = 7;
88 auto above = storm::storage::BitVector(numberOfStates);
89 above.set(0);
90 auto below = storm::storage::BitVector(numberOfStates);
91 below.set(1);
92 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
93 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
94 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
95 storm::storage::StronglyConnectedComponentDecompositionOptions options;
96 options.forceTopologicalSort();
97 auto matrix = matrixBuilder.build();
98 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
99 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
100 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
101 order.add(2);
102 order.add(3);
103 order.addToNode(4, order.getNode(2));
104 order.addBetween(5, order.getNode(0), order.getNode(3));
105 order.addBetween(6, order.getNode(5), order.getNode(3));
106
107 auto orderCopy = storm::analysis::Order(order);
108 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0, 1));
109 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1, 0));
110
111 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0, 2));
112 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2, 0));
113 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(2, 1));
114 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1, 2));
115
116 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(2, 3));
117 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3, 2));
118
119 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(2, 4));
120 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(4, 2));
121 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0, 4));
122 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4, 0));
123 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(4, 1));
124 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1, 4));
125 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(4, 3));
126 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3, 4));
127
128 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(5, 0));
129 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0, 5));
130 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5, 3));
131 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3, 5));
132 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5, 1));
133 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1, 5));
134 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5, 2));
135 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5, 2));
136 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5, 4));
137 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5, 4));
138
139 order.addRelationNodes(order.getNode(6), order.getNode(4));
140 orderCopy = storm::analysis::Order(order);
141 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6, 0));
142 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0, 6));
143 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6, 1));
144 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1, 6));
145 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6, 2));
146 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2, 6));
147 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6, 3));
148 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3, 6));
149 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6, 4));
150 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4, 6));
151 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6, 5));
152 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5, 6));
153}
154
155TEST(OrderTest, merge_nodes) {
156 auto numberOfStates = 7;
157 auto above = storm::storage::BitVector(numberOfStates);
158 above.set(0);
159 auto below = storm::storage::BitVector(numberOfStates);
160 below.set(1);
161 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
162 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
163 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
164 storm::storage::StronglyConnectedComponentDecompositionOptions options;
165 options.forceTopologicalSort();
166 auto matrix = matrixBuilder.build();
167 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
168 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
169 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
170 order.add(2);
171 order.add(3);
172 order.addToNode(4, order.getNode(2));
173 order.addBetween(5, order.getNode(0), order.getNode(3));
174 order.addBetween(6, order.getNode(5), order.getNode(3));
175
176 order.mergeNodes(order.getNode(4), order.getNode(5));
177 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2, 4));
178 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2, 5));
179
180 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 5));
181 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 2));
182 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 4));
183
184 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 2));
185 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 4));
186 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 5));
187 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 2));
188 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 4));
189 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 5));
190 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 2));
191 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 4));
192 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 5));
193}
194
195TEST(OrderTest, sort_states) {
196 auto numberOfStates = 7;
197 auto above = storm::storage::BitVector(numberOfStates);
198 above.set(0);
199 auto below = storm::storage::BitVector(numberOfStates);
200 below.set(1);
201 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
202 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
203 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
204 storm::storage::StronglyConnectedComponentDecompositionOptions options;
205 options.forceTopologicalSort();
206 auto matrix = matrixBuilder.build();
207 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
208 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
209 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
210 order.add(2);
211 order.add(3);
212 order.addToNode(4, order.getNode(2));
213 order.addBetween(5, order.getNode(0), order.getNode(3));
214 order.addBetween(6, order.getNode(5), order.getNode(3));
215
216 std::vector<uint_fast64_t> statesToSort = std::vector<uint_fast64_t>{0, 1, 5, 6};
217 auto sortedStates = order.sortStates(&statesToSort);
218 EXPECT_EQ(4ul, sortedStates.size());
219
220 auto itr = sortedStates.begin();
221 EXPECT_EQ(0ul, *itr);
222 EXPECT_EQ(5ul, *(++itr));
223 EXPECT_EQ(6ul, *(++itr));
224 EXPECT_EQ(1ul, *(++itr));
225
226 statesToSort = std::vector<uint_fast64_t>{0, 1, 5, 6, 2};
227 sortedStates = order.sortStates(&statesToSort);
228 EXPECT_EQ(5ul, sortedStates.size());
229
230 itr = sortedStates.begin();
231 EXPECT_EQ(0ul, *itr);
232 EXPECT_EQ(5ul, *(++itr));
233 EXPECT_EQ(6ul, *(++itr));
234 EXPECT_EQ(1ul, *(++itr));
235 EXPECT_EQ(7ul, *(++itr));
236
237 statesToSort = std::vector<uint_fast64_t>{0, 2, 1, 5, 6};
238 sortedStates = order.sortStates(&statesToSort);
239 EXPECT_EQ(5ul, sortedStates.size());
240
241 itr = sortedStates.begin();
242 EXPECT_EQ(0ul, *itr);
243 EXPECT_EQ(2ul, *(++itr));
244 EXPECT_EQ(1ul, *(++itr));
245 EXPECT_EQ(7ul, *(++itr));
246 EXPECT_EQ(7ul, *(++itr));
247}
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:15
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
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::StronglyConnectedComponentDecomposition
This class represents the decomposition of a graph-like structure into its strongly connected compone...
Definition StronglyConnectedComponentDecomposition.h:100
storm::utility::graph::getTopologicalSort
std::vector< uint_fast64_t > getTopologicalSort(storm::storage::SparseMatrix< T > const &matrix, std::vector< uint64_t > const &firstStates)
Performs a topological sort of the states of the system according to the given transitions.
Definition graph.cpp:1851
storm_gtest.h
storm::storage::StronglyConnectedComponentDecompositionOptions::forceTopologicalSort
StronglyConnectedComponentDecompositionOptions & forceTopologicalSort(bool value=true)
Enforces that the returned SCCs are sorted in a topological order.
Definition StronglyConnectedComponentDecomposition.cpp:33