diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index f6a78b27e..430cf658b 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -15,6 +15,10 @@
#include "src/storage/dd/Bdd.h"
#include "src/adapters/AddExpressionAdapter.h"
+#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Ctmc.h"
+#include "src/models/symbolic/Mdp.h"
+
#include "src/utility/macros.h"
#include "src/utility/jani.h"
#include "src/exceptions/InvalidArgumentException.h"
@@ -412,8 +416,6 @@ namespace storm {
return result;
}
- static int c = 0;
-
// A class that is responsible for performing the actual composition.
template <storm::dd::DdType Type, typename ValueType>
class AutomatonComposer : public storm::jani::CompositionVisitor {
@@ -704,7 +706,18 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
- storm::dd::Add<Type, ValueType> createGlobalTransitionRelation(storm::jani::Model const& model, AutomatonDd<Type, ValueType> const& automatonDd, CompositionVariables<Type, ValueType> const& variables) {
+ struct SystemDd {
+ SystemDd(storm::dd::Add<Type, ValueType> const& transitionsDd, storm::dd::Add<Type, ValueType> const& stateActionDd, uint64_t numberOfNondeterminismVariables = 0) : transitionsDd(transitionsDd), stateActionDd(stateActionDd), numberOfNondeterminismVariables(numberOfNondeterminismVariables) {
+ // Intentionally left empty.
+ }
+
+ storm::dd::Add<Type, ValueType> transitionsDd;
+ storm::dd::Add<Type, ValueType> stateActionDd;
+ uint64_t numberOfNondeterminismVariables;
+ };
+
+ template <storm::dd::DdType Type, typename ValueType>
+ SystemDd<Type, ValueType> buildSystemDd(storm::jani::Model const& model, AutomatonDd<Type, ValueType> const& automatonDd, CompositionVariables<Type, ValueType> const& variables) {
// If the model is an MDP, we need to encode the nondeterminism using additional variables.
if (model.getModelType() == storm::jani::ModelType::MDP) {
// Determine how many nondeterminism variables we need.
@@ -735,6 +748,8 @@ namespace storm {
result += edgesForAction * encodeAction<Type, ValueType>(actionIndexToVariableIndex.at(action.first), actionVariables, variables);
}
+
+ return SystemDd<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables), numberOfNondeterminismVariables);
} else if (model.getModelType() == storm::jani::ModelType::DTMC || model.getModelType() == storm::jani::ModelType::CTMC) {
// Simply add all actions, but make sure to include the missing global variable identities.
storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
@@ -743,25 +758,95 @@ namespace storm {
result += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables);
}
}
- return result;
+
+ return SystemDd<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables));
+ }
+
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ struct ModelComponents {
+ storm::dd::Bdd<Type> reachableStates;
+ storm::dd::Bdd<Type> initialStates;
+ storm::dd::Add<Type, ValueType> transitionMatrix;
+ std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
+ };
+
+ template <storm::dd::DdType Type, typename ValueType>
+ std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
+ if (modelType == storm::jani::ModelType::DTMC) {
+ return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
+ } else if (modelType == storm::jani::ModelType::CTMC) {
+ return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
+ } else if (modelType == storm::jani::ModelType::MDP) {
+ return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
} else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}
- return storm::dd::Add<Type, ValueType>();
+
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ void postprocessSystemDd(storm::jani::Model const& model, SystemDd<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
+ // For DTMCs, we normalize each row to 1 (to account for non-determinism).
+ if (model.getModelType() == storm::jani::ModelType::DTMC) {
+ system.transitionsDd = system.transitionsDd / system.stateActionDd;
+ }
+
+
+ // If we were asked to treat some states as terminal states, we cut away their transitions now.
+ if (options.terminalStates || options.negatedTerminalStates) {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = model.getConstantsSubstitution();
+
+ storm::dd::Bdd<Type> terminalStatesBdd = variables.manager->getBddZero();
+ if (options.terminalStates) {
+ storm::expressions::Expression terminalExpression = options.terminalStates.get().substitute(constantsSubstitution);
+ STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
+ terminalStatesBdd = variables.rowExpressionAdapter->translateExpression(terminalExpression).toBdd();
+ }
+ if (options.negatedTerminalStates) {
+ storm::expressions::Expression negatedTerminalExpression = options.negatedTerminalStates.get().substitute(constantsSubstitution);
+ STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal.");
+ terminalStatesBdd |= !variables.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd();
+ }
+
+ system.transitionMatrix *= (!terminalStatesBdd).template toAdd<ValueType>();
+ }
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ storm::dd::Bdd<Type> computeInitial(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) {
+ storm::dd::Bdd<Type> initialStates = variables.rowExpressionAdapter->translateExpression( generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd();
+
+ for (auto const& metaVariable : generationInfo.rowMetaVariables) {
+ initialStates &= generationInfo.manager->getRange(metaVariable);
+ }
+
+ return initialStates;
}
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
+ // Create all necessary variables.
CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
CompositionVariables<Type, ValueType> variables = variableCreator.create();
+ // Compose the automata to a single automaton.
AutomatonComposer<Type, ValueType> composer(*this->model, variables);
- AutomatonDd<Type, ValueType> system = composer.compose();
+ AutomatonDd<Type, ValueType> globalAutomaton = composer.compose();
+
+ // Combine the edges of the single automaton to the full system DD.
+ SystemDd<Type, ValueType> system = buildSystemDd(*this->model, globalAutomaton, variables);
+
+ // Postprocess the system. This modifies the systemDd in place.
+ postprocessSystemDd(*this->model, system, variables, options);
+
- storm::dd::Add<Type, ValueType> transitions = createGlobalTransitionRelation(*this->model, system, variables);
+ ModelComponents<Type, ValueType> modelComponents;
+
- // FIXME
- return nullptr;
+ return createModel(this->model->getModelType(), variables, modelComponents);
}
template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index 7b336b1c5..4815262bc 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -180,5 +180,17 @@ namespace storm {
return edges.size();
}
+ bool Automaton::hasInitialStatesExpression() const {
+ return initialStatesExpression.isInitialized();
+ }
+
+ storm::expressions::Expression const& Automaton::getInitialStatesExpression() const {
+ return initialStatesExpression;
+ }
+
+ void Automaton::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
+ this->initialStatesExpression = initialStatesExpression;
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 09caef1b3..a63292290 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -210,6 +210,21 @@ namespace storm {
*/
uint64_t getNumberOfEdges() const;
+ /*!
+ * Retrieves whether there is an expression defining the legal initial values of the automaton's variables.
+ */
+ bool hasInitialStatesExpression() const;
+
+ /*!
+ * Retrieves the expression defining the legal initial values of the automaton's variables.
+ */
+ storm::expressions::Expression const& getInitialStatesExpression() const;
+
+ /*!
+ * Sets the expression defining the legal initial values of the automaton's variables.
+ */
+ void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
+
private:
/// The name of the automaton.
std::string name;
@@ -232,6 +247,9 @@ namespace storm {
/// The index of the initial location.
uint64_t initialLocationIndex;
+
+ // The expression characterizing the legal initial values of the variables of the automaton.
+ storm::expressions::Expression initialStatesExpression;
};
}
diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp
index cdc5ff062..8f4f6f106 100644
--- a/src/storage/jani/BooleanVariable.cpp
+++ b/src/storage/jani/BooleanVariable.cpp
@@ -3,7 +3,7 @@
namespace storm {
namespace jani {
- BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue) {
+ BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
// Intentionally left empty.
}
diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h
index fd94c447c..4e6f5d504 100644
--- a/src/storage/jani/BooleanVariable.h
+++ b/src/storage/jani/BooleanVariable.h
@@ -10,7 +10,7 @@ namespace storm {
/*!
* Creates a boolean variable.
*/
- BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+ BooleanVariable(std::string const& name, storm::expressions::Variable const& variable);
virtual bool isBooleanVariable() const;
};
diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp
index dbe3f3855..165e1d0e8 100644
--- a/src/storage/jani/BoundedIntegerVariable.cpp
+++ b/src/storage/jani/BoundedIntegerVariable.cpp
@@ -3,7 +3,7 @@
namespace storm {
namespace jani {
- BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
+ BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) {
// Intentionally left empty.
}
diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h
index b6e7ca6f4..16f7f6eb5 100644
--- a/src/storage/jani/BoundedIntegerVariable.h
+++ b/src/storage/jani/BoundedIntegerVariable.h
@@ -11,7 +11,7 @@ namespace storm {
/*!
* Creates a bounded integer variable.
*/
- BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound);
/*!
* Retrieves the expression defining the lower bound of the variable.
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 182355681..29b0d9dd6 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -281,24 +281,27 @@ namespace storm {
}
// Substitute constants in all global variables.
- for (auto& variable : result.getGlobalVariables()) {
- variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
- }
for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
}
+ // Substitute constants in initial states expression.
+ if (this->hasInitialStatesExpression()) {
+ result.setInitialStatesExpression(this->getInitialStatesExpression().substitute(constantSubstitution));
+ }
+
// Substitute constants in variables of automata and their edges.
for (auto& automaton : result.getAutomata()) {
- for (auto& variable : automaton.getVariables()) {
- variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
- }
for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
}
+ if (automaton.hasInitialStatesExpression()) {
+ automaton.setInitialStatesExpression(automaton.getInitialStatesExpression().substitute(constantSubstitution));
+ }
+
for (auto& edge : automaton.getEdges()) {
edge.setGuard(edge.getGuard().substitute(constantSubstitution));
if (edge.hasRate()) {
@@ -316,6 +319,40 @@ namespace storm {
return result;
}
+ std::map<storm::expressions::Variable, storm::expressions::Expression> Model::getConstantsSubstitution() const {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> result;
+
+ for (auto const& constant : constants) {
+ if (constant.isDefined()) {
+ result.emplace(constant.getExpressionVariable(), constant.getExpression());
+ }
+ }
+
+ return result;
+ }
+
+ bool Model::hasInitialStatesExpression() const {
+ return initialStatesExpression.isInitialized();
+ }
+
+ storm::expressions::Expression Model::getInitialStatesExpression(bool includeAutomataInitialStatesExpressions) const {
+ STORM_LOG_THROW(globalVariables.empty() || this->hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve global initial states expression, because there is none.");
+ storm::expressions::Expression result = this->hasInitialStatesExpression() ? initialStatesExpression : expressionManager->boolean(true);
+ if (includeAutomataInitialStatesExpressions) {
+ for (auto const& automaton : automata) {
+ STORM_LOG_THROW(automaton.getVariables().empty() || automaton.hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve initial states expression from automaton '" << automaton.getName() << "', because there is none.");
+ if (!automaton.getVariables().empty()) {
+ result = result && automaton.getInitialStatesExpression();
+ }
+ }
+ }
+ return result;
+ }
+
+ void Model::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
+ this->initialStatesExpression = initialStatesExpression;
+ }
+
bool Model::checkValidity(bool logdbg) const {
// TODO switch to exception based return value.
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index 258f9417d..460fb50c1 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -219,6 +219,30 @@ namespace storm {
*/
Model substituteConstants() const;
+ /*!
+ * Retrieves a mapping from expression variables associated with defined constants of the model to their
+ * (the constants') defining expression.
+ */
+ std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
+
+ /*!
+ * Retrieves whether there is an expression defining the legal initial values of the global variables.
+ */
+ bool hasInitialStatesExpression() const;
+
+ /*!
+ * Retrieves the expression defining the legal initial values of the variables.
+ *
+ * @param includeAutomataInitialStatesExpressions If set to true, the expression defines the legal initial
+ * states not only for the global variables but also for the variables of each automaton.
+ */
+ storm::expressions::Expression getInitialStatesExpression(bool includeAutomataInitialStatesExpressions = false) const;
+
+ /*!
+ * Sets the expression defining the legal initial values of the global variables.
+ */
+ void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
+
/*!
* Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
*/
@@ -263,6 +287,9 @@ namespace storm {
/// An expression describing how the system is composed of the automata.
std::shared_ptr<Composition> composition;
+
+ // The expression characterizing the legal initial values of the global variables.
+ storm::expressions::Expression initialStatesExpression;
};
}
}
diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp
index 2dd297d96..bf8f7615f 100644
--- a/src/storage/jani/UnboundedIntegerVariable.cpp
+++ b/src/storage/jani/UnboundedIntegerVariable.cpp
@@ -3,7 +3,7 @@
namespace storm {
namespace jani {
- UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue) {
+ UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
// Intentionally left empty.
}
diff --git a/src/storage/jani/UnboundedIntegerVariable.h b/src/storage/jani/UnboundedIntegerVariable.h
index bb6a79e4e..585b953d4 100644
--- a/src/storage/jani/UnboundedIntegerVariable.h
+++ b/src/storage/jani/UnboundedIntegerVariable.h
@@ -10,7 +10,7 @@ namespace storm {
/*!
* Creates an unbounded integer variable.
*/
- UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+ UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable);
virtual bool isUnboundedIntegerVariable() const override;
};
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
index 5988cf45b..3bcb8fcd0 100644
--- a/src/storage/jani/Variable.cpp
+++ b/src/storage/jani/Variable.cpp
@@ -7,7 +7,7 @@
namespace storm {
namespace jani {
- Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : name(name), variable(variable), initialValue(initialValue) {
+ Variable::Variable(std::string const& name, storm::expressions::Variable const& variable) : name(name), variable(variable) {
// Intentionally left empty.
}
@@ -15,22 +15,10 @@ namespace storm {
return variable;
}
- bool Variable::hasInitialValue() const {
- return initialValue.isInitialized();
- }
-
std::string const& Variable::getName() const {
return name;
}
- storm::expressions::Expression const& Variable::getInitialValue() const {
- return initialValue;
- }
-
- void Variable::setInitialValue(storm::expressions::Expression const& initialValue) {
- this->initialValue = initialValue;
- }
-
bool Variable::isBooleanVariable() const {
return false;
}
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index f113de4a6..2ef15321b 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -18,7 +18,7 @@ namespace storm {
/*!
* Creates a new variable.
*/
- Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue);
+ Variable(std::string const& name, storm::expressions::Variable const& variable);
/*!
* Retrieves the associated expression variable
@@ -29,22 +29,7 @@ namespace storm {
* Retrieves the name of the variable.
*/
std::string const& getName() const;
-
- /*!
- * Retrieves the initial value of the variable.
- */
- storm::expressions::Expression const& getInitialValue() const;
-
- /*!
- * Sets a new value as the initial value of the variable.
- */
- void setInitialValue(storm::expressions::Expression const& initialValue);
-
- /*!
- * Retrieves whether the variable has an initial value.
- */
- bool hasInitialValue() const;
-
+
// Methods to determine the type of the variable.
virtual bool isBooleanVariable() const;
virtual bool isBoundedIntegerVariable() const;
@@ -64,9 +49,6 @@ namespace storm {
// The expression variable associated with this variable.
storm::expressions::Variable variable;
-
- // The expression defining the initial value of the variable.
- storm::expressions::Expression initialValue;
};
}
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index e7f2b42b7..78cfab2cc 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -149,6 +149,10 @@ namespace storm {
return !unboundedIntegerVariables.empty();
}
+ bool VariableSet::empty() const {
+ return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables());
+ }
+
template class detail::Dereferencer<Variable>;
template class detail::Dereferencer<BooleanVariable>;
template class detail::Dereferencer<BoundedIntegerVariable>;
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index eeedcdc6f..2dc5105e3 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -167,6 +167,11 @@ namespace storm {
*/
bool containsUnboundedIntegerVariables() const;
+ /*!
+ * Retrieves whether this variable set is empty.
+ */
+ bool empty() const;
+
private:
/// The vector of all variables.
std::vector<std::shared_ptr<Variable>> variables;