Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
permutation.cpp
Go to the documentation of this file.
2
3#include <algorithm>
4#include <deque>
5#include <numeric>
6#include <random>
7
13
15
19std::string orderKindtoString(OrderKind order) {
20 switch (order) {
21 case OrderKind::Bfs:
22 return "bfs";
23 case OrderKind::Dfs:
24 return "dfs";
26 return "reverse-bfs";
28 return "reverse-dfs";
30 return "random";
31 }
32 STORM_LOG_ASSERT(false, "unreachable");
33 return "";
34}
35
36OrderKind orderKindFromString(std::string const& order) {
38 if (order == orderKindtoString(kind)) {
39 return kind;
40 }
41 }
42 STORM_LOG_ASSERT(false, "Unknown order kind");
43 return OrderKind::Bfs;
44}
45
46std::vector<std::string> orderKinds() {
47 std::vector<std::string> kinds;
49 kinds.push_back(orderKindtoString(kind));
50 }
51 return kinds;
52}
53
54std::vector<index_type> createRandomPermutation(index_type size) {
55 std::random_device rd;
56 return createRandomPermutation(size, rd());
57}
58
59std::vector<index_type> createRandomPermutation(index_type size, index_type seed) {
60 std::vector<index_type> permutation(size);
61 std::iota(permutation.begin(), permutation.end(), 0);
62 // The random number engine below assumes that it operates on 64-bit unsigned integers.
63 static_assert(std::is_same_v<index_type, uint64_t>, "index_type is assumed to be a 64-bit unsigned integer");
64 std::shuffle(permutation.begin(), permutation.end(), std::mt19937_64(seed));
65 return permutation;
66}
67
68template<typename ValueType>
69std::vector<index_type> createPermutation(OrderKind order, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
70 storm::storage::BitVector const& initialStates) {
71 if (order == OrderKind::Random) {
72 return createRandomPermutation(transitionMatrix.getRowGroupCount());
73 }
75 "Unknown order kind");
76 STORM_LOG_ASSERT(initialStates.size() == transitionMatrix.getRowGroupCount(), "Unexpected dimensions of initial states and transition matrix.");
77 STORM_LOG_ASSERT(initialStates.size() == transitionMatrix.getColumnCount(), "Unexpected dimensions of initial states and transition matrix.");
78 std::vector<index_type> permutation;
79 permutation.reserve(transitionMatrix.getRowGroupCount());
80
81 std::deque<index_type> stack(initialStates.begin(), initialStates.end());
82 storm::storage::BitVector discoveredStates = initialStates;
83 bool const useFifoStack = order == OrderKind::Bfs || order == OrderKind::ReverseBfs;
84
85 while (!stack.empty()) {
86 auto current = stack.front();
87 stack.pop_front();
88 permutation.push_back(current);
89 for (auto const& entry : transitionMatrix.getRowGroup(current)) {
90 if (auto const successor = entry.getColumn(); !discoveredStates.get(successor)) {
91 discoveredStates.set(successor, true);
92 if (useFifoStack) {
93 stack.push_back(successor);
94 } else {
95 stack.push_front(successor);
96 }
97 }
98 }
99 }
100 if (order == OrderKind::ReverseDfs || order == OrderKind::ReverseBfs) {
101 reversePermutationInPlace(permutation);
102 }
103 return permutation;
104}
105
106std::vector<index_type> invertPermutation(std::vector<index_type> const& permutation) {
107 std::vector<index_type> inverted(permutation.size());
108 for (index_type i = 0; i < permutation.size(); ++i) {
109 inverted[permutation[i]] = i;
110 }
111 return inverted;
112}
113
114void reversePermutationInPlace(std::vector<index_type>& permutation) {
115 auto const max = permutation.size() - 1;
116 for (auto& i : permutation) {
117 i = max - i;
118 }
119}
120
121bool isValidPermutation(std::vector<index_type> const& permutation) {
122 storage::BitVector occurring(permutation.size(), false);
123 for (auto i : permutation) {
124 if (occurring.get(i)) {
125 return false;
126 }
127 occurring.set(i, true);
128 }
129 return occurring.full();
130}
131
132template std::vector<index_type> createPermutation(OrderKind order, storm::storage::SparseMatrix<double> const& transitionMatrix,
133 storm::storage::BitVector const& initialStates);
134template std::vector<index_type> createPermutation(OrderKind order, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix,
135 storm::storage::BitVector const& initialStates);
136template std::vector<index_type> createPermutation(OrderKind order, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix,
137 storm::storage::BitVector const& initialStates);
138
139} // namespace storm::utility::permutation
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
bool full() const
Retrieves whether all bits are set in this bit vector.
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
void set(uint_fast64_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.
bool get(uint_fast64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
A class that holds a possibly non-square matrix in the compressed row storage format.
const_rows getRowGroup(index_type rowGroup) const
Returns an object representing the given row group.
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
index_type getColumnCount() const
Returns the number of columns of the matrix.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
OrderKind
The order in which the states of a matrix are visited in a depth-first search or breadth-first search...
Definition permutation.h:21
std::vector< index_type > createRandomPermutation(index_type size)
Creates a random (uniformly distributed) permutation of the given size.
std::string orderKindtoString(OrderKind order)
Converts the given order to a string.
std::vector< index_type > createPermutation(OrderKind order, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates)
Creates a permutation that orders the states of the given matrix in the given exploration order.
void reversePermutationInPlace(std::vector< index_type > &permutation)
Reverses the given permutation.
std::vector< index_type > invertPermutation(std::vector< index_type > const &permutation)
Inverts the given permutation.
std::vector< std::string > orderKinds()
Returns a list of possible order kinds.
OrderKind orderKindFromString(std::string const &order)
Gets the order from the given string.
bool isValidPermutation(std::vector< index_type > const &permutation)
Returns true if the given vector is a permutation of the numbers 0, 1, ..., n-1 for n = permutation....
ValueType max(ValueType const &first, ValueType const &second)