Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Order.cpp
Go to the documentation of this file.
1#include "Order.h"
2
3#include <iostream>
4#include <queue>
6
7namespace storm {
8namespace analysis {
9Order::Order(storm::storage::BitVector* topStates, storm::storage::BitVector* bottomStates, uint_fast64_t numberOfStates,
10 storage::Decomposition<storage::StronglyConnectedComponent> decomposition, std::vector<uint_fast64_t> statesSorted) {
11 init(numberOfStates, decomposition);
12 this->numberOfAddedStates = 0;
13 this->onlyBottomTopOrder = true;
14 for (auto const& i : *topStates) {
15 this->doneStates.set(i);
16 this->bottom->statesAbove.set(i);
17 this->top->states.insert(i);
18 this->nodes[i] = top;
19 numberOfAddedStates++;
20 }
21 this->statesSorted = statesSorted;
22
23 for (auto const& i : *bottomStates) {
24 this->doneStates.set(i);
25 this->bottom->states.insert(i);
26 this->nodes[i] = bottom;
27 numberOfAddedStates++;
28 }
29 assert(numberOfAddedStates <= numberOfStates);
30 assert(doneStates.getNumberOfSetBits() == (topStates->getNumberOfSetBits() + bottomStates->getNumberOfSetBits()));
31 if (numberOfAddedStates == numberOfStates) {
32 doneBuilding = doneStates.full();
33 }
34}
35
36Order::Order(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates,
37 storage::Decomposition<storage::StronglyConnectedComponent> decomposition, std::vector<uint_fast64_t> statesSorted) {
38 init(numberOfStates, decomposition);
39
40 this->onlyBottomTopOrder = true;
41 this->doneStates.set(topState);
42
43 this->bottom->statesAbove.set(topState);
44 this->top->states.insert(topState);
45 this->nodes[topState] = top;
46
47 this->doneStates.set(bottomState);
48
49 this->bottom->states.insert(bottomState);
50 this->nodes[bottomState] = bottom;
51 this->numberOfAddedStates = 2;
52 assert(numberOfAddedStates <= numberOfStates);
53
54 this->statesSorted = statesSorted;
55 assert(doneStates.getNumberOfSetBits() == 2);
56 if (numberOfAddedStates == numberOfStates) {
57 doneBuilding = doneStates.full();
58 }
59}
60
62 this->invalid = false;
63}
64
65/*** Modifying the order ***/
66
67void Order::add(uint_fast64_t state) {
68 assert(nodes[state] == nullptr);
69 addBetween(state, top, bottom);
70 addStateToHandle(state);
71}
72
73void Order::addAbove(uint_fast64_t state, Node* node) {
74 STORM_LOG_INFO("Add " << state << " above " << *node->states.begin() << '\n');
75
76 assert(nodes[state] == nullptr);
77 Node* newNode = new Node();
78 nodes[state] = newNode;
79
80 newNode->states.insert(state);
81 newNode->statesAbove = storm::storage::BitVector(numberOfStates, false);
82 for (auto const& state : top->states) {
83 newNode->statesAbove.set(state);
84 }
85 node->statesAbove.set(state);
86 numberOfAddedStates++;
87 onlyBottomTopOrder = false;
88 if (numberOfAddedStates == numberOfStates) {
89 doneBuilding = doneStates.full();
90 }
91}
92
93void Order::addBelow(uint_fast64_t state, Node* node) {
94 STORM_LOG_INFO("Add " << state << " below " << *node->states.begin() << '\n');
95
96 assert(nodes[state] == nullptr);
97 Node* newNode = new Node();
98 nodes[state] = newNode;
99 newNode->states.insert(state);
101 for (auto statesAbove : node->states) {
102 newNode->statesAbove.set(statesAbove);
103 }
104 bottom->statesAbove.set(state);
105 numberOfAddedStates++;
106 onlyBottomTopOrder = false;
107 if (numberOfAddedStates == numberOfStates) {
108 doneBuilding = doneStates.full();
109 }
110 assert(numberOfAddedStates <= numberOfStates);
111}
112
113void Order::addBetween(uint_fast64_t state, Node* above, Node* below) {
114 STORM_LOG_INFO("Add " << state << " between (above) " << *above->states.begin() << " and " << *below->states.begin() << '\n');
115
116 assert(compare(above, below) == ABOVE);
117 assert(above != nullptr && below != nullptr);
118 if (nodes[state] == nullptr) {
119 // State is not in the order yet
120 Node* newNode = new Node();
121 nodes[state] = newNode;
122
123 newNode->states.insert(state);
125 for (auto aboveStates : above->states) {
126 newNode->statesAbove.set(aboveStates);
127 }
128 below->statesAbove.set(state);
129 numberOfAddedStates++;
130 onlyBottomTopOrder = false;
131 if (numberOfAddedStates == numberOfStates) {
132 doneBuilding = doneStates.full();
133 }
134 assert(numberOfAddedStates <= numberOfStates);
135 } else {
136 // State is in the order already, so we add the new relations
137 addRelationNodes(above, nodes[state]);
138 addRelationNodes(nodes[state], below);
139 }
140}
141
142void Order::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) {
143 assert(compare(above, below) == ABOVE);
144 assert(getNode(below)->states.find(below) != getNode(below)->states.end());
145 assert(getNode(above)->states.find(above) != getNode(above)->states.end());
146
147 addBetween(state, getNode(above), getNode(below));
148}
149
150void Order::addRelation(uint_fast64_t above, uint_fast64_t below, bool allowMerge) {
151 assert(getNode(above) != nullptr && getNode(below) != nullptr);
152 addRelationNodes(getNode(above), getNode(below), allowMerge);
153}
154
155void Order::addRelationNodes(Order::Node* above, Order::Node* below, bool allowMerge) {
156 assert(allowMerge || compare(above, below) != BELOW);
157
158 STORM_LOG_INFO("Add relation between (above) " << *above->states.begin() << " and " << *below->states.begin() << '\n');
159
160 if (allowMerge) {
161 if (compare(below, above) == ABOVE) {
162 mergeNodes(above, below);
163 return;
164 }
165 }
166 below->statesAbove |= ((above->statesAbove));
167 for (auto const& state : above->states) {
168 below->statesAbove.set(state);
169 }
170 assert(compare(above, below) == ABOVE);
171}
172
173void Order::addToNode(uint_fast64_t state, Node* node) {
174 STORM_LOG_INFO("Add " << state << " to between (above) " << *node->states.begin() << '\n');
175
176 if (nodes[state] == nullptr) {
177 // State is not in the order yet
178 node->states.insert(state);
179 nodes[state] = node;
180 numberOfAddedStates++;
181 if (numberOfAddedStates == numberOfStates) {
182 doneBuilding = doneStates.full();
183 }
184 assert(numberOfAddedStates <= numberOfStates);
185
186 } else {
187 // State is in the order already, so we merge the nodes
188 mergeNodes(nodes[state], node);
189 }
190}
191
193 STORM_LOG_INFO("Merge " << *node1->states.begin() << " and " << *node2->states.begin() << '\n');
194
195 // Merges node2 into node 1
196 // everything above n2 also above n1
197 node1->statesAbove |= ((node2->statesAbove));
198 // add states of node 2 to node 1
199 node1->states.insert(node2->states.begin(), node2->states.end());
200
201 for (auto const& i : node2->states) {
202 nodes[i] = node1;
203 }
204
205 for (auto const& node : nodes) {
206 if (node != nullptr) {
207 for (auto state2 : node2->states) {
208 if (node->statesAbove[state2]) {
209 for (auto state1 : node1->states) {
210 node->statesAbove.set(state1);
211 }
212 break;
213 }
214 }
215 }
216 }
217 for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
218 for (uint_fast64_t j = i + 1; j < numberOfStates; ++j) {
219 auto comp1 = compare(i, j);
220 auto comp2 = compare(j, i);
221 if (!((comp1 == BELOW && comp2 == ABOVE) || (comp1 == ABOVE && comp2 == BELOW) || (comp1 == UNKNOWN && comp2 == UNKNOWN) ||
222 (comp1 == SAME && comp2 == SAME))) {
223 invalid = true;
224 return false;
225 }
226 }
227 }
228 return !invalid;
229}
230
231bool Order::merge(uint_fast64_t var1, uint_fast64_t var2) {
232 return mergeNodes(getNode(var1), getNode(var2));
233}
234
235/*** Checking on the order ***/
236
237Order::NodeComparison Order::compare(uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis) {
238 return compare(getNode(state1), getNode(state2), hypothesis);
239}
240
241Order::NodeComparison Order::compareFast(uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis) const {
242 auto res = compareFast(getNode(state1), getNode(state2), hypothesis);
243 return res;
244}
245
247 if (node1 != nullptr && node2 != nullptr) {
248 if (node1 == node2) {
249 return SAME;
250 }
251
252 if ((hypothesis == UNKNOWN || hypothesis == ABOVE) && ((node1 == top || node2 == bottom) || aboveFast(node1, node2))) {
253 return ABOVE;
254 }
255
256 if ((hypothesis == UNKNOWN || hypothesis == BELOW) && ((node2 == top || node1 == bottom) || aboveFast(node2, node1))) {
257 return BELOW;
258 }
259 } else if (node1 == top || node2 == bottom) {
260 return ABOVE;
261 } else if (node2 == top || node1 == bottom) {
262 return BELOW;
263 }
264 return UNKNOWN;
265}
266
268 if (node1 != nullptr && node2 != nullptr) {
269 auto comp = compareFast(node1, node2, hypothesis);
270 if (comp != UNKNOWN) {
271 return comp;
272 }
273 if ((hypothesis == UNKNOWN || hypothesis == ABOVE) && above(node1, node2)) {
274 assert(!above(node2, node1));
275 return ABOVE;
276 }
277
278 if ((hypothesis == UNKNOWN || hypothesis == BELOW) && above(node2, node1)) {
279 return BELOW;
280 }
281 } else if (node1 == top || node2 == bottom) {
282 return ABOVE;
283 } else if (node2 == top || node1 == bottom) {
284 return BELOW;
285 }
286 return UNKNOWN;
287}
288
289bool Order::contains(uint_fast64_t state) const {
290 return state < numberOfStates && nodes[state] != nullptr;
291}
292
294 return bottom;
295}
296
298 assert(!doneStates.full() || numberOfAddedStates == numberOfStates);
299 return doneStates.full();
300}
301
302uint_fast64_t Order::getNextDoneState(uint_fast64_t state) const {
303 return doneStates.getNextSetIndex(state + 1);
304}
305
306Order::Node* Order::getNode(uint_fast64_t stateNumber) const {
307 assert(stateNumber < numberOfStates);
308 return nodes[stateNumber];
309}
310
311std::vector<Order::Node*> Order::getNodes() const {
312 return nodes;
313}
314
315std::vector<uint_fast64_t>& Order::getStatesSorted() {
316 return statesSorted;
317}
318
320 return top;
321}
322
323uint_fast64_t Order::getNumberOfAddedStates() const {
324 return numberOfAddedStates;
325}
326
327uint_fast64_t Order::getNumberOfStates() const {
328 return numberOfStates;
329}
330
331bool Order::isBottomState(uint_fast64_t state) const {
332 auto states = bottom->states;
333 return states.find(state) != states.end();
334}
335
336bool Order::isTopState(uint_fast64_t state) const {
337 auto states = top->states;
338 return states.find(state) != states.end();
339}
340
342 return onlyBottomTopOrder;
343}
344
345std::vector<uint_fast64_t> Order::sortStates(std::vector<uint_fast64_t>* states) {
346 assert(states != nullptr);
347 uint_fast64_t numberOfStatesToSort = states->size();
348 std::vector<uint_fast64_t> result;
349 // Go over all states
350 for (auto state : *states) {
351 bool unknown = false;
352 if (result.size() == 0) {
353 result.push_back(state);
354 } else {
355 bool added = false;
356 for (auto itr = result.begin(); itr != result.end(); ++itr) {
357 auto compareRes = compare(state, (*itr));
358 if (compareRes == ABOVE || compareRes == SAME) {
359 // insert at current pointer (while keeping other values)
360 result.insert(itr, state);
361 added = true;
362 break;
363 } else if (compareRes == UNKNOWN) {
364 unknown = true;
365 break;
366 }
367 }
368 if (unknown) {
369 break;
370 }
371 if (!added) {
372 result.push_back(state);
373 }
374 }
375 }
376 while (result.size() < numberOfStatesToSort) {
377 result.push_back(numberOfStates);
378 }
379 assert(result.size() == numberOfStatesToSort);
380 return result;
381}
382
383std::pair<std::pair<uint_fast64_t, uint_fast64_t>, std::vector<uint_fast64_t>> Order::sortStatesForForward(uint_fast64_t currentState,
384 std::vector<uint_fast64_t> const& states) {
385 std::vector<uint_fast64_t> statesSorted;
386 statesSorted.push_back(currentState);
387 // Go over all states
388 bool oneUnknown = false;
389 bool unknown = false;
390 uint_fast64_t s1 = numberOfStates;
391 uint_fast64_t s2 = numberOfStates;
392 for (auto& state : states) {
393 unknown = false;
394 bool added = false;
395 for (auto itr = statesSorted.begin(); itr != statesSorted.end(); ++itr) {
396 auto compareRes = compare(state, (*itr));
397 if (compareRes == ABOVE || compareRes == SAME) {
398 if (!contains(state) && compareRes == ABOVE) {
399 add(state);
400 }
401 added = true;
402 // insert at current pointer (while keeping other values)
403 statesSorted.insert(itr, state);
404 break;
405 } else if (compareRes == UNKNOWN && !oneUnknown) {
406 // We miss state in the result.
407 s1 = state;
408 s2 = *itr;
409 oneUnknown = true;
410 added = true;
411 break;
412 } else if (compareRes == UNKNOWN && oneUnknown) {
413 unknown = true;
414 added = true;
415 break;
416 }
417 }
418 if (!added) {
419 // State will be last in the list
420 statesSorted.push_back(state);
421 }
422 if (unknown && oneUnknown) {
423 break;
424 }
425 }
426 if (!unknown && oneUnknown) {
427 assert(statesSorted.size() == states.size());
428 s2 = numberOfStates;
429 }
430 assert(s1 == numberOfStates || (s1 != numberOfStates && s2 == numberOfStates && statesSorted.size() == states.size()) ||
431 (s1 != numberOfStates && s2 != numberOfStates && statesSorted.size() < states.size()));
432
433 return {{s1, s2}, statesSorted};
434}
435
436std::pair<std::pair<uint_fast64_t, uint_fast64_t>, std::vector<uint_fast64_t>> Order::sortStatesUnorderedPair(const std::vector<uint_fast64_t>* states) {
437 assert(states != nullptr);
438 uint_fast64_t numberOfStatesToSort = states->size();
439 std::vector<uint_fast64_t> result;
440 // Go over all states
441 for (auto state : *states) {
442 bool unknown = false;
443 if (result.size() == 0) {
444 result.push_back(state);
445 } else {
446 bool added = false;
447 for (auto itr = result.begin(); itr != result.end(); ++itr) {
448 auto compareRes = compare(state, (*itr));
449 if (compareRes == ABOVE || compareRes == SAME) {
450 // insert at current pointer (while keeping other values)
451 result.insert(itr, state);
452 added = true;
453 break;
454 } else if (compareRes == UNKNOWN) {
455 return {{(*itr), state}, std::move(result)};
456 }
457 }
458 if (unknown) {
459 break;
460 }
461 if (!added) {
462 result.push_back(state);
463 }
464 }
465 }
466
467 assert(result.size() == numberOfStatesToSort);
468 return {{numberOfStates, numberOfStates}, std::move(result)};
469}
470
471std::vector<uint_fast64_t> Order::sortStates(storm::storage::BitVector* states) {
472 uint_fast64_t numberOfStatesToSort = states->getNumberOfSetBits();
473 std::vector<uint_fast64_t> result;
474 // Go over all states
475 for (auto state : *states) {
476 bool unknown = false;
477 if (result.size() == 0) {
478 result.push_back(state);
479 } else {
480 bool added = false;
481 for (auto itr = result.begin(); itr != result.end(); ++itr) {
482 auto compareRes = compare(state, (*itr));
483 if (compareRes == ABOVE || compareRes == SAME) {
484 // insert at current pointer (while keeping other values)
485 result.insert(itr, state);
486 added = true;
487 break;
488 } else if (compareRes == UNKNOWN) {
489 unknown = true;
490 break;
491 }
492 }
493 if (unknown) {
494 break;
495 }
496 if (!added) {
497 result.push_back(state);
498 }
499 }
500 }
501 while (result.size() < numberOfStatesToSort) {
502 result.push_back(numberOfStates);
503 }
504 assert(result.size() == numberOfStatesToSort);
505 return result;
506}
507
508/*** Checking on helpfunctionality for building of order ***/
509
510std::shared_ptr<Order> Order::copy() const {
511 assert(!isInvalid());
512 std::shared_ptr<Order> copiedOrder = std::make_shared<Order>();
513 copiedOrder->nodes = std::vector<Node*>(numberOfStates, nullptr);
514 copiedOrder->onlyBottomTopOrder = this->isOnlyBottomTopOrder();
515 copiedOrder->numberOfStates = this->getNumberOfStates();
516 copiedOrder->statesSorted = std::vector<uint_fast64_t>(this->statesSorted);
517 copiedOrder->statesToHandle = std::vector<uint_fast64_t>(this->statesToHandle);
518 copiedOrder->trivialStates = storm::storage::BitVector(trivialStates);
519 copiedOrder->doneStates = storm::storage::BitVector(doneStates);
520 copiedOrder->numberOfAddedStates = this->numberOfAddedStates;
521 copiedOrder->doneBuilding = this->doneBuilding;
522
523 auto seenStates = storm::storage::BitVector(numberOfStates, false);
524 // copy nodes
525 for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
526 Node* oldNode = nodes.at(state);
527 if (oldNode != nullptr) {
528 if (!seenStates[*(oldNode->states.begin())]) {
529 Node* newNode = new Node();
530 if (oldNode == this->getTop()) {
531 copiedOrder->top = newNode;
532 } else if (oldNode == this->getBottom()) {
533 copiedOrder->bottom = newNode;
534 }
536 for (size_t i = 0; i < oldNode->statesAbove.size(); ++i) {
537 assert(newNode->statesAbove[i] == oldNode->statesAbove[i]);
538 }
539 for (auto const& i : oldNode->states) {
540 assert(!seenStates[i]);
541 newNode->states.insert(i);
542 seenStates.set(i);
543 copiedOrder->nodes[i] = newNode;
544 }
545 }
546 } else {
547 assert(copiedOrder->nodes[state] == nullptr);
548 }
549 }
550
551 return copiedOrder;
552}
553
554/*** Setters ***/
555void Order::setDoneState(uint_fast64_t stateNumber) {
556 doneStates.set(stateNumber);
557}
558
559/*** Output ***/
560
561void Order::toDotOutput() const {
562 // Graphviz Output start
563 STORM_PRINT("Dot Output:\n" << "digraph model {\n");
564
565 // Vertices of the digraph
566 storm::storage::BitVector stateCoverage = storm::storage::BitVector(doneStates);
567 for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
568 if (nodes[i] != nullptr) {
569 stateCoverage.set(i);
570 }
571 }
572 for (uint_fast64_t i = stateCoverage.getNextSetIndex(0); i != numberOfStates; i = stateCoverage.getNextSetIndex(i + 1)) {
573 for (uint_fast64_t j = i + 1; j < numberOfStates; j++) {
574 if (getNode(j) == getNode(i))
575 stateCoverage.set(j, false);
576 }
577 STORM_PRINT("\t" << nodeName(*getNode(i)) << " [ label = \"" << nodeLabel(*getNode(i)) << "\" ];\n");
578 }
579
580 // Edges of the digraph
581 for (uint_fast64_t i = stateCoverage.getNextSetIndex(0); i != numberOfStates; i = stateCoverage.getNextSetIndex(i + 1)) {
582 storm::storage::BitVector v = storm::storage::BitVector(numberOfStates, false);
583 Node* currentNode = getNode(i);
584 for (uint_fast64_t s1 : getNode(i)->statesAbove) {
585 v |= (currentNode->statesAbove & getNode(s1)->statesAbove);
586 }
587
588 std::set<Node*> seenNodes;
589 for (uint_fast64_t state : currentNode->statesAbove) {
590 Node* n = getNode(state);
591 if (std::find(seenNodes.begin(), seenNodes.end(), n) == seenNodes.end()) {
592 seenNodes.insert(n);
593 if (!v[state]) {
594 STORM_PRINT("\t" << nodeName(*currentNode) << " -> " << nodeName(*getNode(state)) << ";\n");
595 }
596 }
597 }
598 }
599 // Graphviz Output end
600 STORM_PRINT("}\n");
601}
602
603void Order::dotOutputToFile(std::ofstream& dotOutfile) const {
604 // Graphviz Output start
605 dotOutfile << "Dot Output:\n"
606 << "digraph model {\n";
607
608 // Vertices of the digraph
609 storm::storage::BitVector stateCoverage = storm::storage::BitVector(numberOfStates, true);
610 for (uint_fast64_t i = stateCoverage.getNextSetIndex(0); i != numberOfStates; i = stateCoverage.getNextSetIndex(i + 1)) {
611 if (getNode(i) == NULL) {
612 continue;
613 }
614 for (uint_fast64_t j = i + 1; j < numberOfStates; j++) {
615 if (getNode(j) == getNode(i))
616 stateCoverage.set(j, false);
617 }
618
619 dotOutfile << "\t" << nodeName(*getNode(i)) << " [ label = \"" << nodeLabel(*getNode(i)) << "\" ];\n";
620 }
621
622 // Edges of the digraph
623 for (uint_fast64_t i = stateCoverage.getNextSetIndex(0); i != numberOfStates; i = stateCoverage.getNextSetIndex(i + 1)) {
624 storm::storage::BitVector v = storm::storage::BitVector(numberOfStates, false);
625 Node* currentNode = getNode(i);
626 if (currentNode == NULL) {
627 continue;
628 }
629
630 for (uint_fast64_t s1 : getNode(i)->statesAbove) {
631 v |= (currentNode->statesAbove & getNode(s1)->statesAbove);
632 }
633
634 std::set<Node*> seenNodes;
635 for (uint_fast64_t state : currentNode->statesAbove) {
636 Node* n = getNode(state);
637 if (std::find(seenNodes.begin(), seenNodes.end(), n) == seenNodes.end()) {
638 seenNodes.insert(n);
639 if (!v[state]) {
640 dotOutfile << "\t" << nodeName(*currentNode) << " -> " << nodeName(*getNode(state)) << ";\n";
641 }
642 }
643 }
644 }
645
646 // Graphviz Output end
647 dotOutfile << "}\n";
648}
649
650/*** Private methods ***/
651
652void Order::init(uint_fast64_t numberOfStates, storage::Decomposition<storage::StronglyConnectedComponent> decomposition, bool doneBuilding) {
653 this->numberOfStates = numberOfStates;
654 this->invalid = false;
655 this->nodes = std::vector<Node*>(numberOfStates, nullptr);
656 this->doneStates = storm::storage::BitVector(numberOfStates, false);
657 assert(doneStates.getNumberOfSetBits() == 0);
658 if (decomposition.size() == 0) {
659 this->trivialStates = storm::storage::BitVector(numberOfStates, true);
660 } else {
661 this->trivialStates = storm::storage::BitVector(numberOfStates, false);
662 for (auto& scc : decomposition) {
663 if (scc.size() == 1) {
664 trivialStates.set(*(scc.begin()));
665 }
666 }
667 }
668 this->top = new Node();
669 this->bottom = new Node();
670 this->top->statesAbove = storm::storage::BitVector(numberOfStates, false);
671 this->bottom->statesAbove = storm::storage::BitVector(numberOfStates, false);
672 this->doneBuilding = doneBuilding;
673}
674
675bool Order::aboveFast(Node* node1, Node* node2) const {
676 bool found = false;
677 for (auto const& state : node1->states) {
678 found = ((node2->statesAbove))[state];
679 if (found) {
680 break;
681 }
682 }
683 return found;
684}
685
686bool Order::above(Node* node1, Node* node2) {
687 assert(!aboveFast(node1, node2));
688 // Check whether node1 is above node2 by going over all states that are above state 2
689 bool above = false;
690 // Only do this when we have to deal with forward reasoning or we are not yet done with the building of the order
691 if (!trivialStates.full() || !doneBuilding) {
692 // First gather all states that are above node 2;
693
694 storm::storage::BitVector statesSeen((node2->statesAbove));
695 std::queue<uint_fast64_t> statesToHandle;
696 for (auto state : statesSeen) {
697 statesToHandle.push(state);
698 }
699 while (!above && !statesToHandle.empty()) {
700 // Get first item from the queue
701 auto state = statesToHandle.front();
702 statesToHandle.pop();
703 auto node = getNode(state);
704 if (aboveFast(node1, node)) {
705 above = true;
706 continue;
707 }
708 for (auto newState : node->statesAbove) {
709 if (!statesSeen[newState]) {
710 statesToHandle.push(newState);
711 statesSeen.set(newState);
712 }
713 }
714 }
715 }
716 if (above) {
717 for (auto state : node1->states) {
718 node2->statesAbove.set(state);
719 }
720 }
721 return above;
722}
723
724std::string Order::nodeName(Node n) const {
725 auto itr = n.states.begin();
726 std::string name = "n" + std::to_string(*itr);
727 return name;
728}
729
730std::string Order::nodeLabel(Node n) const {
731 if (n.states == top->states)
732 return "=)";
733 if (n.states == bottom->states)
734 return "=(";
735 auto itr = n.states.begin();
736 std::string label = "s" + std::to_string(*itr);
737 ++itr;
738 if (itr != n.states.end())
739 label = "[" + label + "]";
740 return label;
741}
742
744 return !doneStates.full();
745}
746
747bool Order::isTrivial(uint_fast64_t state) {
748 return trivialStates[state];
749}
750
751std::pair<uint_fast64_t, bool> Order::getNextStateNumber() {
752 while (!statesSorted.empty()) {
753 auto state = statesSorted.back();
754 statesSorted.pop_back();
755 if (!doneStates[state]) {
756 return {state, true};
757 }
758 }
759 return {numberOfStates, true};
760}
761
762std::pair<uint_fast64_t, bool> Order::getStateToHandle() {
763 assert(existsStateToHandle());
764 auto state = statesToHandle.back();
765 statesToHandle.pop_back();
766 return {state, false};
767}
768
770 while (!statesToHandle.empty() && doneStates[statesToHandle.back()]) {
771 statesToHandle.pop_back();
772 }
773 return !statesToHandle.empty();
774}
775
776void Order::addStateToHandle(uint_fast64_t state) {
777 if (!doneStates[state]) {
778 statesToHandle.push_back(state);
779 }
780}
781
782void Order::addStateSorted(uint_fast64_t state) {
783 statesSorted.push_back(state);
784}
785
786std::pair<bool, bool> Order::allAboveBelow(std::vector<uint_fast64_t> const states, uint_fast64_t state) {
787 auto allAbove = true;
788 auto allBelow = true;
789 for (auto& checkState : states) {
790 auto comp = compare(checkState, state);
791 allAbove &= (comp == ABOVE || comp == SAME);
792 allBelow &= (comp == BELOW || comp == SAME);
793 }
794 return {allAbove, allBelow};
795}
796
797uint_fast64_t Order::getNumberOfDoneStates() const {
798 return doneStates.getNumberOfSetBits();
799}
800
801bool Order::isInvalid() const {
802 return invalid;
803}
804} // namespace analysis
805} // namespace storm
uint_fast64_t getNumberOfDoneStates() const
Definition Order.cpp:797
void addAbove(uint_fast64_t state, Node *node)
Adds a node with the given state above the given node.
Definition Order.cpp:73
bool isTrivial(uint_fast64_t state)
Definition Order.cpp:747
void addStateSorted(uint_fast64_t state)
Definition Order.cpp:782
Node * getBottom() const
Retrieves the bottom node of the order.
Definition Order.cpp:293
bool contains(uint_fast64_t state) const
Check if state is already contained in order.
Definition Order.cpp:289
bool isInvalid() const
Definition Order.cpp:801
Order::NodeComparison compareFast(uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis=UNKNOWN) const
Definition Order.cpp:241
Order::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis=UNKNOWN)
Compares the level of the nodes of the states.
Definition Order.cpp:237
std::pair< uint_fast64_t, bool > getStateToHandle()
Definition Order.cpp:762
std::vector< uint_fast64_t > & getStatesSorted()
Definition Order.cpp:315
std::vector< uint_fast64_t > sortStates(std::vector< uint_fast64_t > *states)
Sorts the given states if possible.
Definition Order.cpp:345
NodeComparison
Constants for comparison of nodes/states.
Definition Order.h:18
Order()
Constructs a new Order.
Definition Order.cpp:61
void toDotOutput() const
Prints the dot output to normal STORM_PRINT.
Definition Order.cpp:561
void dotOutputToFile(std::ofstream &dotOutfile) const
Writes dotoutput to the given file.
Definition Order.cpp:603
void addRelation(uint_fast64_t above, uint_fast64_t below, bool allowMerge=false)
Adds a new relation between two states to the order.
Definition Order.cpp:150
Node * getNode(uint_fast64_t state) const
Retrieves the pointer to a Node at which the state occurs.
Definition Order.cpp:306
bool merge(uint_fast64_t var1, uint_fast64_t var2)
Merges node of var2 into node of var1.
Definition Order.cpp:231
std::vector< Node * > getNodes() const
Returns the vector with the nodes of the order.
Definition Order.cpp:311
bool mergeNodes(Node *node1, Node *node2)
Merges node2 into node1.
Definition Order.cpp:192
std::pair< bool, bool > allAboveBelow(std::vector< uint_fast64_t > const states, uint_fast64_t state)
Definition Order.cpp:786
uint_fast64_t getNextDoneState(uint_fast64_t state) const
Returns the next done state of the order, returns the number of state if end of done states is reache...
Definition Order.cpp:302
bool getDoneBuilding() const
Returns true if done building the order.
Definition Order.cpp:297
void addToNode(uint_fast64_t state, Node *node)
Adds state to the states of the given node.
Definition Order.cpp:173
bool isTopState(uint_fast64_t) const
Checks if the given state is a top state.
Definition Order.cpp:336
std::pair< std::pair< uint_fast64_t, uint_fast64_t >, std::vector< uint_fast64_t > > sortStatesForForward(uint_fast64_t currentState, std::vector< uint_fast64_t > const &successors)
Sorts the given states if possible.
Definition Order.cpp:383
std::pair< std::pair< uint_fast64_t, uint_fast64_t >, std::vector< uint_fast64_t > > sortStatesUnorderedPair(const std::vector< uint_fast64_t > *states)
Sorts the given states if possible.
Definition Order.cpp:436
void addStateToHandle(uint_fast64_t state)
Definition Order.cpp:776
void addBetween(uint_fast64_t state, Node *node1, Node *node2)
Adds a node with the given state below node1 and above node2.
Definition Order.cpp:113
uint_fast64_t getNumberOfStates() const
Returns the number of possible states in the order.
Definition Order.cpp:327
void addBelow(uint_fast64_t state, Node *node)
Adds a node with the given state below the given node.
Definition Order.cpp:93
void setDoneState(uint_fast64_t sccNumber)
Definition Order.cpp:555
std::pair< uint_fast64_t, bool > getNextStateNumber()
Definition Order.cpp:751
std::shared_ptr< Order > copy() const
Creates a copy of the calling Order.
Definition Order.cpp:510
bool isOnlyBottomTopOrder() const
Returns if the order only consists of bottom and top states (so no in-between nodes).
Definition Order.cpp:341
uint_fast64_t getNumberOfAddedStates() const
Returns the number of added states.
Definition Order.cpp:323
bool isBottomState(uint_fast64_t) const
Checks if the given state is a bottom state.
Definition Order.cpp:331
Node * getTop() const
Retrieves the top node of the order.
Definition Order.cpp:319
void add(uint_fast64_t state)
Adds state between the top and bottom node of the order.
Definition Order.cpp:67
void addRelationNodes(storm::analysis::Order::Node *above, storm::analysis::Order::Node *below, bool allowMerge=false)
Adds a new relation between two nodes to the order.
Definition Order.cpp:155
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
uint64_t getNextSetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
bool full() const
Retrieves whether all bits are set in this bit vector.
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
size_t size() const
Retrieves the number of bits this bit vector can store.
This class represents the decomposition of a model into blocks which are of the template type.
std::size_t size() const
Retrieves the number of blocks of this decomposition.
#define STORM_LOG_INFO(message)
Definition logging.h:24
#define STORM_PRINT(message)
Define the macros that print information and optionally also log it.
Definition macros.h:62
LabParser.cpp.
Nodes of the Reachability Order.
Definition Order.h:28
boost::container::flat_set< uint_fast64_t > states
Definition Order.h:29
storm::storage::BitVector statesAbove
Definition Order.h:30