3#include <boost/algorithm/string/join.hpp>
29template<storm::dd::DdType Type,
typename ValueType>
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)
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);
52template<storm::dd::DdType Type,
typename ValueType>
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)
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);
76template<storm::dd::DdType Type,
typename ValueType>
78 return reachableStates.getNonZeroCount();
81template<storm::dd::DdType Type,
typename ValueType>
83 return transitionMatrix.getNonZeroCount();
86template<storm::dd::DdType Type,
typename ValueType>
88 return reachableStates.getNonZeroCount();
91template<storm::dd::DdType Type,
typename ValueType>
96template<storm::dd::DdType Type,
typename ValueType>
101template<storm::dd::DdType Type,
typename ValueType>
103 return reachableStates;
106template<storm::dd::DdType Type,
typename ValueType>
108 return labelToBddMap.at(
"init");
111template<storm::dd::DdType Type,
typename ValueType>
113 return labelToBddMap.at(
"deadlock");
116template<storm::dd::DdType Type,
typename ValueType>
119 auto bddIt = labelToBddMap.find(label);
120 if (bddIt != labelToBddMap.end()) {
121 return bddIt->second;
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);
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;
139template<storm::dd::DdType Type,
typename ValueType>
141 if (expression.
isTrue()) {
142 return this->getReachableStates();
143 }
else if (expression.
isFalse()) {
144 return manager->getBddZero();
148 std::stringstream stream;
149 stream << expression;
150 auto bddIt = labelToBddMap.find(stream.str());
151 if (bddIt != labelToBddMap.end()) {
152 return bddIt->second;
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;
161template<storm::dd::DdType Type,
typename ValueType>
163 auto bddIt = labelToBddMap.find(label);
164 if (bddIt != labelToBddMap.end()) {
168 auto expressionIt = labelToExpressionMap.find(label);
169 if (expressionIt != labelToExpressionMap.end()) {
176template<storm::dd::DdType Type,
typename ValueType>
178 return transitionMatrix;
181template<storm::dd::DdType Type,
typename ValueType>
183 return transitionMatrix;
186template<storm::dd::DdType Type,
typename ValueType>
188 return this->getTransitionMatrix().notZero();
191template<storm::dd::DdType Type,
typename ValueType>
196template<storm::dd::DdType Type,
typename ValueType>
198 return columnVariables;
201template<storm::dd::DdType Type,
typename ValueType>
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()));
209template<storm::dd::DdType Type,
typename ValueType>
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()));
217template<storm::dd::DdType Type,
typename ValueType>
219 return emptyVariableSet;
222template<storm::dd::DdType Type,
typename ValueType>
224 return rowColumnMetaVariablePairs;
227template<storm::dd::DdType Type,
typename ValueType>
229 this->transitionMatrix = transitionMatrix;
232template<storm::dd::DdType Type,
typename ValueType>
234 return labelToExpressionMap;
237template<storm::dd::DdType Type,
typename ValueType>
239 return labelToBddMap;
242template<storm::dd::DdType Type,
typename ValueType>
244 return (storm::utility::dd::getRowColumnDiagonal<Type>(this->getManager(), this->getRowColumnMetaVariablePairs()) && this->getReachableStates())
245 .template toAdd<ValueType>();
248template<storm::dd::DdType Type,
typename ValueType>
250 return this->rewardModels.find(rewardModelName) != this->rewardModels.end();
253template<storm::dd::DdType Type,
typename ValueType>
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();
262 "Unable to refer to default reward model, because there is no default model or it is not unique.");
265 STORM_LOG_THROW(
false, storm::exceptions::IllegalArgumentException,
"The requested reward model '" << rewardModelName <<
"' does not exist.");
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;
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;
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;
292template<storm::dd::DdType Type,
typename ValueType>
294 return this->rewardModels.size() == 1;
297template<storm::dd::DdType Type,
typename ValueType>
299 return !this->rewardModels.empty();
302template<storm::dd::DdType Type,
typename ValueType>
304 return this->rewardModels;
307template<storm::dd::DdType Type,
typename ValueType>
309 return this->rewardModels;
312template<storm::dd::DdType Type,
typename ValueType>
314 this->printModelInformationHeaderToStream(out);
315 this->printModelInformationFooterToStream(out);
318template<storm::dd::DdType Type,
typename ValueType>
320 std::vector<std::string> labels;
321 for (
auto const& entry : labelToExpressionMap) {
322 labels.push_back(entry.first);
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";
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";
343 for (
auto const& label : labelToExpressionMap) {
344 out <<
" * " << label.first <<
'\n';
346 out <<
"-------------------------------------------------------------- \n";
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)");
358 rewardModelNames.push_back(nameRewardModelPair.first);
361 out <<
"Reward Models: " << boost::join(rewardModelNames,
", ") <<
'\n';
363 out <<
"Reward Models: none\n";
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();
373 uint_fast64_t columnVariableCount = 0;
374 for (
auto const& metaVariable : this->columnVariables) {
375 columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
378 out <<
"Variables: \t" <<
"rows: " << this->rowVariables.size() <<
" meta variables (" << rowVariableCount <<
" DD variables)"
379 <<
", columns: " << this->columnVariables.size() <<
" meta variables (" << columnVariableCount <<
" DD variables)";
382template<storm::dd::DdType Type,
typename ValueType>
384 return this->rowExpressionAdapter;
387template<storm::dd::DdType Type,
typename ValueType>
392template<storm::dd::DdType Type,
typename ValueType>
397template<storm::dd::DdType Type,
typename ValueType>
402template<storm::dd::DdType Type,
typename ValueType>
404 return std::is_same<ValueType, storm::RationalFunction>::value;
407template<storm::dd::DdType Type,
typename ValueType>
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);
416template<storm::dd::DdType Type,
typename ValueType>
418 if (!this->supportsParameters()) {
422 for (
auto it = this->getTransitionMatrix().begin(
false); it != this->getTransitionMatrix().end(); ++it) {
431template<storm::dd::DdType Type,
typename ValueType>
433 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"This value type does not support parameters.");
436template<storm::dd::DdType Type,
typename ValueType>
438 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"This value type does not support parameters.");
443 this->parameters.insert(parameters.begin(), parameters.end());
451template<storm::dd::DdType Type,
typename ValueType>
452template<
typename NewValueType>
455 STORM_LOG_TRACE(
"Converting value type of symbolic model from " <<
typeid(
ValueType).name() <<
" to " <<
typeid(NewValueType).name() <<
".");
459 return this->
template as<storm::models::symbolic::Dtmc<Type, ValueType>>()->
template toValueType<NewValueType>();
461 return this->
template as<storm::models::symbolic::Ctmc<Type, ValueType>>()->
template toValueType<NewValueType>();
463 return this->
template as<storm::models::symbolic::Mdp<Type, ValueType>>()->
template toValueType<NewValueType>();
465 return this->
template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>()->
template toValueType<NewValueType>();
467 return this->
template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>()->
template toValueType<NewValueType>();
474template<storm::dd::DdType Type,
typename ValueType>
475template<
typename NewValueType>
480 return std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(*this->
template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
482 return std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(*this->
template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
484 return std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(*this->
template as<storm::models::symbolic::Mdp<Type, ValueType>>());
486 return std::make_shared<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>(
487 *this->
template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>());
489 return std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>(
490 *this->
template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>());
498template class Model<storm::dd::DdType::CUDD, double>;
499template class Model<storm::dd::DdType::Sylvan, double>;
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;
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>;
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.
virtual bool isSymbolicModel() const
Checks whether the model is a symbolic model.
virtual std::optional< storm::dd::DdType > getDdType() const
virtual bool hasParameters() const
Checks whether the model has parameters.
virtual bool supportsParameters() const
Checks whether the model supports parameters.
Base class for all symbolic models.
storm::dd::DdManager< Type > & getManager() const
Retrieves the manager responsible for the DDs that represent this model.
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
storm::dd::Add< Type, ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
storm::dd::Bdd< Type > const & getDeadlockStates() const
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
virtual storm::expressions::Expression getExpression(std::string const &label) const
Returns the expression for the given label.
RewardModelType const & getUniqueRewardModel() const
Retrieves the unique reward model, if there exists exactly one.
virtual std::string const & getUniqueRewardModelName() const override
Retrieves the name of the unique reward model, if there exists exactly one.
virtual storm::dd::Bdd< Type > getQualitativeTransitionMatrix(bool keepNondeterminism=true) const
Retrieves the matrix qualitatively (i.e.
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...
std::shared_ptr< storm::dd::DdManager< Type > > const & getManagerAsSharedPointer() const
Retrieves the manager responsible for the DDs that represent this model.
Model(Model< Type, ValueType > const &other)=default
std::vector< std::string > getLabels() const
storm::dd::Add< Type, ValueType > getRowColumnIdentity() const
Retrieves an ADD that represents the diagonal of the transition matrix.
void printRewardModelsInformationToStream(std::ostream &out) const
Prints information about the reward models to the specified stream.
std::map< std::string, storm::dd::Bdd< Type > > const & getLabelToBddMap() const
Retrieves the mapping of labels to their defining expressions.
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
virtual std::set< storm::expressions::Variable > const & getNondeterminismVariables() const
Retrieves all meta variables used to encode the nondeterminism.
void printModelInformationFooterToStream(std::ostream &out) const
Prints the information footer (reward models, labels) of the model to the specified stream.
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & getRowColumnMetaVariablePairs() const
Retrieves the pairs of row and column meta variables.
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.
virtual bool hasLabel(std::string const &label) const
Retrieves whether the given label is a valid label in this model.
std::map< std::string, storm::expressions::Expression > const & getLabelToExpressionMap() const
Retrieves the mapping of labels to their defining expressions.
void printModelInformationHeaderToStream(std::ostream &out) const
Prints the information header (number of states and transitions) of the model to the specified stream...
std::unordered_map< std::string, RewardModelType > & getRewardModels()
virtual uint_fast64_t getNumberOfChoices() const override
Returns the number of choices ine the model.
std::set< storm::expressions::Variable > getRowAndNondeterminismVariables() const
Retrieves all meta variables used to encode rows and nondetermism.
void setTransitionMatrix(storm::dd::Add< Type, ValueType > const &transitionMatrix)
Sets the transition matrix of the model.
std::set< storm::expressions::Variable > getColumnAndNondeterminismVariables() const
Retrieves all meta variables used to encode columns and nondetermism.
virtual storm::dd::Bdd< Type > getStates(std::string const &label) const
Returns the sets of states labeled with the given label.
virtual uint_fast64_t getNumberOfTransitions() const override
Returns the number of (non-zero) transitions of the model.
bool hasRewardModel() const
Retrieves whether the model has at least one reward model.
virtual bool hasUniqueRewardModel() const override
Retrieves whether the model has a unique reward model.
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
#define STORM_LOG_WARN(message)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_THROW(cond, exception, message)
bool isConstant(ValueType const &)