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