|
@ -9,31 +9,34 @@ namespace storm { |
|
|
namespace storage { |
|
|
namespace storage { |
|
|
class BitVector; |
|
|
class BitVector; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
namespace modelchecker { |
|
|
namespace modelchecker { |
|
|
namespace helper { |
|
|
namespace helper { |
|
|
template<typename ValueType> |
|
|
template<typename ValueType> |
|
|
struct MDPSparseModelCheckingHelperReturnType { |
|
|
struct MDPSparseModelCheckingHelperReturnType { |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete; |
|
|
MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete; |
|
|
MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default; |
|
|
MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
MDPSparseModelCheckingHelperReturnType(std::vector<ValueType>&& values, std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { |
|
|
MDPSparseModelCheckingHelperReturnType(std::vector<ValueType>&& values, std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { |
|
|
// Intentionally left empty. |
|
|
// Intentionally left empty. |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
virtual ~MDPSparseModelCheckingHelperReturnType() { |
|
|
virtual ~MDPSparseModelCheckingHelperReturnType() { |
|
|
// Intentionally left empty. |
|
|
// Intentionally left empty. |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// The values computed for the states. |
|
|
// The values computed for the states. |
|
|
std::vector<ValueType> values; |
|
|
std::vector<ValueType> values; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// The values computed for the available choices. |
|
|
|
|
|
std::vector<ValueType> choiceValues; |
|
|
|
|
|
|
|
|
// A scheduler, if it was computed. |
|
|
// A scheduler, if it was computed. |
|
|
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler; |
|
|
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler; |
|
|
}; |
|
|
}; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|