Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExplicitQuantitativeResult.cpp
Go to the documentation of this file.
2
4
6
9
10namespace storm::gbar {
11namespace abstraction {
12
13template<typename ValueType>
14ExplicitQuantitativeResult<ValueType>::ExplicitQuantitativeResult(uint64_t numberOfStates) : values(numberOfStates) {
15 // Intentionally left empty.
16}
17
18template<typename ValueType>
19ExplicitQuantitativeResult<ValueType>::ExplicitQuantitativeResult(std::vector<ValueType>&& values) : values(std::move(values)) {
20 // Intentionally left empty.
21}
22
23template<typename ValueType>
24std::vector<ValueType> const& ExplicitQuantitativeResult<ValueType>::getValues() const {
25 return values;
26}
27
28template<typename ValueType>
30 return values;
31}
32
33template<typename ValueType>
34void ExplicitQuantitativeResult<ValueType>::setValue(uint64_t state, ValueType const& value) {
35 values[state] = value;
36}
37
38template<typename ValueType>
39std::pair<ValueType, ValueType> ExplicitQuantitativeResult<ValueType>::getRange(storm::storage::BitVector const& states) const {
40 STORM_LOG_THROW(!states.empty(), storm::exceptions::InvalidArgumentException, "Expected non-empty set of states.");
41
42 auto stateIt = states.begin();
43 std::pair<ValueType, ValueType> result = std::make_pair(values[*stateIt], values[*stateIt]);
44 ++stateIt;
45
46 while (stateIt != states.end()) {
47 if (values[*stateIt] < result.first) {
48 result.first = values[*stateIt];
49 } else if (values[*stateIt] < result.first) {
50 result.second = values[*stateIt];
51 }
52
53 ++stateIt;
54 }
55
56 return result;
57}
58
61} // namespace abstraction
62} // namespace storm::gbar
std::pair< ValueType, ValueType > getRange(storm::storage::BitVector const &states) const
void setValue(uint64_t state, ValueType const &value)
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30