47 std::vector<std::string> kinds;
55 std::random_device rd;
60 std::vector<index_type> permutation(size);
61 std::iota(permutation.begin(), permutation.end(), 0);
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));
68template<
typename ValueType>
75 "Unknown order kind");
78 std::vector<index_type> permutation;
81 std::deque<index_type> stack(initialStates.
begin(), initialStates.
end());
85 while (!stack.empty()) {
86 auto current = stack.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);
93 stack.push_back(successor);
95 stack.push_front(successor);
107 std::vector<index_type> inverted(permutation.size());
108 for (
index_type i = 0; i < permutation.size(); ++i) {
109 inverted[permutation[i]] = i;
115 auto const max = permutation.size() - 1;
116 for (
auto& i : permutation) {
123 for (
auto i : permutation) {
124 if (occurring.
get(i)) {
127 occurring.
set(i,
true);
129 return occurring.
full();
A bit vector that is internally represented as a vector of 64-bit values.
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)
OrderKind
The order in which the states of a matrix are visited in a depth-first search or breadth-first search...
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)