diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 623ad0187..3a46a36c5 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -6,6 +6,15 @@
#include "src/logic/Formulas.h"
+#include "src/storage/jani/Model.h"
+#include "src/storage/jani/RenameComposition.h"
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
+
+#include "src/storage/dd/Add.h"
+#include "src/storage/dd/Bdd.h"
+#include "src/adapters/AddExpressionAdapter.h"
+
#include "src/utility/macros.h"
#include "src/utility/jani.h"
#include "src/exceptions/InvalidArgumentException.h"
@@ -119,34 +128,521 @@ namespace storm {
this->model = this->model->substituteConstants();
}
- /*!
- * This structure represents a subcomponent of a composition.
- */
+ template <storm::dd::DdType Type, typename ValueType>
+ struct CompositionVariables {
+ CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()) {
+ // Intentionally left empty.
+ }
+
+ std::shared_ptr<storm::dd::DdManager<Type>> manager;
+
+ // The meta variables for the row encoding.
+ std::set<storm::expressions::Variable> rowMetaVariables;
+ std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
+ std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
+
+ // The meta variables for the column encoding.
+ std::set<storm::expressions::Variable> columnMetaVariables;
+ std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
+ std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
+
+ // All pairs of row/column meta variables.
+ std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
+
+ // A mapping from automata to the meta variable encoding their location.
+ std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
+
+ // The meta variables used to encode the actions.
+ std::vector<storm::expressions::Variable> actionVariables;
+
+ // The meta variables used to encode the remaining nondeterminism.
+ std::vector<storm::expressions::Variable> nondeterminismVariables;
+
+ // DDs representing the identity for each variable.
+ std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> variableToIdentityMap;
+
+ // A set of all meta variables that correspond to global variables.
+ std::set<storm::expressions::Variable> allGlobalVariables;
+
+ // DDs representing the identity for each automaton.
+ std::map<std::string, storm::dd::Add<Type, ValueType>> automatonToIdentityMap;
+
+ // DDs representing the valid ranges of the variables of each automaton.
+ std::map<std::string, storm::dd::Add<Type, ValueType>> automatonToRangeMap;
+ };
+
+ // A class responsible for creating the necessary variables for a subsequent composition of automata.
+ template <storm::dd::DdType Type, typename ValueType>
+ class CompositionVariableCreator : public storm::jani::CompositionVisitor {
+ public:
+ CompositionVariableCreator(storm::jani::Model const& model) : model(model) {
+ // Intentionally left empty.
+ }
+
+ CompositionVariables<Type, ValueType> create() {
+ // First, check whether every automaton appears exactly once in the system composition.
+ automata.clear();
+ this->model.getSystemComposition().accept(*this, boost::none);
+ STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata.");
+
+ // Then, check that the model does not contain unbounded integer variables.
+ STORM_LOG_THROW(!this->model.getGlobalVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global unbounded integer variables.");
+ for (auto const& automaton : this->model.getAutomata()) {
+ STORM_LOG_THROW(!automaton.getVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains unbounded integer variables in automaton '" << automaton.getName() << "'.");
+ }
+
+ // Based on this assumption, we create the variables.
+ return createVariables();
+ }
+
+ boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
+ auto it = automata.find(composition.getAutomatonName());
+ STORM_LOG_THROW(it != automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the same automaton multiple times.");
+ automata.insert(it, composition.getAutomatonName());
+ return boost::none;
+ }
+
+ boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
+ composition.getSubcomposition().accept(*this, boost::none);
+ return boost::none;
+ }
+
+ boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
+ composition.getLeftSubcomposition().accept(*this, boost::none);
+ composition.getRightSubcomposition().accept(*this, boost::none);
+ return boost::none;
+ }
+
+ private:
+ CompositionVariables<Type, ValueType> createVariables() {
+ CompositionVariables<Type, ValueType> result;
+
+ for (auto const& action : this->model.getActions()) {
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName());
+ result.actionVariables.push_back(variablePair.first);
+ }
+
+ // FIXME: check how many nondeterminism variables we should actually allocate.
+ uint64_t numberOfNondeterminismVariables = this->model.getNumberOfAutomata();
+ for (auto const& automaton : this->model.getAutomata()) {
+ numberOfNondeterminismVariables *= automaton.getNumberOfEdges();
+ }
+ for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) {
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i));
+ result.nondeterminismVariables.push_back(variablePair.first);
+ }
+
+ // Create global variables.
+ for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) {
+ createVariable(variable, result);
+ }
+ for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) {
+ createVariable(variable, result);
+ }
+
+ // Create the variables for the individual automata.
+ for (auto const& automaton : this->model.getAutomata()) {
+ storm::dd::Bdd<Type> identity = result.manager->getBddOne();
+ storm::dd::Bdd<Type> range = result.manager->getBddOne();
+
+ // Start by creating a meta variable for the location of the automaton.
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations());
+ result.automatonToLocationVariableMap[automaton.getName()] = variablePair.first;
+ storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
+ identity &= variableIdentity.toBdd();
+ range &= result.manager->getRange(variablePair.first);
+
+ // Then create variables for the variables of the automaton.
+ for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+ createVariable(variable, result);
+ identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
+ range &= result.manager->getRange(result.variableToRowMetaVariableMap.at(variable.getExpressionVariable()));
+ }
+ for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
+ createVariable(variable, result);
+ identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
+ range &= result.manager->getRange(result.variableToRowMetaVariableMap.at(variable.getExpressionVariable()));
+ }
+
+ result.automatonToIdentityMap[automaton.getName()] = identity.template toAdd<ValueType>();
+ result.automatonToRangeMap[automaton.getName()] = range.template toAdd<ValueType>();
+ }
+
+ return result;
+ }
+
+ void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+ int_fast64_t low = variable.getLowerBound().evaluateAsInt();
+ int_fast64_t high = variable.getUpperBound().evaluateAsInt();
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName(), low, high);
+
+ STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "] and " << variablePair.second.getName() << ".");
+
+ result.rowMetaVariables.insert(variablePair.first);
+ result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first);
+
+ result.columnMetaVariables.insert(variablePair.second);
+ result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second);
+
+ storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
+ result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+ result.rowColumnMetaVariablePairs.push_back(variablePair);
+
+ result.allGlobalVariables.insert(variable.getExpressionVariable());
+ }
+
+ void createVariable(storm::jani::BooleanVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName());
+
+ STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
+
+ result.rowMetaVariables.insert(variablePair.first);
+ result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first);
+
+ result.columnMetaVariables.insert(variablePair.second);
+ result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second);
+
+ storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
+ result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+
+ result.rowColumnMetaVariablePairs.push_back(variablePair);
+ result.allGlobalVariables.insert(variable.getExpressionVariable());
+ }
+
+ storm::jani::Model const& model;
+ std::set<std::string> automata;
+ };
+
+ template<storm::dd::DdType Type, typename ValueType>
+ struct EdgeDestinationDd {
+ EdgeDestinationDd(storm::dd::Add<Type, ValueType> const& transitionsDd, std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}) : transitionsDd(transitionsDd), writtenGlobalVariables(writtenGlobalVariables) {
+ // Intentionally left empty.
+ }
+
+ storm::dd::Add<Type, ValueType> transitionsDd;
+ std::set<storm::expressions::Variable> writtenGlobalVariables;
+ };
+
+ // This structure represents an edge.
+ template<storm::dd::DdType Type, typename ValueType>
+ struct EdgeDd {
+ EdgeDd(storm::dd::Add<Type> const& guardDd = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitionsDd = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> const& globalVariablesWrittenMultipleTimes = {}) {
+ // Intentionally left empty.
+ }
+
+ EdgeDd(EdgeDd const& other) : globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes), writtenGlobalVariables(other.writtenGlobalVariables), guardDd(other.guardDd), transitionsDd(other.transitionsDd) {
+ // Intentionally left empty.
+ }
+
+ EdgeDd& operator=(EdgeDd const& other) {
+ if (this != &other) {
+ globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes;
+ writtenGlobalVariables = other.writtenGlobalVariables;
+ guardDd = other.guardDd;
+ transitionsDd = other.transitionsDd;
+ }
+ return *this;
+ }
+
+ std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
+ std::set<storm::expressions::Variable> writtenGlobalVariables;
+ storm::dd::Add<Type, ValueType> guardDd;
+ storm::dd::Add<Type, ValueType> transitionsDd;
+ };
+
+ // This structure represents a subcomponent of a composition.
template<storm::dd::DdType Type, typename ValueType>
struct AutomatonDd {
-
+ AutomatonDd(storm::dd::Add<Type, ValueType> const& identity) : identity(identity) {
+ // Intentionally left empty.
+ }
+
+ std::map<uint64_t, std::vector<EdgeDd<Type, ValueType>>> actionIndexToEdges;
+ storm::dd::Add<Type, ValueType> identity;
};
template <storm::dd::DdType Type, typename ValueType>
- std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
- auto system = this->model->getSystemComposition().accept(*this, boost::any());
+ EdgeDd<Type, ValueType> extendEdgeWithIdentity(EdgeDd<Type, ValueType> const& edge, storm::dd::Add<Type, ValueType> const& identity) {
+ EdgeDd<Type, ValueType> result(edge);
+ result.transitionsDd *= identity;
+ return result;
}
template <storm::dd::DdType Type, typename ValueType>
- boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) {
+ EdgeDd<Type, ValueType> composeEdgesInParallel(EdgeDd<Type, ValueType> const& edge1, EdgeDd<Type, ValueType> const& edge2) {
+ EdgeDd<Type, ValueType> result;
+
+ // Compute the set of variables written multiple times by the composition.
+ std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
+ std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
+ std::set<storm::expressions::Variable> newVariablesWrittenMultipleTimes;
+ std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin()));
+
+ std::set<storm::expressions::Variable> variablesWrittenMultipleTimes;
+ std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin()));
+
+ result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes);
+
+ // Compute the set of variables written by the composition.
+ std::set<storm::expressions::Variable> variablesWritten;
+ std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin()));
+
+ result.writtenGlobalVariables = variablesWritten;
+
+ // Compose the guards.
+ result.guardDd = edge1.guardDd * edge2.guardDd;
+
+ // Compose the transitions.
+ result.transitionsDd = edge1.transitionsDd * edge2.transitionsDd;
+
+ return result;
}
+ // A class that is responsible for performing the actual composition.
template <storm::dd::DdType Type, typename ValueType>
- boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::RenameComposition const& composition, boost::any const& data) {
+ class AutomatonComposer : public storm::jani::CompositionVisitor {
+ public:
+ AutomatonComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : model(model), variables(variables) {
+ // Intentionally left empty.
+ }
- }
+ AutomatonDd<Type, ValueType> compose() {
+ return boost::any_cast<AutomatonDd<Type, ValueType>>(this->model.getSystemComposition().accept(*this, boost::none));
+ }
+
+ boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
+ return buildAutomatonDd(composition.getAutomatonName());
+ }
+
+ boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
+ AutomatonDd<Type, ValueType> subautomaton = boost::any_cast<AutomatonDd<Type, ValueType>>(composition.getSubcomposition().accept(*this, boost::none));
+
+ // Build a mapping from indices to indices for the renaming.
+ std::map<uint64_t, uint64_t> renamingIndexToIndex;
+ for (auto const& entry : composition.getRenaming()) {
+ if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) {
+ // Distinguish the cases where we hide the action or properly rename it.
+ if (entry.second) {
+ renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get()));
+ } else {
+ renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex());
+ }
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action.");
+ }
+ }
+
+ // Finally, apply the renaming.
+ AutomatonDd<Type, ValueType> result(subautomaton.identity);
+ for (auto const& actionEdges : subautomaton.actionIndexToEdges) {
+ auto it = renamingIndexToIndex.find(actionEdges.first);
+ if (it != renamingIndexToIndex.end()) {
+ // If we are to rename the action, do so.
+ result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end());
+ } else {
+ // Otherwise copy over the edges.
+ result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end());
+ }
+ }
+ return result;
+ }
+
+ boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
+ AutomatonDd<Type, ValueType> leftSubautomaton = boost::any_cast<AutomatonDd<Type, ValueType>>(composition.getLeftSubcomposition().accept(*this, boost::none));
+ AutomatonDd<Type, ValueType> rightSubautomaton = boost::any_cast<AutomatonDd<Type, ValueType>>(composition.getRightSubcomposition().accept(*this, boost::none));
+
+ // Build the set of synchronizing action indices.
+ std::set<uint64_t> synchronizingActionIndices;
+ for (auto const& entry : composition.getSynchronizationAlphabet()) {
+ if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) {
+ synchronizingActionIndices.insert(this->model.getActionIndex(entry));
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action.");
+ }
+ }
+
+ // Perform the composition.
+
+ // First, consider all actions in the left subcomposition.
+ AutomatonDd<Type, ValueType> result(leftSubautomaton.identity * rightSubautomaton.identity);
+ for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) {
+ // If we need to synchronize over this action, do so now.
+ if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) {
+ auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first);
+ if (rightIt != rightSubautomaton.actionIndexToEdges.end()) {
+ for (auto const& edge1 : actionEdges.second) {
+ for (auto const& edge2 : rightIt->second) {
+ result.actionIndexToEdges[actionEdges.first].push_back(composeEdgesInParallel(edge1, edge2));
+ }
+ }
+ }
+ } else {
+ // Extend all edges by the missing identity (unsynchronizing) and copy them over.
+ for (auto const& edge : actionEdges.second) {
+ result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity));
+ }
+ }
+ }
+
+ // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because
+ // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none,
+ // such transitions can not be taken and we can drop them.
+ for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) {
+ if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) {
+ for (auto const& edge : actionEdges.second) {
+ result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity));
+ }
+ }
+ }
+
+ return result;
+ }
+
+ private:
+ EdgeDestinationDd<Type, ValueType> buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add<Type, ValueType> const& guard) {
+ storm::dd::Add<Type, ValueType> transitionsDd = variables.manager->template getAddOne<ValueType>();
+
+ STORM_LOG_TRACE("Translating edge destination.");
+
+ // Iterate over all assignments (boolean and integer) and build the DD for it.
+ std::set<storm::expressions::Variable> assignedVariables;
+ for (auto const& assignment : destination.getAssignments()) {
+ // Record the variable as being written.
+ STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap.at(assignment.getExpressionVariable()).getName());
+ assignedVariables.insert(assignment.getExpressionVariable());
+
+ // Translate the written variable.
+ auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap.at(assignment.getExpressionVariable());
+ storm::dd::Add<Type, ValueType> writtenVariable = variables.manager->template getIdentity<ValueType>(primedMetaVariable);
+
+ // Translate the expression that is being assigned.
+ storm::dd::Add<Type, ValueType> updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getExpressionVariable());
+
+ // Combine the update expression with the guard.
+ storm::dd::Add<Type, ValueType> result = updateExpression * guard;
+
+ // Combine the variable and the assigned expression.
+ result = result.equals(writtenVariable).template toAdd<ValueType>();
+ result *= guard;
+
+ // Restrict the transitions to the range of the written variable.
+ result = result * variables.manager->getRange(primedMetaVariable).template toAdd<ValueType>();
+
+ transitionsDd *= result;
+ }
+
+ // Compute the set of assigned global variables.
+ std::set<storm::expressions::Variable> assignedGlobalVariables;
+ std::set_intersection(assignedVariables.begin(), assignedVariables.end(), variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin()));
+
+ // All unassigned boolean variables need to keep their value.
+ for (storm::jani::BooleanVariable const& variable : automaton.getVariables().getBooleanVariables()) {
+ if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) {
+ STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName());
+ transitionsDd *= variables.variableToIdentityMap.at(variable.getExpressionVariable());
+ }
+ }
+
+ // All unassigned integer variables need to keep their value.
+ for (storm::jani::BoundedIntegerVariable const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+ if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) {
+ STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName());
+ transitionsDd *= variables.variableToIdentityMap.at(variable.getExpressionVariable());
+ }
+ }
+
+ return EdgeDestinationDd<Type, ValueType>(transitionsDd * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables);
+ }
+
+ /*!
+ * Builds the DD for the given edge.
+ */
+ EdgeDd<Type, ValueType> buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) {
+ STORM_LOG_TRACE("Translating guard " << edge.getGuard());
+ storm::dd::Add<Type, ValueType> guard = variables.rowExpressionAdapter->translateExpression(edge.getGuard()) * variables.automatonToRangeMap.at(automaton.getName());
+ STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable.");
+
+ if (!guard.isZero()) {
+ // Create the DDs representing the individual updates.
+ std::vector<EdgeDestinationDd<Type, ValueType>> destinationDds;
+ for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) {
+ destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard));
+
+ STORM_LOG_WARN_COND(!destinationDds.back().transitionsDd.isZero(), "Destination does not have any effect.");
+ }
+
+ // Start by gathering all variables that were written in at least one update.
+ std::set<storm::expressions::Variable> globalVariablesInSomeUpdate;
+
+ // If the edge is not labeled with the silent action, we have to analyze which portion of the global
+ // variables was written by any of the updates and make all update results equal w.r.t. this set. If
+ // the edge is labeled with the silent action, we can already multiply the identities of all global variables.
+ if (edge.getActionId() != this->model.getSilentActionIndex()) {
+ std::for_each(destinationDds.begin(), destinationDds.end(), [&globalVariablesInSomeUpdate] (EdgeDestinationDd<Type, ValueType> const& edgeDestinationDd) { globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); } );
+ } else {
+ globalVariablesInSomeUpdate = variables.allGlobalVariables;
+ }
+
+ // Then, multiply the missing identities.
+ for (auto& destinationDd : destinationDds) {
+ std::set<storm::expressions::Variable> missingIdentities;
+ std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+
+ for (auto const& variable : missingIdentities) {
+ STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD.");
+ destinationDd.transitionsDd *= variables.variableToIdentityMap.at(variable);
+ }
+ }
+
+ // Now combine the destination DDs to the edge DD.
+ storm::dd::Add<Type, ValueType> transitionsDd = variables.manager->template getAddZero<ValueType>();
+ for (auto const& destinationDd : destinationDds) {
+ transitionsDd += destinationDd.transitionsDd;
+ }
+
+ return EdgeDd<Type, ValueType>(guard, guard * transitionsDd, globalVariablesInSomeUpdate);
+ } else {
+ return EdgeDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>());
+ }
+ }
+
+ /*!
+ * Builds the DD for the automaton with the given name.
+ */
+ AutomatonDd<Type, ValueType> buildAutomatonDd(std::string const& automatonName) {
+ AutomatonDd<Type, ValueType> result(variables.automatonToIdentityMap.at(automatonName));
+
+ storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
+ for (auto const& edge : automaton.getEdges()) {
+ // Build the edge and add it if it adds transitions.
+ EdgeDd<Type, ValueType> edgeDd = buildEdgeDd(automaton, edge);
+ if (!edgeDd.guardDd.isZero()) {
+ result.actionIndexToEdges[edge.getActionId()].push_back(edgeDd);
+ }
+ }
+
+ return result;
+ }
+
+ // The model that is referred to by the composition.
+ storm::jani::Model const& model;
+
+ // The variable to use when building an automaton.
+ CompositionVariables<Type, ValueType> const& variables;
+ };
template <storm::dd::DdType Type, typename ValueType>
- boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::ParallelComposition const& composition, boost::any const& data) {
+ std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
+ CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
+ CompositionVariables<Type, ValueType> variables = variableCreator.create();
+
+ AutomatonComposer<Type, ValueType> composer(*this->model, variables);
+ AutomatonDd<Type, ValueType> system = composer.compose();
+ // FIXME
+ return nullptr;
}
-
template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h
index a3f07a21c..a90f911b5 100644
--- a/src/builder/DdJaniModelBuilder.h
+++ b/src/builder/DdJaniModelBuilder.h
@@ -19,7 +19,7 @@ namespace storm {
namespace builder {
template <storm::dd::DdType Type, typename ValueType = double>
- class DdJaniModelBuilder : public storm::jani::CompositionVisitor {
+ class DdJaniModelBuilder {
public:
struct Options {
/*!
@@ -108,11 +108,7 @@ namespace storm {
* @return The translated model.
*/
storm::jani::Model const& getTranslatedModel() const;
-
- virtual boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override;
- virtual boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override;
- virtual boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override;
-
+
private:
/// The model to translate.
boost::optional<storm::jani::Model> model;
diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp
index 79f658356..ccdec51aa 100644
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@@ -8,133 +8,42 @@ namespace storm {
namespace jani {
namespace detail {
- EdgeIterator::EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
+ Edges::Edges(iterator it, iterator ite) : it(it), ite(ite) {
// Intentionally left empty.
}
- EdgeIterator& EdgeIterator::operator++() {
- incrementIterator();
- return *this;
+ Edges::iterator Edges::begin() const {
+ return it;
}
- EdgeIterator& EdgeIterator::operator++(int) {
- incrementIterator();
- return *this;
+ Edges::iterator Edges::end() const {
+ return ite;
}
- Edge& EdgeIterator::operator*() {
- return *in_it;
+ bool Edges::empty() const {
+ return it == ite;
}
- bool EdgeIterator::operator==(EdgeIterator const& other) const {
- return this->out_it == other.out_it && this->in_it == other.in_it;
- }
-
- bool EdgeIterator::operator!=(EdgeIterator const& other) const {
- return !(*this == other);
- }
-
- void EdgeIterator::incrementIterator() {
- ++in_it;
-
- // If the inner iterator has reached its end move it to the beginning of the next outer element.
- if (in_it == out_it->end()) {
- ++out_it;
- while (out_it != out_ite && out_it->empty()) {
- ++out_it;
- in_it = out_it->end();
- }
- if (out_it != out_ite) {
- in_it = out_it->begin();
- }
- }
- }
-
- ConstEdgeIterator::ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
- // Intentionally left empty.
- }
-
- ConstEdgeIterator& ConstEdgeIterator::operator++() {
- incrementIterator();
- return *this;
- }
-
- ConstEdgeIterator& ConstEdgeIterator::operator++(int) {
- incrementIterator();
- return *this;
- }
-
- Edge const& ConstEdgeIterator::operator*() const {
- return *in_it;
- }
-
- bool ConstEdgeIterator::operator==(ConstEdgeIterator const& other) const {
- return this->out_it == other.out_it && this->in_it == other.in_it;
- }
-
- bool ConstEdgeIterator::operator!=(ConstEdgeIterator const& other) const {
- return !(*this == other);
- }
-
- void ConstEdgeIterator::incrementIterator() {
- ++in_it;
-
- // If the inner iterator has reached its end move it to the beginning of the next outer element.
- if (in_it == out_it->end()) {
- ++out_it;
- while (out_it != out_ite && out_it->empty()) {
- ++out_it;
- in_it = out_it->end();
- }
- if (out_it != out_ite) {
- in_it = out_it->begin();
- }
- }
- }
-
- Edges::Edges(Automaton& automaton) : automaton(automaton) {
+ ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) {
// Intentionally left empty.
}
- EdgeIterator Edges::begin() {
- auto outer = automaton.edges.begin();
- while (outer != automaton.edges.end() && outer->empty()) {
- ++outer;
- }
- if (outer == automaton.edges.end()) {
- return end();
- } else {
- return EdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
- }
- }
-
- EdgeIterator Edges::end() {
- return EdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
- }
-
- ConstEdges::ConstEdges(Automaton const& automaton) : automaton(automaton) {
- // Intentionally left empty.
+ ConstEdges::const_iterator ConstEdges::begin() const {
+ return it;
}
- ConstEdgeIterator ConstEdges::begin() const {
- auto outer = automaton.edges.begin();
- while (outer != automaton.edges.end() && outer->empty()) {
- ++outer;
- }
- if (outer == automaton.edges.end()) {
- return end();
- } else {
- return ConstEdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
- }
+ ConstEdges::const_iterator ConstEdges::end() const {
+ return ite;
}
-
- ConstEdgeIterator ConstEdges::end() const {
- return ConstEdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
+
+ bool ConstEdges::empty() const {
+ return it == ite;
}
}
Automaton::Automaton(std::string const& name) : name(name) {
- // Intentionally left empty.
+ // Add a sentinel element to the mapping from locations to starting indices.
+ locationToStartingIndex.push_back(0);
}
std::string const& Automaton::getName() const {
@@ -177,7 +86,7 @@ namespace storm {
STORM_LOG_THROW(!this->hasLocation(location.getName()), storm::exceptions::WrongFormatException, "Cannot add location with name '" << location.getName() << "', because a location with this name already exists.");
locationToIndex.emplace(location.getName(), locations.size());
locations.push_back(location);
- edges.push_back(EdgeSet());
+ locationToStartingIndex.push_back(edges.size());
return locations.size() - 1;
}
@@ -204,31 +113,62 @@ namespace storm {
uint64_t Automaton::getInitialLocationIndex() const {
return initialLocationIndex;
}
+
+ Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) {
+ auto it = locationToIndex.find(name);
+ STORM_LOG_THROW(it != locationToIndex.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve edges from unknown location '" << name << ".");
+ return getEdgesFromLocation(it->second);
+ }
+
+ Automaton::Edges Automaton::getEdgesFromLocation(uint64_t index) {
+ auto it = edges.begin();
+ std::advance(it, locationToStartingIndex[index]);
+ auto ite = edges.begin();
+ std::advance(ite, locationToStartingIndex[index + 1]);
+ return Edges(it, ite);
+ }
- EdgeSet const& Automaton::getEdgesFromLocation(std::string const& name) const {
+ Automaton::ConstEdges Automaton::getEdgesFromLocation(std::string const& name) const {
auto it = locationToIndex.find(name);
STORM_LOG_THROW(it != locationToIndex.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve edges from unknown location '" << name << ".");
return getEdgesFromLocation(it->second);
}
- EdgeSet const& Automaton::getEdgesFromLocation(uint64_t index) const {
- return edges[index];
+ Automaton::ConstEdges Automaton::getEdgesFromLocation(uint64_t index) const {
+ auto it = edges.begin();
+ std::advance(it, locationToStartingIndex[index]);
+ auto ite = edges.begin();
+ std::advance(ite, locationToStartingIndex[index + 1]);
+ return ConstEdges(it, ite);
}
void Automaton::addEdge(Edge const& edge) {
STORM_LOG_THROW(edge.getSourceLocationId() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationId() << "'.");
- edges[edge.getSourceLocationId()].addEdge(edge);
+
+ // Find the right position for the edge and insert it properly.
+ auto posIt = edges.begin();
+ std::advance(posIt, locationToStartingIndex[edge.getSourceLocationId() + 1]);
+ edges.insert(posIt, edge);
+
+ // Now update the starting indices of all subsequent locations.
+ for (uint64_t locationIndex = edge.getSourceLocationId() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
+ ++locationToStartingIndex[locationIndex];
+ }
}
- Automaton::Edges Automaton::getEdges() {
- return Edges(*this);
+ std::vector<Edge>& Automaton::getEdges() {
+ return edges;
}
- Automaton::ConstEdges Automaton::getEdges() const {
- return ConstEdges(*this);
+ std::vector<Edge> const& Automaton::getEdges() const {
+ return edges;
}
uint64_t Automaton::getNumberOfLocations() const {
+ return locations.size();
+ }
+
+ uint64_t Automaton::getNumberOfEdges() const {
return edges.size();
}
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index 36a525703..08b803248 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -5,7 +5,7 @@
#include <unordered_map>
#include "src/storage/jani/VariableSet.h"
-#include "src/storage/jani/EdgeSet.h"
+#include "src/storage/jani/Edge.h"
#include "src/storage/jani/Location.h"
namespace storm {
@@ -14,108 +14,58 @@ namespace storm {
class Automaton;
namespace detail {
- class EdgeIterator {
- private:
- typedef std::vector<EdgeSet>::iterator outer_iter;
- typedef EdgeSet::iterator inner_iter;
-
+ class Edges {
public:
- /*!
- * Creates an iterator over all edges.
- */
- EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
-
- // Methods to advance the iterator.
- EdgeIterator& operator++();
- EdgeIterator& operator++(int);
-
- Edge& operator*();
-
- bool operator==(EdgeIterator const& other) const;
- bool operator!=(EdgeIterator const& other) const;
-
- private:
- // Moves the iterator to the next position.
- void incrementIterator();
-
- // The underlying automaton.
- Automaton& automaton;
+ typedef std::vector<Edge>::iterator iterator;
+ typedef std::vector<Edge>::const_iterator const_iterator;
- // The current iterator positions.
- outer_iter out_it;
- outer_iter out_ite;
- inner_iter in_it;
- };
-
- class ConstEdgeIterator {
- private:
- typedef std::vector<EdgeSet>::const_iterator outer_iter;
- typedef EdgeSet::const_iterator inner_iter;
+ Edges(iterator it, iterator ite);
- public:
/*!
- * Creates an iterator over all edges.
+ * Retrieves an iterator to the edges.
*/
- ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
-
- // Methods to advance the iterator.
- ConstEdgeIterator& operator++();
- ConstEdgeIterator& operator++(int);
-
- Edge const& operator*() const;
-
- bool operator==(ConstEdgeIterator const& other) const;
- bool operator!=(ConstEdgeIterator const& other) const;
-
- private:
- // Moves the iterator to the next position.
- void incrementIterator();
-
- // The underlying automaton.
- Automaton const& automaton;
-
- // The current iterator positions.
- outer_iter out_it;
- outer_iter out_ite;
- inner_iter in_it;
- };
-
- class Edges {
- public:
- Edges(Automaton& automaton);
+ iterator begin() const;
/*!
- * Retrieves an iterator to all edges of the automaton.
+ * Retrieves an end iterator to the edges.
*/
- EdgeIterator begin();
+ iterator end() const;
/*!
- * Retrieves the end iterator to edges of the automaton.
+ * Determines whether this set of edges is empty.
*/
- EdgeIterator end();
+ bool empty() const;
private:
- // The underlying automaton.
- Automaton& automaton;
+ iterator it;
+ iterator ite;
};
class ConstEdges {
public:
- ConstEdges(Automaton const& automaton);
+ typedef std::vector<Edge>::iterator iterator;
+ typedef std::vector<Edge>::const_iterator const_iterator;
+
+ ConstEdges(const_iterator it, const_iterator ite);
/*!
- * Retrieves an iterator to all edges of the automaton.
+ * Retrieves an iterator to the edges.
*/
- ConstEdgeIterator begin() const;
+ const_iterator begin() const;
/*!
- * Retrieves the end iterator to edges of the automaton.
+ * Retrieves an end iterator to the edges.
*/
- ConstEdgeIterator end() const;
+ const_iterator end() const;
+
+ /*!
+ * Determines whether this set of edges is empty.
+ */
+ bool empty() const;
private:
- // The underlying automaton.
- Automaton const& automaton;
+ const_iterator it;
+ const_iterator ite;
};
}
@@ -209,16 +159,26 @@ namespace storm {
* Retrieves the index of the initial location.
*/
uint64_t getInitialLocationIndex() const;
+
+ /*!
+ * Retrieves the edges of the location with the given name.
+ */
+ Edges getEdgesFromLocation(std::string const& name);
+
+ /*!
+ * Retrieves the edges of the location with the given index.
+ */
+ Edges getEdgesFromLocation(uint64_t index);
/*!
* Retrieves the edges of the location with the given name.
*/
- EdgeSet const& getEdgesFromLocation(std::string const& name) const;
+ ConstEdges getEdgesFromLocation(std::string const& name) const;
/*!
* Retrieves the edges of the location with the given index.
*/
- EdgeSet const& getEdgesFromLocation(uint64_t index) const;
+ ConstEdges getEdgesFromLocation(uint64_t index) const;
/*!
* Adds an edge to the automaton.
@@ -228,35 +188,44 @@ namespace storm {
/*!
* Retrieves the edges of the automaton.
*/
- Edges getEdges();
+ std::vector<Edge>& getEdges();
/*!
* Retrieves the edges of the automaton.
*/
- ConstEdges getEdges() const;
+ std::vector<Edge> const& getEdges() const;
/*!
* Retrieves the number of locations.
*/
uint64_t getNumberOfLocations() const;
-
+
+ /*!
+ * Retrieves the number of edges.
+ */
+ uint64_t getNumberOfEdges() const;
+
private:
- // The name of the automaton.
+ /// The name of the automaton.
std::string name;
- // The set of variables of this automaton.
+ /// The set of variables of this automaton.
VariableSet variables;
- // The locations of the automaton.
+ /// The locations of the automaton.
std::vector<Location> locations;
- // A mapping of location names to their indices.
+ /// A mapping of location names to their indices.
std::unordered_map<std::string, uint64_t> locationToIndex;
- // All edges of the automaton. The edges at index i are the edges of the location with index i.
- std::vector<EdgeSet> edges;
+ /// All edges of the automaton
+ std::vector<Edge> edges;
+
+ /// A mapping from location indices to the starting indices. If l is mapped to i, it means that the edges
+ /// leaving location l start at index i of the edges vector.
+ std::vector<uint64_t> locationToStartingIndex;
- // The index of the initial location.
+ /// The index of the initial location.
uint64_t initialLocationIndex;
};
diff --git a/src/storage/jani/EdgeSet.cpp b/src/storage/jani/EdgeSet.cpp
deleted file mode 100644
index d71b3f5be..000000000
--- a/src/storage/jani/EdgeSet.cpp
+++ /dev/null
@@ -1,35 +0,0 @@
-#include "src/storage/jani/EdgeSet.h"
-
-namespace storm {
- namespace jani {
-
- EdgeSet::EdgeSet(std::vector<Edge> const& edges) : edges(edges) {
- // Intentionally left empty.
- }
-
- EdgeSet::iterator EdgeSet::begin() {
- return edges.begin();
- }
-
- EdgeSet::iterator EdgeSet::end() {
- return edges.end();
- }
-
- EdgeSet::const_iterator EdgeSet::begin() const {
- return edges.cbegin();
- }
-
- EdgeSet::const_iterator EdgeSet::end() const {
- return edges.cend();
- }
-
- void EdgeSet::addEdge(Edge const& edge) {
- edges.push_back(edge);
- }
-
- bool EdgeSet::empty() const {
- return edges.empty();
- }
-
- }
-}
\ No newline at end of file
diff --git a/src/storage/jani/EdgeSet.h b/src/storage/jani/EdgeSet.h
deleted file mode 100644
index a9e7336ad..000000000
--- a/src/storage/jani/EdgeSet.h
+++ /dev/null
@@ -1,41 +0,0 @@
-#pragma once
-
-#include "src/storage/jani/Edge.h"
-
-namespace storm {
- namespace jani {
-
- class EdgeSet {
- public:
- typedef std::vector<Edge> container_type;
- typedef container_type::iterator iterator;
- typedef container_type::const_iterator const_iterator;
-
- /*!
- * Creates a new set of edges.
- */
- EdgeSet(std::vector<Edge> const& edges = std::vector<Edge>());
-
- /*!
- * Adds the edge to the edges.
- */
- void addEdge(Edge const& edge);
-
- /*!
- * Retrieves whether the set of edges is empty.
- */
- bool empty() const;
-
- // Methods to get an iterator to the edges.
- iterator begin();
- iterator end();
- const_iterator begin() const;
- const_iterator end() const;
-
- private:
- // The set of edges.
- container_type edges;
- };
-
- }
-}
\ No newline at end of file
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index ec0066ed4..1d976d084 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -65,6 +65,10 @@ namespace storm {
return it->second;
}
+ std::vector<Action> const& Model::getActions() const {
+ return actions;
+ }
+
uint64_t Model::addConstant(Constant const& constant) {
auto it = constantToIndex.find(constant.getName());
STORM_LOG_THROW(it == constantToIndex.end(), storm::exceptions::WrongFormatException, "Cannot add constant with name '" << constant.getName() << "', because a constant with that name already exists.");
@@ -147,6 +151,10 @@ namespace storm {
return automata[it->second];
}
+ std::size_t Model::getNumberOfAutomata() const {
+ return automata.size();
+ }
+
std::shared_ptr<Composition> Model::getStandardSystemComposition() const {
std::set<std::string> fullSynchronizationAlphabet = getActionNames(false);
@@ -249,6 +257,7 @@ namespace storm {
// Substitute constants in all global variables.
for (auto& variable : result.getGlobalVariables()) {
+ std::cout << "init: " << variable.getInitialValue() << std::endl;
variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
}
for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index e719f6d96..258f9417d 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -72,6 +72,11 @@ namespace storm {
*/
Action const& getAction(uint64_t index) const;
+ /*!
+ * Retrieves the actions of the model.
+ */
+ std::vector<Action> const& getActions() const;
+
/*!
* Adds the given constant to the model.
*/
@@ -157,6 +162,11 @@ namespace storm {
*/
Automaton const& getAutomaton(std::string const& name) const;
+ /*!
+ * Retrieves the number of automata in this model.
+ */
+ std::size_t getNumberOfAutomata() const;
+
/*!
* Sets the system composition expression of the JANI model.
*/
diff --git a/src/storage/jani/RenameComposition.cpp b/src/storage/jani/RenameComposition.cpp
index a88139fa7..77ab94f5c 100644
--- a/src/storage/jani/RenameComposition.cpp
+++ b/src/storage/jani/RenameComposition.cpp
@@ -20,6 +20,10 @@ namespace storm {
return visitor.visit(*this, data);
}
+ std::map<std::string, boost::optional<std::string>> const& RenameComposition::getRenaming() const {
+ return renaming;
+ }
+
void RenameComposition::write(std::ostream& stream) const {
std::vector<std::string> renamingStrings;
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index e4d37957d..97697e2f7 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -9,190 +9,96 @@ namespace storm {
namespace detail {
- VariableSetIterator::VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
- // Intentionally left empty.
- }
-
- VariableSetIterator& VariableSetIterator::operator++() {
- incrementIterator();
- return *this;
- }
-
- VariableSetIterator& VariableSetIterator::operator++(int) {
- incrementIterator();
- return *this;
- }
-
- Variable& VariableSetIterator::operator*() {
- if (it.which() == 0) {
- return *boost::get<bool_iter>(it);
- } else if (it.which() == 1) {
- return *boost::get<bint_iter>(it);
- } else {
- return *boost::get<int_iter>(it);
- }
- }
-
- bool VariableSetIterator::operator==(VariableSetIterator const& other) const {
- return this->it == other.it;
+ template<typename VariableType>
+ VariableType& Dereferencer<VariableType>::operator()(std::shared_ptr<VariableType> const& d) {
+ return *d;
}
- bool VariableSetIterator::operator!=(VariableSetIterator const& other) const {
- return this->it != other.it;
- }
-
- void VariableSetIterator::incrementIterator() {
- if (it.which() == 0) {
- bool_iter& tmp = boost::get<bool_iter>(it);
- if (tmp != variableSet.getBooleanVariables().end()) {
- ++tmp;
- } else {
- it = variableSet.getBoundedIntegerVariables().begin();
- }
- } else if (it.which() == 1) {
- bint_iter& tmp = boost::get<bint_iter>(it);
- if (tmp != variableSet.getBoundedIntegerVariables().end()) {
- ++tmp;
- } else {
- it = variableSet.getUnboundedIntegerVariables().begin();
- }
- } else {
- ++boost::get<int_iter>(it);
- }
- }
-
- ConstVariableSetIterator::ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
+ template<typename VariableType>
+ Variables<VariableType>::Variables(input_iterator it, input_iterator ite) : it(it), ite(ite) {
// Intentionally left empty.
}
-
- ConstVariableSetIterator& ConstVariableSetIterator::operator++() {
- incrementIterator();
- return *this;
- }
-
- ConstVariableSetIterator& ConstVariableSetIterator::operator++(int) {
- incrementIterator();
- return *this;
- }
-
- Variable const& ConstVariableSetIterator::operator*() {
- if (it.which() == 0) {
- return *boost::get<bool_iter>(it);
- } else if (it.which() == 1) {
- return *boost::get<bint_iter>(it);
- } else {
- return *boost::get<int_iter>(it);
- }
+
+ template<typename VariableType>
+ typename Variables<VariableType>::iterator Variables<VariableType>::begin() {
+ return boost::make_transform_iterator(it, Dereferencer<VariableType>());
}
- bool ConstVariableSetIterator::operator==(ConstVariableSetIterator const& other) const {
- return this->it == other.it;
+ template<typename VariableType>
+ typename Variables<VariableType>::iterator Variables<VariableType>::end() {
+ return boost::make_transform_iterator(ite, Dereferencer<VariableType>());
}
-
- bool ConstVariableSetIterator::operator!=(ConstVariableSetIterator const& other) const {
- return this->it != other.it;
- }
-
- void ConstVariableSetIterator::incrementIterator() {
- if (it.which() == 0) {
- bool_iter& tmp = boost::get<bool_iter>(it);
- if (tmp != variableSet.getBooleanVariables().end()) {
- ++tmp;
- } else {
- it = variableSet.getBoundedIntegerVariables().begin();
- }
- } else if (it.which() == 1) {
- bint_iter& tmp = boost::get<bint_iter>(it);
- if (tmp != variableSet.getBoundedIntegerVariables().end()) {
- ++tmp;
- } else {
- it = variableSet.getUnboundedIntegerVariables().begin();
- }
- } else {
- ++boost::get<int_iter>(it);
- }
- }
-
- IntegerVariables::IntegerVariables(VariableSet& variableSet) : variableSet(variableSet) {
- // Intentionally left empty.
- }
-
- VariableSetIterator IntegerVariables::begin() {
- return VariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
- }
-
- VariableSetIterator IntegerVariables::end() {
- return VariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
- }
-
- ConstIntegerVariables::ConstIntegerVariables(VariableSet const& variableSet) : variableSet(variableSet) {
+
+ template<typename VariableType>
+ ConstVariables<VariableType>::ConstVariables(const_input_iterator it, const_input_iterator ite) : it(it), ite(ite) {
// Intentionally left empty.
}
- ConstVariableSetIterator ConstIntegerVariables::begin() const {
- return ConstVariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
+ template<typename VariableType>
+ typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::begin() {
+ return boost::make_transform_iterator(it, Dereferencer<VariableType>());
}
- ConstVariableSetIterator ConstIntegerVariables::end() const {
- return ConstVariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
+ template<typename VariableType>
+ typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::end() {
+ return boost::make_transform_iterator(ite, Dereferencer<VariableType>());
}
+
}
VariableSet::VariableSet() {
// Intentionally left empty.
}
- std::vector<BooleanVariable>& VariableSet::getBooleanVariables() {
- return booleanVariables;
+ detail::Variables<BooleanVariable> VariableSet::getBooleanVariables() {
+ return detail::Variables<BooleanVariable>(booleanVariables.begin(), booleanVariables.end());
}
- std::vector<BooleanVariable> const& VariableSet::getBooleanVariables() const {
- return booleanVariables;
- }
-
- std::vector<BoundedIntegerVariable>& VariableSet::getBoundedIntegerVariables() {
- return boundedIntegerVariables;
+ detail::ConstVariables<BooleanVariable> VariableSet::getBooleanVariables() const {
+ return detail::ConstVariables<BooleanVariable>(booleanVariables.begin(), booleanVariables.end());
}
- std::vector<BoundedIntegerVariable> const& VariableSet::getBoundedIntegerVariables() const {
- return boundedIntegerVariables;
+ detail::Variables<BoundedIntegerVariable> VariableSet::getBoundedIntegerVariables() {
+ return detail::Variables<BoundedIntegerVariable>(boundedIntegerVariables.begin(), boundedIntegerVariables.end());
}
- std::vector<UnboundedIntegerVariable>& VariableSet::getUnboundedIntegerVariables() {
- return unboundedIntegerVariables;
+ detail::ConstVariables<BoundedIntegerVariable> VariableSet::getBoundedIntegerVariables() const {
+ return detail::ConstVariables<BoundedIntegerVariable>(boundedIntegerVariables.begin(), boundedIntegerVariables.end());
}
- std::vector<UnboundedIntegerVariable> const& VariableSet::getUnboundedIntegerVariables() const {
- return unboundedIntegerVariables;
+ detail::Variables<UnboundedIntegerVariable> VariableSet::getUnboundedIntegerVariables() {
+ return detail::Variables<UnboundedIntegerVariable>(unboundedIntegerVariables.begin(), unboundedIntegerVariables.end());
}
- VariableSet::IntegerVariables VariableSet::getIntegerVariables() {
- return IntegerVariables(*this);
+ detail::ConstVariables<UnboundedIntegerVariable> VariableSet::getUnboundedIntegerVariables() const {
+ return detail::ConstVariables<UnboundedIntegerVariable>(unboundedIntegerVariables.begin(), unboundedIntegerVariables.end());
}
- VariableSet::ConstIntegerVariables VariableSet::getIntegerVariables() const {
- return ConstIntegerVariables(*this);
- }
-
void VariableSet::addBooleanVariable(BooleanVariable const& variable) {
STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
- booleanVariables.push_back(variable);
+ std::shared_ptr<BooleanVariable> newVariable = std::make_shared<BooleanVariable>(variable);
+ variables.push_back(newVariable);
+ booleanVariables.push_back(newVariable);
nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
- variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(0, booleanVariables.size() - 1));
+ variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
}
void VariableSet::addBoundedIntegerVariable(BoundedIntegerVariable const& variable) {
STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
- boundedIntegerVariables.push_back(variable);
+ std::shared_ptr<BoundedIntegerVariable> newVariable = std::make_shared<BoundedIntegerVariable>(variable);
+ variables.push_back(newVariable);
+ boundedIntegerVariables.push_back(newVariable);
nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
- variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(1, boundedIntegerVariables.size() - 1));
+ variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
}
void VariableSet::addUnboundedIntegerVariable(UnboundedIntegerVariable const& variable) {
STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
- unboundedIntegerVariables.push_back(variable);
+ std::shared_ptr<UnboundedIntegerVariable> newVariable = std::make_shared<UnboundedIntegerVariable>(variable);
+ variables.push_back(newVariable);
+ unboundedIntegerVariables.push_back(newVariable);
nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
- variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(2, boundedIntegerVariables.size() - 1));
+ variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
}
bool VariableSet::hasVariable(std::string const& name) const {
@@ -206,36 +112,42 @@ namespace storm {
}
VariableSet::iterator VariableSet::begin() {
- return iterator(*this, booleanVariables.begin());
+ return boost::make_transform_iterator(variables.begin(), detail::Dereferencer<Variable>());
}
VariableSet::const_iterator VariableSet::begin() const {
- return const_iterator(*this, booleanVariables.begin());
+ return boost::make_transform_iterator(variables.begin(), detail::Dereferencer<Variable const>());
}
VariableSet::iterator VariableSet::end() {
- return iterator(*this, unboundedIntegerVariables.end());
+ return boost::make_transform_iterator(variables.end(), detail::Dereferencer<Variable>());
}
VariableSet::const_iterator VariableSet::end() const {
- return const_iterator(*this, unboundedIntegerVariables.end());
+ return boost::make_transform_iterator(variables.end(), detail::Dereferencer<Variable const>());
}
Variable const& VariableSet::getVariable(storm::expressions::Variable const& variable) const {
auto it = variableToVariable.find(variable);
STORM_LOG_THROW(it != variableToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << variable.getName() << "'.");
-
- if (it->second.first == 0) {
- return booleanVariables[it->second.second];
- } else if (it->second.first == 1) {
- return boundedIntegerVariables[it->second.second];
- } else {
- return unboundedIntegerVariables[it->second.second];
- }
+ return *it->second;
}
bool VariableSet::hasVariable(storm::expressions::Variable const& variable) const {
return variableToVariable.find(variable) != variableToVariable.end();
}
+
+ bool VariableSet::containsBooleanVariable() const {
+ return !booleanVariables.empty();
+ }
+
+ bool VariableSet::containsBoundedIntegerVariable() const {
+ return !boundedIntegerVariables.empty();
+ }
+
+ bool VariableSet::containsUnboundedIntegerVariables() const {
+ return !unboundedIntegerVariables.empty();
+ }
+
}
}
\ No newline at end of file
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index 8c8ec6815..058e56457 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -3,7 +3,7 @@
#include <vector>
#include <set>
-#include <boost/variant.hpp>
+#include <boost/iterator/transform_iterator.hpp>
#include "src/storage/jani/BooleanVariable.h"
#include "src/storage/jani/UnboundedIntegerVariable.h"
@@ -16,117 +16,55 @@ namespace storm {
namespace detail {
- class VariableSetIterator {
- private:
- typedef std::vector<BooleanVariable>::iterator bool_iter;
- typedef std::vector<BoundedIntegerVariable>::iterator bint_iter;
- typedef std::vector<UnboundedIntegerVariable>::iterator int_iter;
-
+ template<typename VariableType>
+ class Dereferencer {
public:
- /*!
- * Creates an iterator over all variables.
- */
- VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
-
- // Methods to advance the iterator.
- VariableSetIterator& operator++();
- VariableSetIterator& operator++(int);
-
- Variable& operator*();
-
- bool operator==(VariableSetIterator const& other) const;
- bool operator!=(VariableSetIterator const& other) const;
-
- private:
- // Moves the iterator to the next position.
- void incrementIterator();
-
- // The underlying variable set.
- VariableSet& variableSet;
-
- // The current iterator position.
- boost::variant<bool_iter, bint_iter, int_iter> it;
+ VariableType& operator()(std::shared_ptr<VariableType> const& d);
};
- class ConstVariableSetIterator {
- private:
- typedef std::vector<BooleanVariable>::const_iterator bool_iter;
- typedef std::vector<BoundedIntegerVariable>::const_iterator bint_iter;
- typedef std::vector<UnboundedIntegerVariable>::const_iterator int_iter;
-
+ template<typename VariableType>
+ class Variables {
public:
- /*!
- * Creates an iterator over all variables.
- */
- ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
-
- // Methods to advance the iterator.
- ConstVariableSetIterator& operator++();
- ConstVariableSetIterator& operator++(int);
-
- Variable const& operator*();
-
- bool operator==(ConstVariableSetIterator const& other) const;
- bool operator!=(ConstVariableSetIterator const& other) const;
-
- private:
- // Moves the iterator to the next position.
- void incrementIterator();
-
- // The underlying variable set.
- VariableSet const& variableSet;
+ typedef typename std::vector<std::shared_ptr<VariableType>>::iterator input_iterator;
+ typedef typename std::vector<std::shared_ptr<VariableType>>::const_iterator const_input_iterator;
+ typedef boost::transform_iterator<Dereferencer<VariableType>, input_iterator> iterator;
+ typedef boost::transform_iterator<Dereferencer<VariableType const>, const_input_iterator> const_iterator;
- // The current iterator position.
- boost::variant<bool_iter, bint_iter, int_iter> it;
- };
-
- class IntegerVariables {
- public:
- IntegerVariables(VariableSet& variableSet);
+ Variables(input_iterator it, input_iterator ite);
- /*!
- * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
- */
- VariableSetIterator begin();
-
- /*!
- * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
- */
- VariableSetIterator end();
+ iterator begin();
+ iterator end();
private:
- // The underlying variable set.
- VariableSet& variableSet;
+ input_iterator it;
+ input_iterator ite;
};
-
- class ConstIntegerVariables {
+
+ template<typename VariableType>
+ class ConstVariables {
public:
- ConstIntegerVariables(VariableSet const& variableSet);
+ typedef typename std::vector<std::shared_ptr<VariableType>>::iterator input_iterator;
+ typedef typename std::vector<std::shared_ptr<VariableType>>::const_iterator const_input_iterator;
+ typedef boost::transform_iterator<Dereferencer<VariableType>, input_iterator> iterator;
+ typedef boost::transform_iterator<Dereferencer<VariableType const>, const_input_iterator> const_iterator;
- /*!
- * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
- */
- ConstVariableSetIterator begin() const;
+ ConstVariables(const_input_iterator it, const_input_iterator ite);
- /*!
- * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
- */
- ConstVariableSetIterator end() const;
+ const_iterator begin();
+ const_iterator end();
private:
- // The underlying variable set.
- VariableSet const& variableSet;
+ input_iterator it;
+ input_iterator ite;
};
}
class VariableSet {
public:
- friend class detail::VariableSetIterator;
-
- typedef detail::VariableSetIterator iterator;
- typedef detail::ConstVariableSetIterator const_iterator;
- typedef detail::IntegerVariables IntegerVariables;
- typedef detail::ConstIntegerVariables ConstIntegerVariables;
+ typedef typename std::vector<std::shared_ptr<Variable>>::iterator input_iterator;
+ typedef typename std::vector<std::shared_ptr<Variable>>::const_iterator const_input_iterator;
+ typedef boost::transform_iterator<detail::Dereferencer<Variable>, input_iterator> iterator;
+ typedef boost::transform_iterator<detail::Dereferencer<Variable>, const_input_iterator> const_iterator;
/*!
* Creates an empty variable set.
@@ -136,42 +74,32 @@ namespace storm {
/*!
* Retrieves the boolean variables in this set.
*/
- std::vector<BooleanVariable>& getBooleanVariables();
+ detail::Variables<BooleanVariable> getBooleanVariables();
/*!
* Retrieves the boolean variables in this set.
*/
- std::vector<BooleanVariable> const& getBooleanVariables() const;
+ detail::ConstVariables<BooleanVariable> getBooleanVariables() const;
/*!
* Retrieves the bounded integer variables in this set.
*/
- std::vector<BoundedIntegerVariable>& getBoundedIntegerVariables();
+ detail::Variables<BoundedIntegerVariable> getBoundedIntegerVariables();
/*!
* Retrieves the bounded integer variables in this set.
*/
- std::vector<BoundedIntegerVariable> const& getBoundedIntegerVariables() const;
+ detail::ConstVariables<BoundedIntegerVariable> getBoundedIntegerVariables() const;
/*!
* Retrieves the unbounded integer variables in this set.
*/
- std::vector<UnboundedIntegerVariable>& getUnboundedIntegerVariables();
+ detail::Variables<UnboundedIntegerVariable> getUnboundedIntegerVariables();
/*!
* Retrieves the unbounded integer variables in this set.
*/
- std::vector<UnboundedIntegerVariable> const& getUnboundedIntegerVariables() const;
-
- /*!
- * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
- */
- IntegerVariables getIntegerVariables();
-
- /*!
- * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
- */
- ConstIntegerVariables getIntegerVariables() const;
+ detail::ConstVariables<UnboundedIntegerVariable> getUnboundedIntegerVariables() const;
/*!
* Adds the given boolean variable to this set.
@@ -228,21 +156,39 @@ namespace storm {
*/
const_iterator end() const;
+ /*!
+ * Retrieves whether the set of variables contains a boolean variable.
+ */
+ bool containsBooleanVariable() const;
+
+ /*!
+ * Retrieves whether the set of variables contains a bounded integer variable.
+ */
+ bool containsBoundedIntegerVariable() const;
+
+ /*!
+ * Retrieves whether the set of variables contains an unbounded integer variable.
+ */
+ bool containsUnboundedIntegerVariables() const;
+
private:
+ /// The vector of all variables.
+ std::vector<std::shared_ptr<Variable>> variables;
+
/// The boolean variables in this set.
- std::vector<BooleanVariable> booleanVariables;
+ std::vector<std::shared_ptr<BooleanVariable>> booleanVariables;
/// The bounded integer variables in this set.
- std::vector<BoundedIntegerVariable> boundedIntegerVariables;
+ std::vector<std::shared_ptr<BoundedIntegerVariable>> boundedIntegerVariables;
/// The unbounded integer variables in this set.
- std::vector<UnboundedIntegerVariable> unboundedIntegerVariables;
+ std::vector<std::shared_ptr<UnboundedIntegerVariable>> unboundedIntegerVariables;
/// A set of all variable names currently in use.
std::map<std::string, storm::expressions::Variable> nameToVariable;
/// A mapping from expression variables to their variable objects.
- std::map<storm::expressions::Variable, std::pair<uint8_t, uint64_t>> variableToVariable;
+ std::map<storm::expressions::Variable, std::shared_ptr<Variable>> variableToVariable;
};
}
diff --git a/test/functional/.DS_Store b/test/functional/.DS_Store
deleted file mode 100644
index 31a582c70..000000000
Binary files a/test/functional/.DS_Store and /dev/null differ
diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp
new file mode 100644
index 000000000..6b73c1a59
--- /dev/null
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@@ -0,0 +1,75 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Ctmc.h"
+#include "src/models/symbolic/Mdp.h"
+
+#include "src/storage/dd/Add.h"
+#include "src/storage/dd/Bdd.h"
+
+#include "src/models/symbolic/StandardRewardModel.h"
+#include "src/parser/PrismParser.h"
+#include "src/builder/DdJaniModelBuilder.h"
+
+TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+ storm::jani::Model janiModel = program.toJani();
+
+ storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
+ EXPECT_EQ(13ul, model->getNumberOfStates());
+ EXPECT_EQ(20ul, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+ janiModel = program.toJani();
+ builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+ model = builder.translate();
+ EXPECT_EQ(677ul, model->getNumberOfStates());
+ EXPECT_EQ(867ul, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+ janiModel = program.toJani();
+ model = builder.translate();
+ EXPECT_EQ(8607ul, model->getNumberOfStates());
+ EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+ janiModel = program.toJani();
+ model = builder.translate();
+ EXPECT_EQ(273ul, model->getNumberOfStates());
+ EXPECT_EQ(397ul, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+ janiModel = program.toJani();
+ model = builder.translate();
+ EXPECT_EQ(1728ul, model->getNumberOfStates());
+ EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+}
+
+//TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
+// storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+//
+// std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+// EXPECT_EQ(13ul, model->getNumberOfStates());
+// EXPECT_EQ(20ul, model->getNumberOfTransitions());
+//
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+// model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+// EXPECT_EQ(677ul, model->getNumberOfStates());
+// EXPECT_EQ(867ul, model->getNumberOfTransitions());
+//
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+// model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+// EXPECT_EQ(8607ul, model->getNumberOfStates());
+// EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+//
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+// model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+// EXPECT_EQ(273ul, model->getNumberOfStates());
+// EXPECT_EQ(397ul, model->getNumberOfTransitions());
+//
+// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+// model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+// EXPECT_EQ(1728ul, model->getNumberOfStates());
+// EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+//}
\ No newline at end of file