Storm 1.14.0.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, copy_is_deep) {
156 // Regression test: Order's copy constructor must deep-copy every Node, not alias the
157 // original's nodes. Mutating one Order (adding states, merging nodes) must not affect the
158 // other.
159 auto numberOfStates = 7;
160 auto above = storm::storage::BitVector(numberOfStates);
161 above.set(0);
162 auto below = storm::storage::BitVector(numberOfStates);
163 below.set(1);
164 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
165 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
166 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
167 storm::storage::StronglyConnectedComponentDecompositionOptions options;
168 options.forceTopologicalSort();
169 auto matrix = matrixBuilder.build();
170 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
171 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
172 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
173 order.add(2);
174 order.add(3);
175 order.addToNode(4, order.getNode(2));
176
177 auto orderCopy = storm::analysis::Order(order);
178
179 // Mutating the copy (adding a new state) must not be visible in the original.
180 orderCopy.addBetween(5, orderCopy.getNode(0), orderCopy.getNode(3));
181 EXPECT_TRUE(orderCopy.contains(5));
182 EXPECT_FALSE(order.contains(5));
183
184 // Mutating the original (adding a different state) must not be visible in the copy.
185 order.addBetween(6, order.getNode(0), order.getNode(3));
186 EXPECT_TRUE(order.contains(6));
187 EXPECT_FALSE(orderCopy.contains(6));
188
189 // Merging nodes in the copy must not merge the corresponding nodes in the original: states 2
190 // and 3 stay unrelated in the original, even after they are merged in the copy.
191 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 3));
192 orderCopy.mergeNodes(orderCopy.getNode(2), orderCopy.getNode(3));
193 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(2, 3));
194 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 3));
195
196 // Node pointers themselves must not be shared between the two Orders.
197 EXPECT_NE(order.getNode(0), orderCopy.getNode(0));
198 EXPECT_NE(order.getTop(), orderCopy.getTop());
199 EXPECT_NE(order.getBottom(), orderCopy.getBottom());
200}
201
202TEST(OrderTest, merge_nodes) {
203 auto numberOfStates = 7;
204 auto above = storm::storage::BitVector(numberOfStates);
205 above.set(0);
206 auto below = storm::storage::BitVector(numberOfStates);
207 below.set(1);
208 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
209 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
210 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
211 storm::storage::StronglyConnectedComponentDecompositionOptions options;
212 options.forceTopologicalSort();
213 auto matrix = matrixBuilder.build();
214 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
215 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
216 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
217 order.add(2);
218 order.add(3);
219 order.addToNode(4, order.getNode(2));
220 order.addBetween(5, order.getNode(0), order.getNode(3));
221 order.addBetween(6, order.getNode(5), order.getNode(3));
222
223 order.mergeNodes(order.getNode(4), order.getNode(5));
224 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2, 4));
225 EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2, 5));
226
227 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 5));
228 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 2));
229 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0, 4));
230
231 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 2));
232 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 4));
233 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6, 5));
234 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 2));
235 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 4));
236 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3, 5));
237 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 2));
238 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 4));
239 EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 5));
240}
241
242TEST(OrderTest, merge_nodes_inconsistent) {
243 // Regression test: forcing a merge that contradicts an already-established chain of relations
244 // must be reported gracefully (mergeNodes returns false, isInvalid() becomes true) rather than
245 // crashing on an internal assertion when a later compare() call discovers the resulting cycle.
246 auto numberOfStates = 6;
247 auto above = storm::storage::BitVector(numberOfStates);
248 above.set(0);
249 auto below = storm::storage::BitVector(numberOfStates);
250 below.set(1);
251 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
252 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
253 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
254 storm::storage::StronglyConnectedComponentDecompositionOptions options;
255 options.forceTopologicalSort();
256 auto matrix = matrixBuilder.build();
257 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
258 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
259 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
260
261 // Build a strict chain: top(0) > 3 > 4 > 5 > 2 > bottom(1).
262 order.add(2);
263 order.addBetween(3, order.getNode(0), order.getNode(2));
264 order.addBetween(4, order.getNode(3), order.getNode(2));
265 order.addBetween(5, order.getNode(4), order.getNode(2));
266 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(3, 2));
267 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(3, 4));
268 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(4, 5));
269 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5, 2));
270
271 // Forcing 3 and 2 to be equal directly contradicts 3 > 4 > 5 > 2: mergeNodes must refuse this
272 // (returning false, marking the order invalid) instead of leaving the order in a state where a
273 // later compare() call would discover a state both above and below another.
274 EXPECT_FALSE(order.mergeNodes(order.getNode(3), order.getNode(2)));
275 EXPECT_TRUE(order.isInvalid());
276
277 // Further compare() calls on the now-invalid order must not crash.
278 EXPECT_NO_FATAL_FAILURE(order.compare(4, 5));
279 EXPECT_NO_FATAL_FAILURE(order.compare(3, 4));
280 EXPECT_NO_FATAL_FAILURE(order.compare(0, 1));
281}
282
283TEST(OrderTest, sort_states) {
284 auto numberOfStates = 7;
285 auto above = storm::storage::BitVector(numberOfStates);
286 above.set(0);
287 auto below = storm::storage::BitVector(numberOfStates);
288 below.set(1);
289 storm::storage::SparseMatrixBuilder<storm::RationalFunction> matrixBuilder(2, 2, 2);
290 matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1));
291 matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1));
292 storm::storage::StronglyConnectedComponentDecompositionOptions options;
293 options.forceTopologicalSort();
294 auto matrix = matrixBuilder.build();
295 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(matrix, options);
296 auto statesSorted = storm::utility::graph::getTopologicalSort(matrix);
297 auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted);
298 order.add(2);
299 order.add(3);
300 order.addToNode(4, order.getNode(2));
301 order.addBetween(5, order.getNode(0), order.getNode(3));
302 order.addBetween(6, order.getNode(5), order.getNode(3));
303
304 std::vector<uint_fast64_t> statesToSort = std::vector<uint_fast64_t>{0, 1, 5, 6};
305 auto sortedStates = order.sortStates(&statesToSort);
306 EXPECT_EQ(4ul, sortedStates.size());
307
308 auto itr = sortedStates.begin();
309 EXPECT_EQ(0ul, *itr);
310 EXPECT_EQ(5ul, *(++itr));
311 EXPECT_EQ(6ul, *(++itr));
312 EXPECT_EQ(1ul, *(++itr));
313
314 statesToSort = std::vector<uint_fast64_t>{0, 1, 5, 6, 2};
315 sortedStates = order.sortStates(&statesToSort);
316 EXPECT_EQ(5ul, sortedStates.size());
317
318 itr = sortedStates.begin();
319 EXPECT_EQ(0ul, *itr);
320 EXPECT_EQ(5ul, *(++itr));
321 EXPECT_EQ(6ul, *(++itr));
322 EXPECT_EQ(1ul, *(++itr));
323 EXPECT_EQ(7ul, *(++itr));
324
325 statesToSort = std::vector<uint_fast64_t>{0, 2, 1, 5, 6};
326 sortedStates = order.sortStates(&statesToSort);
327 EXPECT_EQ(5ul, sortedStates.size());
328
329 itr = sortedStates.begin();
330 EXPECT_EQ(0ul, *itr);
331 EXPECT_EQ(2ul, *(++itr));
332 EXPECT_EQ(1ul, *(++itr));
333 EXPECT_EQ(7ul, *(++itr));
334 EXPECT_EQ(7ul, *(++itr));
335}
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:134
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:198
storm::storage::SparseMatrixBuilder::build
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
Definition SparseMatrix.cpp:293
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:1883
storm::RationalFunction
carl::RationalFunction< Polynomial, true > RationalFunction
Definition RationalFunctionForward.h:47
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