Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Engine.cpp
Go to the documentation of this file.
1#include "storm/utility/Engine.h"
2
3#include "storm/adapters/RationalFunctionAdapter.h"
4#include "storm/exceptions/InvalidArgumentException.h"
5#include "storm/modelchecker/CheckTask.h"
6#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h"
7#include "storm/modelchecker/csl/HybridMarkovAutomatonCslModelChecker.h"
8#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
9#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
10#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
11#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
12#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
13#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
14#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
15#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
16#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
17#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h"
18#include "storm/models/sparse/StandardRewardModel.h"
19#include "storm/models/symbolic/MarkovAutomaton.h"
20#include "storm/models/symbolic/StandardRewardModel.h"
21#include "storm/storage/SymbolicModelDescription.h"
22#include "storm/storage/jani/Property.h"
23#include "storm/utility/macros.h"
24
25namespace storm {
26namespace utility {
27
28// Returns a list of all available engines (excluding Unknown)
29std::vector<Engine> getEngines() {
30 std::vector<Engine> res;
31 for (int i = 0; i != static_cast<int>(Engine::Unknown); ++i) {
32 res.push_back(static_cast<Engine>(i));
33 }
34 return res;
35}
36
37std::string toString(Engine const& engine) {
38 switch (engine) {
39 case Engine::Sparse:
40 return "sparse";
41 case Engine::Hybrid:
42 return "hybrid";
43 case Engine::Dd:
44 return "dd";
45 case Engine::DdSparse:
46 return "dd-to-sparse";
47 case Engine::Exploration:
48 return "expl";
49 case Engine::AbstractionRefinement:
50 return "abs";
51 case Engine::Automatic:
52 return "automatic";
53 case Engine::Unknown:
54 return "UNKNOWN";
55 default:
56 STORM_LOG_ASSERT(false, "The given engine has no name assigned to it.");
57 return "UNKNOWN";
58 }
59}
60
61std::ostream& operator<<(std::ostream& os, Engine const& engine) {
62 os << toString(engine);
63 return os;
64}
65
66Engine engineFromString(std::string const& engineStr) {
67 for (Engine const& e : getEngines()) {
68 if (engineStr == toString(e)) {
69 return e;
70 }
71 }
72 if (engineStr == "portfolio") {
73 STORM_LOG_WARN("The engine name \"portfolio\" is deprecated. The name of this engine has been changed to \"" << toString(Engine::Automatic) << "\".");
74 return Engine::Automatic;
75 }
76 STORM_LOG_ERROR("The engine '" << engineStr << "' was not found.");
77 return Engine::Unknown;
78}
79
80storm::builder::BuilderType getBuilderType(Engine const& engine) {
81 switch (engine) {
82 case Engine::Sparse:
83 return storm::builder::BuilderType::Explicit;
84 case Engine::Hybrid:
85 return storm::builder::BuilderType::Dd;
86 case Engine::Dd:
87 return storm::builder::BuilderType::Dd;
88 case Engine::DdSparse:
89 return storm::builder::BuilderType::Dd;
90 case Engine::Exploration:
91 return storm::builder::BuilderType::Explicit;
92 case Engine::AbstractionRefinement:
93 return storm::builder::BuilderType::Dd;
94 default:
95 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given engine has no builder type to it.");
96 return storm::builder::BuilderType::Explicit;
97 }
98}
99
100template<typename ValueType>
101bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription::ModelType const& modelType,
102 storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
103 // Define types to improve readability
104 typedef storm::storage::SymbolicModelDescription::ModelType ModelType;
105 // The Dd library does not make much of a difference (in case of exact or parametric models we will switch to sylvan anyway).
106 // Therefore, we always use sylvan here
107 storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
108 switch (engine) {
109 case Engine::Sparse:
110 case Engine::DdSparse:
111 switch (modelType) {
112 case ModelType::DTMC:
113 return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>>::canHandleStatic(checkTask);
114 case ModelType::MDP:
115 return storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>>::canHandleStatic(checkTask);
116 case ModelType::CTMC:
117 return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>>::canHandleStatic(checkTask);
118 case ModelType::MA:
119 return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::canHandleStatic(
120 checkTask);
121 case ModelType::POMDP:
122 return false;
123 case ModelType::SMG:
124 return storm::modelchecker::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>>::canHandleStatic(checkTask);
125 }
126 break;
127 case Engine::Hybrid:
128 switch (modelType) {
129 case ModelType::DTMC:
130 return storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
131 case ModelType::MDP:
132 return storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask);
133 case ModelType::CTMC:
134 return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, ValueType>>::canHandleStatic(checkTask);
135 case ModelType::MA:
136 return storm::modelchecker::HybridMarkovAutomatonCslModelChecker<
137 storm::models::symbolic::MarkovAutomaton<ddType, ValueType>>::canHandleStatic(checkTask);
138 case ModelType::POMDP:
139 case ModelType::SMG:
140 return false;
141 }
142 break;
143 case Engine::Dd:
144 switch (modelType) {
145 case ModelType::DTMC:
146 return storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
147 case ModelType::MDP:
148 return storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask);
149 case ModelType::CTMC:
150 case ModelType::MA:
151 case ModelType::POMDP:
152 case ModelType::SMG:
153 return false;
154 }
155 break;
156 case Engine::Exploration:
157 if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
158 return false;
159 }
160 switch (modelType) {
161 case ModelType::DTMC:
162 return storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Dtmc<ValueType>>::canHandleStatic(checkTask);
163 case ModelType::MDP:
164 return storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<ValueType>>::canHandleStatic(checkTask);
165 case ModelType::CTMC:
166 case ModelType::MA:
167 case ModelType::POMDP:
168 case ModelType::SMG:
169 return false;
170 }
171 break;
172 case Engine::AbstractionRefinement:
173 if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
174 return false;
175 }
176 switch (modelType) {
177 case ModelType::DTMC:
178 case ModelType::MDP:
179 // Since the corresponding model checker is in a separate library, we can only make a very crude over-approximation of what can be handled
180 // at this point.
181 return true;
182 case ModelType::CTMC:
183 case ModelType::MA:
184 case ModelType::POMDP:
185 case ModelType::SMG:
186 return false;
187 }
188 break;
189 default:
190 STORM_LOG_ERROR("The selected engine " << engine << " is not considered.");
191 }
192 STORM_LOG_ERROR("The selected combination of engine (" << engine << ") and model type (" << modelType
193 << ") does not seem to be supported for this value type.");
194 return false;
195}
196
197template<>
198bool canHandle<storm::RationalFunction>(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription::ModelType const& modelType,
199 storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> const& checkTask) {
200 // Define types to improve readability
201 typedef storm::storage::SymbolicModelDescription::ModelType ModelType;
202 // The Dd library does not make much of a difference (in case of exact or parametric models we will switch to sylvan anyway).
203 // Therefore, we always use sylvan here
204 storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
205 switch (engine) {
206 case Engine::Sparse:
207 case Engine::DdSparse:
208 switch (modelType) {
209 case ModelType::DTMC:
210 return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>::canHandleStatic(checkTask);
211 case ModelType::CTMC:
212 return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>::canHandleStatic(checkTask);
213 case ModelType::MDP:
214 case ModelType::MA:
215 case ModelType::POMDP:
216 case ModelType::SMG:
217 return false;
218 }
219 break;
220 case Engine::Hybrid:
221 switch (modelType) {
222 case ModelType::DTMC:
223 return storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, storm::RationalFunction>>::canHandleStatic(
224 checkTask);
225 case ModelType::CTMC:
226 return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, storm::RationalFunction>>::canHandleStatic(
227 checkTask);
228 case ModelType::MDP:
229 case ModelType::MA:
230 case ModelType::POMDP:
231 case ModelType::SMG:
232 return false;
233 }
234 break;
235 case Engine::Dd:
236 switch (modelType) {
237 case ModelType::DTMC:
238 return storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, storm::RationalFunction>>::canHandleStatic(
239 checkTask);
240 case ModelType::MDP:
241 case ModelType::CTMC:
242 case ModelType::MA:
243 case ModelType::POMDP:
244 case ModelType::SMG:
245 return false;
246 }
247 break;
248 case Engine::Exploration:
249 case Engine::AbstractionRefinement:
250 return false;
251 default:
252 STORM_LOG_ERROR("The selected engine" << engine << " is not considered.");
253 }
254 STORM_LOG_ERROR("The selected combination of engine (" << engine << ") and model type (" << modelType
255 << ") does not seem to be supported for this value type.");
256 return false;
257}
258
259template<typename ValueType>
260bool canHandle(storm::utility::Engine const& engine, std::vector<storm::jani::Property> const& properties,
261 storm::storage::SymbolicModelDescription const& modelDescription) {
262 auto canHandleFormula = [&engine, &modelDescription](auto const& formula, bool onlyInitialStatesRelevant) {
263 auto task = storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(formula, onlyInitialStatesRelevant);
264 bool result = canHandle(engine, modelDescription.getModelType(), task);
265 STORM_LOG_INFO_COND(result, "Engine " << engine << " can not handle formula '" << task.getFormula() << "' on models of type "
266 << modelDescription.getModelType() << ".");
267 return result;
268 };
269 auto canHandleProperty = [&canHandleFormula](auto const& property) {
270 if (property.getFilter().isDefault()) {
271 return canHandleFormula(*property.getRawFormula(), true);
272 } else {
273 return canHandleFormula(*property.getRawFormula(), false) && canHandleFormula(*property.getFilter().getStatesFormula(), false);
274 }
275 };
276 return std::all_of(properties.begin(), properties.end(), canHandleProperty) &&
277 storm::builder::canHandle<ValueType>(getBuilderType(engine), modelDescription, properties);
278}
279
280// explicit template instantiations.
281template bool canHandle<double>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&, storm::storage::SymbolicModelDescription const&);
282template bool canHandle<storm::RationalNumber>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&,
283 storm::storage::SymbolicModelDescription const&);
284template bool canHandle<storm::RationalFunction>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&,
285 storm::storage::SymbolicModelDescription const&);
286
287} // namespace utility
288} // namespace storm
storm::models::symbolic::MarkovAutomaton
This class represents a discrete-time Markov decision process.
Definition MarkovAutomaton.h:13
STORM_LOG_WARN
#define STORM_LOG_WARN(message)
Definition logging.h:25
STORM_LOG_ERROR
#define STORM_LOG_ERROR(message)
Definition logging.h:26
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
STORM_LOG_INFO_COND
#define STORM_LOG_INFO_COND(cond, message)
Definition macros.h:45
storm::utility::canHandle< storm::RationalFunction >
bool canHandle< storm::RationalFunction >(storm::utility::Engine const &engine, storm::storage::SymbolicModelDescription::ModelType const &modelType, storm::modelchecker::CheckTask< storm::logic::Formula, storm::RationalFunction > const &checkTask)
Definition Engine.cpp:198
storm::utility::Engine
Engine
An enumeration of all engines.
Definition Engine.h:31
storm::utility::canHandle< storm::RationalNumber >
template bool canHandle< storm::RationalNumber >(storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)
storm::utility::canHandle< double >
template bool canHandle< double >(storm::utility::Engine const &, std::vector< storm::jani::Property > const &, storm::storage::SymbolicModelDescription const &)
storm::utility::getBuilderType
storm::builder::BuilderType getBuilderType(Engine const &engine)
Returns the builder type used for the given engine.
Definition Engine.cpp:80
storm::utility::toString
std::string toString(Engine const &engine)
Returns a string representation of the given engine.
Definition Engine.cpp:37
storm::utility::getEngines
std::vector< Engine > getEngines()
Returns a list of all available engines (excluding Unknown)
Definition Engine.cpp:29
storm::utility::engineFromString
Engine engineFromString(std::string const &engineStr)
Parses the string representation of an engine and returns the corresponding engine.
Definition Engine.cpp:66
storm::utility::canHandle
bool canHandle(storm::utility::Engine const &engine, storm::storage::SymbolicModelDescription::ModelType const &modelType, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask)
Definition Engine.cpp:101