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