dehnert
7 years ago
11 changed files with 246 additions and 205 deletions
-
5src/storm-cli-utilities/model-handling.h
-
37src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
-
158src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
20src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
-
6src/storm/solver/LinearEquationSolverRequirements.cpp
-
1src/storm/solver/LinearEquationSolverRequirements.h
-
6src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
-
1src/storm/solver/MinMaxLinearEquationSolverRequirements.h
-
7src/storm/solver/NativeLinearEquationSolver.cpp
-
81src/storm/storage/ConsecutiveUint64DynamicPriorityQueue.h
-
99src/storm/storage/VectorDynamicPriorityQueue.h
@ -0,0 +1,81 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include <algorithm> |
||||
|
#include <vector> |
||||
|
|
||||
|
#include "storm/utility/macros.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace storage { |
||||
|
|
||||
|
template<typename Compare = std::less<uint64_t>> |
||||
|
class ConsecutiveUint64DynamicPriorityQueue { |
||||
|
public: |
||||
|
typedef uint64_t T; |
||||
|
typedef std::vector<T> Container; |
||||
|
|
||||
|
private: |
||||
|
Container container; |
||||
|
Compare compare; |
||||
|
|
||||
|
std::vector<uint64_t> positions; |
||||
|
|
||||
|
public: |
||||
|
explicit ConsecutiveUint64DynamicPriorityQueue(uint64_t numberOfIntegers, Compare const& compare) : container(numberOfIntegers), compare(compare), positions(numberOfIntegers) { |
||||
|
std::iota(container.begin(), container.end(), 0); |
||||
|
} |
||||
|
|
||||
|
void fix() { |
||||
|
std::make_heap(container.begin(), container.end(), compare); |
||||
|
} |
||||
|
|
||||
|
void increase(uint64_t element) { |
||||
|
uint64_t position = positions[element]; |
||||
|
if (position >= container.size()) { |
||||
|
return; |
||||
|
} |
||||
|
|
||||
|
uint64_t parentPosition = (position - 1) / 2; |
||||
|
while (position > 0 && compare(container[parentPosition], container[position])) { |
||||
|
std::swap(container[parentPosition], container[position]); |
||||
|
std::swap(positions[container[parentPosition]], positions[container[position]]); |
||||
|
|
||||
|
position = parentPosition; |
||||
|
parentPosition = (position - 1) / 2; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
bool contains(uint64_t element) const { |
||||
|
return positions[element] < container.size(); |
||||
|
} |
||||
|
|
||||
|
bool empty() const { |
||||
|
return container.empty(); |
||||
|
} |
||||
|
|
||||
|
std::size_t size() const { |
||||
|
return container.size(); |
||||
|
} |
||||
|
|
||||
|
const T& top() const { |
||||
|
return container.front(); |
||||
|
} |
||||
|
|
||||
|
void push(uint64_t const& item) { |
||||
|
container.emplace_back(item); |
||||
|
std::push_heap(container.begin(), container.end(), compare); |
||||
|
} |
||||
|
|
||||
|
void pop() { |
||||
|
std::pop_heap(container.begin(), container.end(), compare); |
||||
|
container.pop_back(); |
||||
|
} |
||||
|
|
||||
|
T popTop() { |
||||
|
T item = top(); |
||||
|
pop(); |
||||
|
return item; |
||||
|
} |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
@ -1,99 +0,0 @@ |
|||||
#ifndef STORM_STORAGE_DYNAMICPRIORITYQUEUE_H_ |
|
||||
#define STORM_STORAGE_DYNAMICPRIORITYQUEUE_H_ |
|
||||
|
|
||||
#include <algorithm> |
|
||||
#include <vector> |
|
||||
|
|
||||
#include "storm/utility/macros.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
namespace storage { |
|
||||
|
|
||||
template<typename Compare = std::less<uint64_t>> |
|
||||
class VectorDynamicPriorityQueue { |
|
||||
public: |
|
||||
typedef uint64_t T; |
|
||||
typedef std::vector<T> Container; |
|
||||
|
|
||||
private: |
|
||||
Container container; |
|
||||
Compare compare; |
|
||||
|
|
||||
std::vector<uint64_t> positions; |
|
||||
uint64_t upperBound; |
|
||||
|
|
||||
uint64_t numberOfSortedEntriesAtBack; |
|
||||
|
|
||||
uint64_t const NUMBER_OF_ENTRIES_TO_SORT = 100; |
|
||||
|
|
||||
public: |
|
||||
explicit DynamicPriorityQueue(Compare const& compare, uint64_t upperBound) : container(), compare(compare), positions(upperBound) { |
|
||||
// Intentionally left empty |
|
||||
} |
|
||||
|
|
||||
explicit DynamicPriorityQueue(Container&& container, Compare const& compare) : container(std::move(container)), compare(compare), positions(this->container.size()) { |
|
||||
sortAndUpdatePositions(container.begin(), container.end()); |
|
||||
} |
|
||||
|
|
||||
void fix() { |
|
||||
sortAndUpdatePositions(container.begin(), container.end()); |
|
||||
} |
|
||||
|
|
||||
bool empty() const { |
|
||||
return container.empty(); |
|
||||
} |
|
||||
|
|
||||
std::size_t size() const { |
|
||||
return container.size(); |
|
||||
} |
|
||||
|
|
||||
const T& top() const { |
|
||||
return container.front(); |
|
||||
} |
|
||||
|
|
||||
template<typename TemplateType> |
|
||||
void push(TemplateType&& item) { |
|
||||
if (this->empty() || container.back() < item) { |
|
||||
container.emplace_back(std::forward<TemplateType>(item)); |
|
||||
} else { |
|
||||
|
|
||||
} |
|
||||
} |
|
||||
|
|
||||
void pop() { |
|
||||
container.pop_back(); |
|
||||
--numberOfSortedEntriesAtBack; |
|
||||
if (numberOfSortedEntriesAtBack == 0) { |
|
||||
if (container.size() > NUMBER_OF_ENTRIES_TO_SORT) { |
|
||||
sortAndUpdatePositions(container.end() - NUMBER_OF_ENTRIES_TO_SORT, container.end()); |
|
||||
numberOfSortedEntriesAtBack = NUMBER_OF_ENTRIES_TO_SORT; |
|
||||
} else { |
|
||||
sortAndUpdatePositions(container.begin(), container.end()); |
|
||||
numberOfSortedEntriesAtBack = container.size(); |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
T popTop() { |
|
||||
T item = top(); |
|
||||
pop(); |
|
||||
return item; |
|
||||
} |
|
||||
|
|
||||
private: |
|
||||
void sortAndUpdatePositions(Container::const_iterator start, Container::const_iterator end) { |
|
||||
std::sort(start, end); |
|
||||
updatePositions(start, end); |
|
||||
} |
|
||||
|
|
||||
void updatePositions(Container::const_iterator start, Container::const_iterator end) { |
|
||||
for (; start != end; ++start) { |
|
||||
position = std::distance(container.begin(), start); |
|
||||
positions[container[position]] = position; |
|
||||
} |
|
||||
} |
|
||||
}; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
#endif // STORM_STORAGE_DYNAMICPRIORITYQUEUE_H_ |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue