From 82023d280d50947bf74c2d63a2cbae64e9a49ae5 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 3 Jun 2016 15:09:52 +0200
Subject: [PATCH] JANI model builder for MDPs is working now, but too slow
Former-commit-id: 8b36f65251bed031701fe51760ce6350afd37c0f
---
src/builder/DdJaniModelBuilder.cpp | 298 ++++++++++++------
src/builder/DdPrismModelBuilder.cpp | 8 +-
src/models/symbolic/NondeterministicModel.cpp | 6 +-
src/storage/dd/Dd.h | 16 +-
.../builder/DdJaniModelBuilderTest.cpp | 4 +-
.../builder/DdPrismModelBuilderTest.cpp | 2 -
6 files changed, 212 insertions(+), 122 deletions(-)
diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index d76da2f74..51fe6f36f 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -26,6 +26,7 @@
#include "src/utility/macros.h"
#include "src/utility/jani.h"
#include "src/utility/dd.h"
+#include "src/utility/math.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
@@ -161,7 +162,7 @@ namespace storm {
// 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, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationVariableMap;
@@ -170,7 +171,7 @@ namespace storm {
// The meta variables used to encode the remaining nondeterminism.
std::vector<storm::expressions::Variable> localNondeterminismVariables;
-
+
// The meta variables used to encode the actions and nondeterminism.
std::set<storm::expressions::Variable> allNondeterminismVariables;
@@ -236,16 +237,6 @@ namespace storm {
CompositionVariables<Type, ValueType> createVariables() {
CompositionVariables<Type, ValueType> result;
- for (auto const& automaton : this->model.getAutomata()) {
- // 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() - 1);
- result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
-
- // Add the location variable to the row/column variables.
- result.rowMetaVariables.insert(variablePair.first);
- result.columnMetaVariables.insert(variablePair.second);
- }
-
for (auto const& action : this->model.getActions()) {
if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName());
@@ -265,6 +256,16 @@ namespace storm {
result.allNondeterminismVariables.insert(variablePair.first);
}
+ for (auto const& automaton : this->model.getAutomata()) {
+ // 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() - 1);
+ result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
+
+ // Add the location variable to the row/column variables.
+ result.rowMetaVariables.insert(variablePair.first);
+ result.columnMetaVariables.insert(variablePair.second);
+ }
+
// Create global variables.
storm::dd::Bdd<Type> globalVariableRanges = result.manager->getBddOne();
for (auto const& variable : this->model.getGlobalVariables()) {
@@ -272,7 +273,7 @@ namespace storm {
globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
}
result.globalVariableRanges = globalVariableRanges.template toAdd<ValueType>();
-
+
// Create the variables for the individual automata.
for (auto const& automaton : this->model.getAutomata()) {
storm::dd::Bdd<Type> identity = result.manager->getBddOne();
@@ -408,13 +409,14 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
EdgeDd<Type, ValueType> composeEdgesInParallel(EdgeDd<Type, ValueType> const& edge1, EdgeDd<Type, ValueType> const& edge2) {
EdgeDd<Type, ValueType> result;
-
+
// Compose the guards.
result.guardDd = edge1.guardDd * edge2.guardDd;
// If the composed guard is already zero, we can immediately return an empty result.
if (result.guardDd.isZero()) {
result.transitionsDd = edge1.transitionsDd.getDdManager().template getAddZero<ValueType>();
+ return result;
}
// Compute the set of variables written multiple times by the composition.
@@ -571,7 +573,7 @@ namespace storm {
// 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;
@@ -654,7 +656,7 @@ namespace storm {
// Add the source location and the guard.
transitionsDd *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard;
-
+
// If we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeUpdate.empty()) {
transitionsDd *= variables.globalVariableRanges;
@@ -697,18 +699,14 @@ namespace storm {
};
template <storm::dd::DdType Type, typename ValueType>
- storm::dd::Add<Type, ValueType> encodeAction(boost::optional<uint64_t> trueIndex, std::vector<storm::expressions::Variable> const& actionVariables, CompositionVariables<Type, ValueType> const& variables) {
+ storm::dd::Add<Type, ValueType> encodeAction(boost::optional<uint64_t> const& actionIndex, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> encoding = variables.manager->template getAddOne<ValueType>();
-
- if (trueIndex) {
- *trueIndex = actionVariables.size() - (*trueIndex + 1);
- }
- uint64_t index = 0;
- for (auto it = actionVariables.rbegin(), ite = actionVariables.rend(); it != ite; ++it, ++index) {
- if (trueIndex && index == trueIndex) {
- encoding *= variables.manager->getEncoding(*it, 1).template toAdd<ValueType>();
+
+ for (auto it = variables.actionVariablesMap.rbegin(), ite = variables.actionVariablesMap.rend(); it != ite; ++it) {
+ if (actionIndex && it->first == actionIndex.get()) {
+ encoding *= variables.manager->getEncoding(it->second, 1).template toAdd<ValueType>();
} else {
- encoding *= variables.manager->getEncoding(*it, 0).template toAdd<ValueType>();
+ encoding *= variables.manager->getEncoding(it->second, 0).template toAdd<ValueType>();
}
}
@@ -727,17 +725,15 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
- storm::dd::Add<Type, ValueType> encodeIndex(uint64_t index, std::vector<storm::expressions::Variable> const& localNondeterminismVariables, CompositionVariables<Type, ValueType> const& variables) {
+ storm::dd::Add<Type, ValueType> encodeIndex(uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
- STORM_LOG_TRACE("Encoding " << index << " with " << localNondeterminismVariables.size() << " binary variable(s).");
-
std::map<storm::expressions::Variable, int_fast64_t> metaVariableNameToValueMap;
- for (uint_fast64_t i = 0; i < localNondeterminismVariables.size(); ++i) {
- if (index & (1ull << (localNondeterminismVariables.size() - i - 1))) {
- metaVariableNameToValueMap.emplace(localNondeterminismVariables[i], 1);
+ for (uint_fast64_t i = 0; i < numberOfLocalNondeterminismVariables; ++i) {
+ if (index & (1ull << (numberOfLocalNondeterminismVariables - i - 1))) {
+ metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 1);
} else {
- metaVariableNameToValueMap.emplace(localNondeterminismVariables[i], 0);
+ metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 0);
}
}
@@ -746,8 +742,8 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
- 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) {
+ struct BuilderResult {
+ BuilderResult(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.
}
@@ -757,66 +753,136 @@ namespace storm {
};
template <storm::dd::DdType Type, typename ValueType>
- SystemDd<Type, ValueType> buildSystemDd(storm::jani::Model const& model, AutomatonDd<Type, ValueType> const& automatonDd, CompositionVariables<Type, ValueType>& 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.
- std::vector<storm::expressions::Variable> orderedActionVariables;
- std::set<storm::expressions::Variable> actionVariables;
- std::map<uint64_t, boost::optional<uint64_t>> actionIndexToVariableIndex;
- uint64_t maximalNumberOfEdgesPerAction = 0;
- for (auto const& action : automatonDd.actionIndexToEdges) {
- if (action.first != model.getSilentActionIndex()) {
- orderedActionVariables.push_back(variables.actionVariablesMap.at(action.first));
- actionVariables.insert(orderedActionVariables.back());
- actionIndexToVariableIndex[action.first] = orderedActionVariables.size() - 1;
- } else {
- actionIndexToVariableIndex[action.first] = boost::none;
- }
- maximalNumberOfEdgesPerAction = std::max(maximalNumberOfEdgesPerAction, static_cast<uint64_t>(action.second.size()));
- }
-
- // If the maximal number of edges per action is zero, which can happen if the model only has unsatisfiable guards,
- // then we must not compute the number of variables.
- if (maximalNumberOfEdgesPerAction == 0) {
- return SystemDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>(), 0);
- }
+ storm::dd::Add<Type, ValueType> combineEdgesBySummation(std::vector<EdgeDd<Type, ValueType>> const& edges, CompositionVariables<Type, ValueType> const& variables) {
+ storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+ for (auto const& edge : edges) {
+ // Simply add all actions, but make sure to include the missing global variable identities.
+ result += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables);
+ }
+ return result;
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ std::pair<uint64_t, storm::dd::Add<Type, ValueType>> combineEdgesByNondeterministicChoice(std::vector<EdgeDd<Type, ValueType>>& edges, CompositionVariables<Type, ValueType> const& variables) {
+ // Complete all edges by adding the missing global variable identities.
+ for (auto& edge : edges) {
+ edge.transitionsDd *= computeMissingGlobalVariableIdentities(edge, variables);
+ }
+
+ // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
+ storm::dd::Add<Type, ValueType> sumOfGuards = variables.manager->template getAddZero<ValueType>();
+ for (auto const& edge : edges) {
+ sumOfGuards += edge.guardDd;
+ }
+ uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
+ STORM_LOG_TRACE("Found " << maxChoices << " local choices.");
+
+ // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism.
+ if (maxChoices == 0) {
+ return std::make_pair(0, variables.manager->template getAddZero<ValueType>());
+ } else if (maxChoices == 1) {
+ return std::make_pair(0, combineEdgesBySummation(edges, variables));
+ } else {
+ // Calculate number of required variables to encode the nondeterminism.
+ uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
- uint64_t numberOfNondeterminismVariables = static_cast<uint64_t>(std::ceil(std::log2(maximalNumberOfEdgesPerAction)));
- std::vector<storm::expressions::Variable> localNondeterminismVariables(numberOfNondeterminismVariables);
- std::copy(variables.localNondeterminismVariables.begin(), variables.localNondeterminismVariables.begin() + numberOfNondeterminismVariables, localNondeterminismVariables.begin());
+ storm::dd::Add<Type, ValueType> allEdges = variables.manager->template getAddZero<ValueType>();
- // Prepare result.
- storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+ storm::dd::Bdd<Type> equalsNumberOfChoicesDd;
+ std::vector<storm::dd::Add<Type, ValueType>> choiceDds(maxChoices, variables.manager->template getAddZero<ValueType>());
+ std::vector<storm::dd::Bdd<Type>> remainingDds(maxChoices, variables.manager->getBddZero());
- // Add edges to the result.
- for (auto const& action : automatonDd.actionIndexToEdges) {
- storm::dd::Add<Type, ValueType> edgesForAction = variables.manager->template getAddZero<ValueType>();
+ for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
+ // Determine the set of states with exactly currentChoices choices.
+ equalsNumberOfChoicesDd = sumOfGuards.equals(variables.manager->getConstant(static_cast<double>(currentChoices)));
+
+ // If there is no such state, continue with the next possible number of choices.
+ if (equalsNumberOfChoicesDd.isZero()) {
+ continue;
+ }
- uint64_t edgeIndex = 0;
- for (auto const& edge : action.second) {
- storm::dd::Add<Type, ValueType> dd = edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, localNondeterminismVariables, variables);
- dd.exportToDot("add" + std::to_string(edgeIndex) + ".dot");
- edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, localNondeterminismVariables, variables);
- ++edgeIndex;
+ // Reset the previously used intermediate storage.
+ for (uint_fast64_t j = 0; j < currentChoices; ++j) {
+ choiceDds[j] = variables.manager->template getAddZero<ValueType>();
+ remainingDds[j] = equalsNumberOfChoicesDd;
}
- result += edgesForAction * encodeAction<Type, ValueType>(actionIndexToVariableIndex.at(action.first), orderedActionVariables, variables);
+ for (std::size_t j = 0; j < edges.size(); ++j) {
+ // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices
+ // choices such that one outgoing choice is given by the j-th edge.
+ storm::dd::Bdd<Type> guardChoicesIntersection = edges[j].guardDd.toBdd() && equalsNumberOfChoicesDd;
+
+ // If there is no such state, continue with the next command.
+ if (guardChoicesIntersection.isZero()) {
+ continue;
+ }
+
+ // Split the currentChoices nondeterministic choices.
+ for (uint_fast64_t k = 0; k < currentChoices; ++k) {
+ // Calculate the overlapping part of command guard and the remaining DD.
+ storm::dd::Bdd<Type> remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k];
+
+ // Check if we can add some overlapping parts to the current index.
+ if (!remainingGuardChoicesIntersection.isZero()) {
+ // Remove overlapping parts from the remaining DD.
+ remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection;
+
+ // Combine the overlapping part of the guard with command updates and add it to the resulting DD.
+ choiceDds[k] += remainingGuardChoicesIntersection.template toAdd<ValueType>() * edges[j].transitionsDd;
+ }
+
+ // Remove overlapping parts from the command guard DD
+ guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection;
+
+ // If the guard DD has become equivalent to false, we can stop here.
+ if (guardChoicesIntersection.isZero()) {
+ break;
+ }
+ }
+ }
+
+ // Add the meta variables that encode the nondeterminisim to the different choices.
+ for (uint_fast64_t j = 0; j < currentChoices; ++j) {
+ allEdges += encodeIndex(j, 0, numberOfBinaryVariables, variables) * choiceDds[j];
+ }
+
+ // Delete currentChoices out of overlapping DD
+ sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
}
- return SystemDd<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables), numberOfNondeterminismVariables);
+ return std::make_pair(numberOfBinaryVariables, allEdges);
+ }
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ BuilderResult<Type, ValueType> buildSystemFromSingleAutomaton(storm::jani::Model const& model, AutomatonDd<Type, ValueType>& 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) {
+ std::map<uint64_t, std::pair<uint64_t, storm::dd::Add<Type, ValueType>>> actionIndexToUsedVariablesAndDd;
+
+ // Combine the edges of each action individually and keep track of how many local nondeterminism variables
+ // were used.
+ uint64_t highestNumberOfUsedNondeterminismVariables = 0;
+ for (auto& action : automatonDd.actionIndexToEdges) {
+ std::pair<uint64_t, storm::dd::Add<Type, ValueType>> usedVariablesAndDd = combineEdgesByNondeterministicChoice<Type, ValueType>(action.second, variables);
+ actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd);
+ highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first);
+ }
+
+ storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
+ for (auto const& element : actionIndexToUsedVariablesAndDd) {
+ result += element.second.second * encodeAction(element.first, variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, variables);
+ }
+
+ return BuilderResult<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables), highestNumberOfUsedNondeterminismVariables);
} 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>();
for (auto const& action : automatonDd.actionIndexToEdges) {
- for (auto const& edge : action.second) {
- result += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables);
- }
+ result += combineEdgesBySummation(action.second, variables);
}
-
- return SystemDd<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables));
+ return BuilderResult<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables));
}
-
+
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
}
@@ -839,17 +905,31 @@ namespace storm {
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}
-
}
template <storm::dd::DdType Type, typename ValueType>
- void postprocessSystemAndVariables(storm::jani::Model const& model, SystemDd<Type, ValueType>& system, CompositionVariables<Type, ValueType>& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
- // Get rid of the nondeterminism variables that were not used.
+ void postprocessVariables(storm::jani::ModelType const& modelType, BuilderResult<Type, ValueType>& system, CompositionVariables<Type, ValueType>& variables) {
+ // Add all action/row/column variables to the DD. If we omitted multiplying edges in the construction, this will
+ // introduce the variables so they can later be abstracted without raising an error.
+ system.transitionsDd.addMetaVariables(variables.rowMetaVariables);
+ system.transitionsDd.addMetaVariables(variables.columnMetaVariables);
+
+ // If the model is an MDP, we also add all action variables.
+ if (modelType == storm::jani::ModelType::MDP) {
+ for (auto const& actionVariablePair : variables.actionVariablesMap) {
+ system.transitionsDd.addMetaVariable(actionVariablePair.second);
+ }
+ }
+
+ // Get rid of the local nondeterminism variables that were not used.
for (uint64_t index = system.numberOfNondeterminismVariables; index < variables.localNondeterminismVariables.size(); ++index) {
variables.allNondeterminismVariables.erase(variables.localNondeterminismVariables[index]);
}
variables.localNondeterminismVariables.resize(system.numberOfNondeterminismVariables);
-
+ }
+
+ template <storm::dd::DdType Type, typename ValueType>
+ void postprocessSystem(storm::jani::Model const& model, BuilderResult<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;
@@ -933,43 +1013,61 @@ namespace storm {
}
}
+ template <storm::dd::DdType Type, typename ValueType>
+ class SeparateEdgesSystemBuilder {
+ public:
+ SeparateEdgesSystemBuilder(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : model(model), variables(variables) {
+ // Intentional
+ }
+
+ BuilderResult<Type, ValueType> build() {
+ // Compose the automata to a single automaton.
+ AutomatonComposer<Type, ValueType> composer(this->model, variables);
+ AutomatonDd<Type, ValueType> globalAutomaton = composer.compose();
+
+ // Combine the edges of the single automaton to the full system DD.
+ return buildSystemFromSingleAutomaton<Type, ValueType>(this->model, globalAutomaton, variables);
+ }
+
+ private:
+ storm::jani::Model const& model;
+ CompositionVariables<Type, ValueType> const& variables;
+ };
+
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> globalAutomaton = composer.compose();
-
- // Combine the edges of the single automaton to the full system DD.
- SystemDd<Type, ValueType> system = buildSystemDd(*this->model, globalAutomaton, variables);
+ // Create a builder to compose and build the model.
+ SeparateEdgesSystemBuilder<Type, ValueType> builder(*this->model, variables);
+ BuilderResult<Type, ValueType> system = builder.build();
+
+ // Postprocess the variables in place.
+ postprocessVariables(this->model->getModelType(), system, variables);
- // Postprocess the system. This modifies the systemDd in place.
- postprocessSystemAndVariables(*this->model, system, variables, options);
+ // Postprocess the system in place.
+ postprocessSystem(*this->model, system, variables, options);
// Start creating the model components.
ModelComponents<Type, ValueType> modelComponents;
// Build initial states.
modelComponents.initialStates = computeInitialStates(*this->model, variables);
-
+
// Perform reachability analysis to obtain reachable states.
- system.transitionsDd.exportToDot("trans.dot");
- std::cout << "nnz: " << system.transitionsDd.getNonZeroCount() << std::endl;
- std::cout << "size: " << system.transitionsDd.getNodeCount() << std::endl;
storm::dd::Bdd<Type> transitionMatrixBdd = system.transitionsDd.notZero();
if (this->model->getModelType() == storm::jani::ModelType::MDP) {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables);
}
modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables);
-
+
// Cut transitions to reachable states.
storm::dd::Add<Type, ValueType> reachableStatesAdd = modelComponents.reachableStates.template toAdd<ValueType>();
modelComponents.transitionMatrix = system.transitionsDd * reachableStatesAdd;
system.stateActionDd *= reachableStatesAdd;
-
+
// Fix deadlocks if existing.
fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index db2567e2c..f03ca33a4 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -1103,7 +1103,7 @@ namespace storm {
typename DdPrismModelBuilder<Type, ValueType>::SystemResult DdPrismModelBuilder<Type, ValueType>::createSystemDecisionDiagram(GenerationInformation& generationInfo) {
ModuleComposer<Type, ValueType> composer(generationInfo);
ModuleDecisionDiagram system = composer.compose(generationInfo.program.specifiesSystemComposition() ? generationInfo.program.getSystemCompositionConstruct().getSystemComposition() : *generationInfo.program.getDefaultSystemComposition());
-
+
storm::dd::Add<Type, ValueType> result = createSystemFromModule(generationInfo, system);
// Create an auxiliary DD that is used later during the construction of reward models.
@@ -1324,11 +1324,7 @@ namespace storm {
// Cut the transitions and rewards to the reachable fragment of the state space.
storm::dd::Bdd<Type> initialStates = createInitialStatesDecisionDiagram(generationInfo);
-
- transitionMatrix.exportToDot("trans_prism.dot");
- std::cout << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
- std::cout << "size: " << transitionMatrix.getNodeCount() << std::endl;
-
+
storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero();
if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);
diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp
index 2eac2ccf5..1ac1b5436 100644
--- a/src/models/symbolic/NondeterministicModel.cpp
+++ b/src/models/symbolic/NondeterministicModel.cpp
@@ -33,10 +33,10 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
uint_fast64_t NondeterministicModel<Type, ValueType>::getNumberOfChoices() const {
- std::set<storm::expressions::Variable> rowAndNondeterminsmVariables;
- std::set_union(this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), this->getRowVariables().begin(), this->getRowVariables().end(), std::inserter(rowAndNondeterminsmVariables, rowAndNondeterminsmVariables.begin()));
+ std::set<storm::expressions::Variable> rowAndNondeterminismVariables;
+ std::set_union(this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), this->getRowVariables().begin(), this->getRowVariables().end(), std::inserter(rowAndNondeterminismVariables, rowAndNondeterminismVariables.begin()));
- storm::dd::Add<Type, uint_fast64_t> tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).template toAdd<uint_fast64_t>().sumAbstract(rowAndNondeterminsmVariables);
+ storm::dd::Add<Type, uint_fast64_t> tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).template toAdd<uint_fast64_t>().sumAbstract(rowAndNondeterminismVariables);
return tmp.getValue();
}
diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h
index 30a0c3b97..18605c259 100644
--- a/src/storage/dd/Dd.h
+++ b/src/storage/dd/Dd.h
@@ -109,14 +109,6 @@ namespace storm {
*/
std::set<storm::expressions::Variable>& getContainedMetaVariables();
- protected:
- /*!
- * Retrieves the (sorted) list of the variable indices of DD variables contained in this DD.
- *
- * @return The sorted list of variable indices.
- */
- std::vector<uint_fast64_t> getSortedVariableIndices() const;
-
/*!
* Adds the given set of meta variables to the DD.
*
@@ -145,6 +137,14 @@ namespace storm {
*/
void removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables);
+ protected:
+ /*!
+ * Retrieves the (sorted) list of the variable indices of DD variables contained in this DD.
+ *
+ * @return The sorted list of variable indices.
+ */
+ std::vector<uint_fast64_t> getSortedVariableIndices() const;
+
/*!
* Creates a DD with the given manager and meta variables.
*
diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp
index 24c372693..083beaf9e 100644
--- a/test/functional/builder/DdJaniModelBuilderTest.cpp
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@@ -270,9 +270,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(364ul, mdp->getNumberOfStates());
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
-
- exit(-1);
-
+
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index bfaffc1f3..fe0e00def 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -211,8 +211,6 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
- exit(-1);
-
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);