Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DeterministicSchedsAchievabilityChecker.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4#include <optional>
5#include <vector>
6
7namespace storm {
8class Environment;
9
10namespace modelchecker {
11
12class CheckResult;
13
14namespace multiobjective {
15template<typename SparseModelType, typename GeometryValueType>
16class DeterministicSchedsLpChecker;
17
18template<typename SparseModelType>
19class DeterministicSchedsObjectiveHelper;
20
21namespace preprocessing {
22template<typename SparseModelType>
24}
25
26template<class SparseModelType, typename GeometryValueType>
28 public:
29 typedef typename SparseModelType::ValueType ModelValueType;
30
32
33 virtual std::unique_ptr<CheckResult> check(Environment const& env);
34
35 private:
36 std::shared_ptr<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>> lpChecker;
37 std::vector<DeterministicSchedsObjectiveHelper<SparseModelType>> objectiveHelper;
38
39 std::shared_ptr<SparseModelType> model;
40 uint64_t const originalModelInitialState;
41 std::optional<uint64_t> optimizingObjectiveIndex;
42};
43
44} // namespace multiobjective
45} // namespace modelchecker
46} // namespace storm
LabParser.cpp.
Definition cli.cpp:18