Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Model.cpp
Go to the documentation of this file.
2
3#include <boost/algorithm/string/join.hpp>
4
10
13
16
18
20#include "storm/utility/dd.h"
22
25
26namespace storm {
27namespace models {
28namespace symbolic {
29template<storm::dd::DdType Type, typename ValueType>
31 storm::dd::Bdd<Type> reachableStates, storm::dd::Bdd<Type> initialStates, storm::dd::Bdd<Type> deadlockStates,
32 storm::dd::Add<Type, ValueType> transitionMatrix, std::set<storm::expressions::Variable> const& rowVariables,
33 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
34 std::set<storm::expressions::Variable> const& columnVariables,
35 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
36 std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
37 std::unordered_map<std::string, RewardModelType> const& rewardModels)
38 : storm::models::Model<ValueType>(modelType),
39 manager(manager),
40 reachableStates(reachableStates),
41 transitionMatrix(transitionMatrix),
42 rowVariables(rowVariables),
43 rowExpressionAdapter(rowExpressionAdapter),
44 columnVariables(columnVariables),
45 rowColumnMetaVariablePairs(rowColumnMetaVariablePairs),
46 labelToExpressionMap(labelToExpressionMap),
47 rewardModels(rewardModels) {
48 this->labelToBddMap.emplace("init", initialStates);
49 this->labelToBddMap.emplace("deadlock", deadlockStates);
50}
51
52template<storm::dd::DdType Type, typename ValueType>
54 storm::dd::Bdd<Type> reachableStates, storm::dd::Bdd<Type> initialStates, storm::dd::Bdd<Type> deadlockStates,
55 storm::dd::Add<Type, ValueType> transitionMatrix, std::set<storm::expressions::Variable> const& rowVariables,
56 std::set<storm::expressions::Variable> const& columnVariables,
57 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
58 std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap, std::unordered_map<std::string, RewardModelType> const& rewardModels)
59 : storm::models::Model<ValueType>(modelType),
60 manager(manager),
61 reachableStates(reachableStates),
62 transitionMatrix(transitionMatrix),
63 rowVariables(rowVariables),
64 rowExpressionAdapter(nullptr),
65 columnVariables(columnVariables),
66 rowColumnMetaVariablePairs(rowColumnMetaVariablePairs),
67 labelToBddMap(labelToBddMap),
68 rewardModels(rewardModels) {
69 STORM_LOG_THROW(this->labelToBddMap.find("init") == this->labelToBddMap.end(), storm::exceptions::WrongFormatException, "Illegal custom label 'init'.");
70 STORM_LOG_THROW(this->labelToBddMap.find("deadlock") == this->labelToBddMap.end(), storm::exceptions::WrongFormatException,
71 "Illegal custom label 'deadlock'.");
72 this->labelToBddMap.emplace("init", initialStates);
73 this->labelToBddMap.emplace("deadlock", deadlockStates);
74}
75
76template<storm::dd::DdType Type, typename ValueType>
78 return reachableStates.getNonZeroCount();
79}
80
81template<storm::dd::DdType Type, typename ValueType>
83 return transitionMatrix.getNonZeroCount();
84}
85
86template<storm::dd::DdType Type, typename ValueType>
88 return reachableStates.getNonZeroCount();
89}
90
91template<storm::dd::DdType Type, typename ValueType>
95
96template<storm::dd::DdType Type, typename ValueType>
97std::shared_ptr<storm::dd::DdManager<Type>> const& Model<Type, ValueType>::getManagerAsSharedPointer() const {
98 return manager;
99}
100
101template<storm::dd::DdType Type, typename ValueType>
103 return reachableStates;
104}
105
106template<storm::dd::DdType Type, typename ValueType>
108 return labelToBddMap.at("init");
109}
111template<storm::dd::DdType Type, typename ValueType>
113 return labelToBddMap.at("deadlock");
114}
115
116template<storm::dd::DdType Type, typename ValueType>
118 // First check whether we have a BDD for this label.
119 auto bddIt = labelToBddMap.find(label);
120 if (bddIt != labelToBddMap.end()) {
121 return bddIt->second;
122 } else {
123 // If not, check for an expression we can translate.
124 auto expressionIt = labelToExpressionMap.find(label);
125 STORM_LOG_THROW(expressionIt != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException,
126 "The label " << label << " is invalid for the labeling of the model.");
127 return this->getStates(expressionIt->second);
128 }
129}
130
131template<storm::dd::DdType Type, typename ValueType>
133 auto expressionIt = labelToExpressionMap.find(label);
134 STORM_LOG_THROW(expressionIt != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException,
135 "Cannot retrieve the expression for the label " << label << ".");
136 return expressionIt->second;
137}
138
139template<storm::dd::DdType Type, typename ValueType>
141 if (expression.isTrue()) {
142 return this->getReachableStates();
143 } else if (expression.isFalse()) {
144 return manager->getBddZero();
146
147 // Look up the string equivalent of the expression.
148 std::stringstream stream;
149 stream << expression;
150 auto bddIt = labelToBddMap.find(stream.str());
151 if (bddIt != labelToBddMap.end()) {
152 return bddIt->second;
154
155 // Finally try to translate the expression with an adapter.
156 STORM_LOG_THROW(rowExpressionAdapter != nullptr, storm::exceptions::InvalidOperationException,
157 "Cannot create BDD for expression without expression adapter.");
158 return rowExpressionAdapter->translateExpression(expression).toBdd() && this->reachableStates;
159}
160
161template<storm::dd::DdType Type, typename ValueType>
162bool Model<Type, ValueType>::hasLabel(std::string const& label) const {
163 auto bddIt = labelToBddMap.find(label);
164 if (bddIt != labelToBddMap.end()) {
165 return true;
166 }
167
168 auto expressionIt = labelToExpressionMap.find(label);
169 if (expressionIt != labelToExpressionMap.end()) {
170 return true;
171 } else {
172 return false;
173 }
174}
175
176template<storm::dd::DdType Type, typename ValueType>
178 return transitionMatrix;
179}
180
181template<storm::dd::DdType Type, typename ValueType>
185
186template<storm::dd::DdType Type, typename ValueType>
188 return this->getTransitionMatrix().notZero();
189}
190
191template<storm::dd::DdType Type, typename ValueType>
192std::set<storm::expressions::Variable> const& Model<Type, ValueType>::getRowVariables() const {
193 return rowVariables;
194}
195
196template<storm::dd::DdType Type, typename ValueType>
197std::set<storm::expressions::Variable> const& Model<Type, ValueType>::getColumnVariables() const {
198 return columnVariables;
199}
201template<storm::dd::DdType Type, typename ValueType>
202std::set<storm::expressions::Variable> Model<Type, ValueType>::getRowAndNondeterminismVariables() const {
203 std::set<storm::expressions::Variable> result;
204 std::set_union(this->getRowVariables().begin(), this->getRowVariables().end(), this->getNondeterminismVariables().begin(),
205 this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
206 return result;
208
209template<storm::dd::DdType Type, typename ValueType>
210std::set<storm::expressions::Variable> Model<Type, ValueType>::getColumnAndNondeterminismVariables() const {
211 std::set<storm::expressions::Variable> result;
212 std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(),
213 this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
214 return result;
215}
216
217template<storm::dd::DdType Type, typename ValueType>
218std::set<storm::expressions::Variable> const& Model<Type, ValueType>::getNondeterminismVariables() const {
219 return emptyVariableSet;
220}
222template<storm::dd::DdType Type, typename ValueType>
223std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& Model<Type, ValueType>::getRowColumnMetaVariablePairs() const {
224 return rowColumnMetaVariablePairs;
225}
226
227template<storm::dd::DdType Type, typename ValueType>
229 this->transitionMatrix = transitionMatrix;
230}
231
232template<storm::dd::DdType Type, typename ValueType>
233std::map<std::string, storm::expressions::Expression> const& Model<Type, ValueType>::getLabelToExpressionMap() const {
234 return labelToExpressionMap;
236
237template<storm::dd::DdType Type, typename ValueType>
238std::map<std::string, storm::dd::Bdd<Type>> const& Model<Type, ValueType>::getLabelToBddMap() const {
239 return labelToBddMap;
240}
241
242template<storm::dd::DdType Type, typename ValueType>
244 return (storm::utility::dd::getRowColumnDiagonal<Type>(this->getManager(), this->getRowColumnMetaVariablePairs()) && this->getReachableStates())
245 .template toAdd<ValueType>();
246}
247
248template<storm::dd::DdType Type, typename ValueType>
249bool Model<Type, ValueType>::hasRewardModel(std::string const& rewardModelName) const {
250 return this->rewardModels.find(rewardModelName) != this->rewardModels.end();
251}
252
253template<storm::dd::DdType Type, typename ValueType>
254typename Model<Type, ValueType>::RewardModelType const& Model<Type, ValueType>::getRewardModel(std::string const& rewardModelName) const {
255 auto it = this->rewardModels.find(rewardModelName);
256 if (it == this->rewardModels.end()) {
257 if (rewardModelName.empty()) {
258 if (this->hasUniqueRewardModel()) {
259 return this->getUniqueRewardModel();
260 } else {
261 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException,
262 "Unable to refer to default reward model, because there is no default model or it is not unique.");
264 } else {
265 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "The requested reward model '" << rewardModelName << "' does not exist.");
266 }
267 }
268 return it->second;
269}
271template<storm::dd::DdType Type, typename ValueType>
273 STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException,
274 "Cannot retrieve unique reward model, because there is no unique one.");
275 return this->rewardModels.cbegin()->second;
276}
278template<storm::dd::DdType Type, typename ValueType>
280 STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException,
281 "Cannot retrieve name of unique reward model, because there is no unique one.");
282 return this->rewardModels.cbegin()->first;
283}
285template<storm::dd::DdType Type, typename ValueType>
287 STORM_LOG_THROW(this->hasUniqueRewardModel(), storm::exceptions::InvalidOperationException,
288 "Cannot retrieve unique reward model, because there is no unique one.");
289 return this->rewardModels.begin()->second;
290}
292template<storm::dd::DdType Type, typename ValueType>
294 return this->rewardModels.size() == 1;
295}
296
297template<storm::dd::DdType Type, typename ValueType>
299 return !this->rewardModels.empty();
302template<storm::dd::DdType Type, typename ValueType>
303std::unordered_map<std::string, typename Model<Type, ValueType>::RewardModelType>& Model<Type, ValueType>::getRewardModels() {
304 return this->rewardModels;
305}
306
307template<storm::dd::DdType Type, typename ValueType>
308std::unordered_map<std::string, typename Model<Type, ValueType>::RewardModelType> const& Model<Type, ValueType>::getRewardModels() const {
309 return this->rewardModels;
311
312template<storm::dd::DdType Type, typename ValueType>
314 this->printModelInformationHeaderToStream(out);
315 this->printModelInformationFooterToStream(out);
317
318template<storm::dd::DdType Type, typename ValueType>
319std::vector<std::string> Model<Type, ValueType>::getLabels() const {
320 std::vector<std::string> labels;
321 for (auto const& entry : labelToExpressionMap) {
322 labels.push_back(entry.first);
323 }
324 return labels;
325}
327template<storm::dd::DdType Type, typename ValueType>
329 out << "-------------------------------------------------------------- \n";
330 out << "Model type: \t" << this->getType() << " (symbolic)\n";
331 out << "States: \t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)\n";
332 out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)\n";
333}
334
335template<storm::dd::DdType Type, typename ValueType>
337 this->printRewardModelsInformationToStream(out);
338 this->printDdVariableInformationToStream(out);
339 out << "\nLabels: \t" << (this->labelToExpressionMap.size() + this->labelToBddMap.size()) << '\n';
340 for (auto const& label : labelToBddMap) {
341 out << " * " << label.first << " -> " << label.second.getNonZeroCount() << " state(s) (" << label.second.getNodeCount() << " nodes)\n";
342 }
343 for (auto const& label : labelToExpressionMap) {
344 out << " * " << label.first << '\n';
345 }
346 out << "-------------------------------------------------------------- \n";
347}
349template<storm::dd::DdType Type, typename ValueType>
351 if (this->rewardModels.size()) {
352 std::vector<std::string> rewardModelNames;
353 std::for_each(this->rewardModels.cbegin(), this->rewardModels.cend(),
354 [&rewardModelNames](typename std::pair<std::string, RewardModelType> const& nameRewardModelPair) {
355 if (nameRewardModelPair.first.empty()) {
356 rewardModelNames.push_back("(default)");
357 } else {
358 rewardModelNames.push_back(nameRewardModelPair.first);
359 }
360 });
361 out << "Reward Models: " << boost::join(rewardModelNames, ", ") << '\n';
362 } else {
363 out << "Reward Models: none\n";
364 }
365}
366
367template<storm::dd::DdType Type, typename ValueType>
369 uint_fast64_t rowVariableCount = 0;
370 for (auto const& metaVariable : this->rowVariables) {
371 rowVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
372 }
373 uint_fast64_t columnVariableCount = 0;
374 for (auto const& metaVariable : this->columnVariables) {
375 columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
376 }
378 out << "Variables: \t" << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)"
379 << ", columns: " << this->columnVariables.size() << " meta variables (" << columnVariableCount << " DD variables)";
380}
381
382template<storm::dd::DdType Type, typename ValueType>
383std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> const& Model<Type, ValueType>::getRowExpressionAdapter() const {
384 return this->rowExpressionAdapter;
385}
386
387template<storm::dd::DdType Type, typename ValueType>
389 return true;
390}
392template<storm::dd::DdType Type, typename ValueType>
393std::optional<storm::dd::DdType> Model<Type, ValueType>::getDdType() const {
394 return Type;
395}
396
397template<storm::dd::DdType Type, typename ValueType>
400}
401
402template<storm::dd::DdType Type, typename ValueType>
404 return std::is_same<ValueType, storm::RationalFunction>::value;
405}
406
407template<storm::dd::DdType Type, typename ValueType>
408void Model<Type, ValueType>::writeDotToFile(std::string const& filename) const {
409 this->getTransitionMatrix().exportToDot(filename, true);
410 this->getInitialStates().exportToDot(filename, true);
411 for (auto const& lab : this->getLabels()) {
412 this->getStates(lab).exportToDot(filename, true);
413 }
414}
415
416template<storm::dd::DdType Type, typename ValueType>
418 if (!this->supportsParameters()) {
419 return false;
420 }
421 // Check for parameters
422 for (auto it = this->getTransitionMatrix().begin(false); it != this->getTransitionMatrix().end(); ++it) {
423 if (!storm::utility::isConstant((*it).second)) {
424 return true;
425 }
426 }
427 // Only constant values present
428 return false;
429}
430
431template<storm::dd::DdType Type, typename ValueType>
432void Model<Type, ValueType>::addParameters(std::set<storm::RationalFunctionVariable> const& parameters) {
433 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters.");
434}
435
436template<storm::dd::DdType Type, typename ValueType>
437std::set<storm::RationalFunctionVariable> const& Model<Type, ValueType>::getParameters() const {
438 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This value type does not support parameters.");
439}
440
441template<>
442void Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::addParameters(std::set<storm::RationalFunctionVariable> const& parameters) {
443 this->parameters.insert(parameters.begin(), parameters.end());
444}
445
446template<>
447std::set<storm::RationalFunctionVariable> const& Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::getParameters() const {
448 return parameters;
449}
450
451template<storm::dd::DdType Type, typename ValueType>
452template<typename NewValueType>
453typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type Model<Type, ValueType>::toValueType()
454 const {
455 STORM_LOG_TRACE("Converting value type of symbolic model from " << typeid(ValueType).name() << " to " << typeid(NewValueType).name() << ".");
456
457 // Make a huge branching here as we cannot make a templated function virtual.
458 if (this->getType() == storm::models::ModelType::Dtmc) {
459 return this->template as<storm::models::symbolic::Dtmc<Type, ValueType>>()->template toValueType<NewValueType>();
460 } else if (this->getType() == storm::models::ModelType::Ctmc) {
461 return this->template as<storm::models::symbolic::Ctmc<Type, ValueType>>()->template toValueType<NewValueType>();
462 } else if (this->getType() == storm::models::ModelType::Mdp) {
463 return this->template as<storm::models::symbolic::Mdp<Type, ValueType>>()->template toValueType<NewValueType>();
464 } else if (this->getType() == storm::models::ModelType::MarkovAutomaton) {
465 return this->template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>()->template toValueType<NewValueType>();
466 } else if (this->getType() == storm::models::ModelType::S2pg) {
467 return this->template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>()->template toValueType<NewValueType>();
468 }
469
470 STORM_LOG_WARN("Could not convert value type of model.");
471 return nullptr;
472}
473
474template<storm::dd::DdType Type, typename ValueType>
475template<typename NewValueType>
476typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type Model<Type, ValueType>::toValueType()
477 const {
478 // Make a huge branching here as we cannot make a templated function virtual.
479 if (this->getType() == storm::models::ModelType::Dtmc) {
480 return std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(*this->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
481 } else if (this->getType() == storm::models::ModelType::Ctmc) {
482 return std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(*this->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
483 } else if (this->getType() == storm::models::ModelType::Mdp) {
484 return std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(*this->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
485 } else if (this->getType() == storm::models::ModelType::MarkovAutomaton) {
486 return std::make_shared<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>(
487 *this->template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>());
488 } else if (this->getType() == storm::models::ModelType::S2pg) {
489 return std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>(
490 *this->template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>());
491 }
492
493 STORM_LOG_WARN("Could not convert value type of model.");
494 return nullptr;
495}
496
497// Explicitly instantiate the template class.
498template class Model<storm::dd::DdType::CUDD, double>;
499template class Model<storm::dd::DdType::Sylvan, double>;
500
501template typename std::enable_if<std::is_same<double, double>::value, std::shared_ptr<Model<storm::dd::DdType::CUDD, double>>>::type
502Model<storm::dd::DdType::CUDD, double>::toValueType<double>() const;
503
504template class Model<storm::dd::DdType::Sylvan, storm::RationalNumber>;
505template typename std::enable_if<std::is_same<double, double>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>>>::type
506Model<storm::dd::DdType::Sylvan, double>::toValueType<double>() const;
507template typename std::enable_if<std::is_same<storm::RationalNumber, storm::RationalNumber>::value,
508 std::shared_ptr<Model<storm::dd::DdType::Sylvan, storm::RationalNumber>>>::type
509Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<storm::RationalNumber>() const;
510template typename std::enable_if<std::is_same<storm::RationalFunction, storm::RationalFunction>::value,
511 std::shared_ptr<Model<storm::dd::DdType::Sylvan, storm::RationalFunction>>>::type
512Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::toValueType<storm::RationalFunction>() const;
513template typename std::enable_if<!std::is_same<storm::RationalNumber, double>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>>>::type
514Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<double>() const;
515template class Model<storm::dd::DdType::Sylvan, storm::RationalFunction>;
516} // namespace symbolic
517} // namespace models
518} // namespace storm
bool isFalse() const
Checks if the expression is equal to the boolean literal false.
bool isTrue() const
Checks if the expression is equal to the boolean literal true.
virtual bool isExact() const
Checks whether the model is exact.
Definition ModelBase.cpp:62
virtual bool isSymbolicModel() const
Checks whether the model is a symbolic model.
Definition ModelBase.cpp:15
virtual std::optional< storm::dd::DdType > getDdType() const
Definition ModelBase.cpp:19
virtual bool hasParameters() const
Checks whether the model has parameters.
Definition ModelBase.cpp:58
virtual bool supportsParameters() const
Checks whether the model supports parameters.
Definition ModelBase.cpp:54
Base class for all symbolic models.
Definition Model.h:45
storm::dd::DdManager< Type > & getManager() const
Retrieves the manager responsible for the DDs that represent this model.
Definition Model.cpp:92
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
Definition Model.cpp:254
storm::dd::Add< Type, ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:177
storm::dd::Bdd< Type > const & getDeadlockStates() const
Definition Model.cpp:112
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
Definition Model.cpp:313
virtual storm::expressions::Expression getExpression(std::string const &label) const
Returns the expression for the given label.
Definition Model.cpp:132
RewardModelType const & getUniqueRewardModel() const
Retrieves the unique reward model, if there exists exactly one.
Definition Model.cpp:272
virtual std::string const & getUniqueRewardModelName() const override
Retrieves the name of the unique reward model, if there exists exactly one.
Definition Model.cpp:279
virtual storm::dd::Bdd< Type > getQualitativeTransitionMatrix(bool keepNondeterminism=true) const
Retrieves the matrix qualitatively (i.e.
Definition Model.cpp:187
std::set< storm::expressions::Variable > const & getColumnVariables() const
Retrieves the meta variables used to encode the columns of the transition matrix and the vector indic...
Definition Model.cpp:197
std::shared_ptr< storm::dd::DdManager< Type > > const & getManagerAsSharedPointer() const
Retrieves the manager responsible for the DDs that represent this model.
Definition Model.cpp:97
Model(Model< Type, ValueType > const &other)=default
std::vector< std::string > getLabels() const
Definition Model.cpp:319
storm::dd::Add< Type, ValueType > getRowColumnIdentity() const
Retrieves an ADD that represents the diagonal of the transition matrix.
Definition Model.cpp:243
void printRewardModelsInformationToStream(std::ostream &out) const
Prints information about the reward models to the specified stream.
Definition Model.cpp:350
std::map< std::string, storm::dd::Bdd< Type > > const & getLabelToBddMap() const
Retrieves the mapping of labels to their defining expressions.
Definition Model.cpp:238
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:107
virtual std::set< storm::expressions::Variable > const & getNondeterminismVariables() const
Retrieves all meta variables used to encode the nondeterminism.
Definition Model.cpp:218
void printModelInformationFooterToStream(std::ostream &out) const
Prints the information footer (reward models, labels) of the model to the specified stream.
Definition Model.cpp:336
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & getRowColumnMetaVariablePairs() const
Retrieves the pairs of row and column meta variables.
Definition Model.cpp:223
std::set< storm::expressions::Variable > const & getRowVariables() const
Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices.
Definition Model.cpp:192
virtual bool hasLabel(std::string const &label) const
Retrieves whether the given label is a valid label in this model.
Definition Model.cpp:162
std::map< std::string, storm::expressions::Expression > const & getLabelToExpressionMap() const
Retrieves the mapping of labels to their defining expressions.
Definition Model.cpp:233
void printModelInformationHeaderToStream(std::ostream &out) const
Prints the information header (number of states and transitions) of the model to the specified stream...
Definition Model.cpp:328
std::unordered_map< std::string, RewardModelType > & getRewardModels()
Definition Model.cpp:303
virtual uint_fast64_t getNumberOfChoices() const override
Returns the number of choices ine the model.
Definition Model.cpp:87
std::set< storm::expressions::Variable > getRowAndNondeterminismVariables() const
Retrieves all meta variables used to encode rows and nondetermism.
Definition Model.cpp:202
void setTransitionMatrix(storm::dd::Add< Type, ValueType > const &transitionMatrix)
Sets the transition matrix of the model.
Definition Model.cpp:228
std::set< storm::expressions::Variable > getColumnAndNondeterminismVariables() const
Retrieves all meta variables used to encode columns and nondetermism.
Definition Model.cpp:210
virtual storm::dd::Bdd< Type > getStates(std::string const &label) const
Returns the sets of states labeled with the given label.
Definition Model.cpp:117
virtual uint_fast64_t getNumberOfTransitions() const override
Returns the number of (non-zero) transitions of the model.
Definition Model.cpp:82
bool hasRewardModel() const
Retrieves whether the model has at least one reward model.
Definition Model.cpp:298
virtual bool hasUniqueRewardModel() const override
Retrieves whether the model has a unique reward model.
Definition Model.cpp:293
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:102
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
Definition Model.cpp:77
#define STORM_LOG_WARN(message)
Definition logging.h:25
#define STORM_LOG_TRACE(message)
Definition logging.h:12
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
bool isConstant(ValueType const &)
Definition constants.cpp:66
LabParser.cpp.