Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SparseCbQuery.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4
8
9namespace storm {
10
11class Environment;
12
13namespace modelchecker {
14namespace multiobjective {
15
16/*
17 * This class represents a multi-objective query for the constraint based approach (using SMT or LP solvers).
18 */
19template<class SparseModelType>
21 public:
22 virtual ~SparseCbQuery() = default;
23
24 /*
25 * Invokes the computation and retrieves the result
26 */
27 virtual std::unique_ptr<CheckResult> check(Environment const& env) = 0;
28
29 protected:
31
32 SparseModelType const& originalModel;
34 std::vector<Objective<typename SparseModelType::ValueType>> objectives;
35 std::shared_ptr<SparseModelType> preprocessedModel;
37 std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
38};
39
40} // namespace multiobjective
41} // namespace modelchecker
42} // namespace storm
std::shared_ptr< storm::expressions::ExpressionManager > expressionManager
storm::logic::MultiObjectiveFormula const & originalFormula
std::shared_ptr< SparseModelType > preprocessedModel
virtual std::unique_ptr< CheckResult > check(Environment const &env)=0
std::vector< Objective< typename SparseModelType::ValueType > > objectives
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
LabParser.cpp.
Definition cli.cpp:18