From efda4e2950a76bf1c1f96b0145f49a551dfadc66 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 7 Jun 2016 18:13:26 +0200 Subject: [PATCH] changed the ordering of operations a bit to get more performance Former-commit-id: 90fc1243f1682106d1c59c84a0de31e366e28adc --- src/builder/DdJaniModelBuilder.cpp | 99 ++++++++--------------------- src/builder/DdPrismModelBuilder.cpp | 18 +----- 2 files changed, 29 insertions(+), 88 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 92bea7da7..a889f54d5 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -180,6 +180,9 @@ namespace storm { // DDs representing the identity for each variable. std::map> variableToIdentityMap; + // DDs representing the ranges of each variable. + std::map> variableToRangeMap; + // A set of all meta variables that correspond to global variables. std::set allGlobalVariables; @@ -266,6 +269,10 @@ namespace storm { // Add the location variable to the row/column variables. result.rowMetaVariables.insert(variablePair.first); result.columnMetaVariables.insert(variablePair.second); + + // Add the legal range for the location variables. + result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first)); + result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second)); } // Create global variables. @@ -327,6 +334,8 @@ namespace storm { storm::dd::Add variableIdentity = result.manager->template getIdentity(variablePair.first).equals(result.manager->template getIdentity(variablePair.second)).template toAdd() * result.manager->getRange(variablePair.first).template toAdd() * result.manager->getRange(variablePair.second).template toAdd(); result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity); result.rowColumnMetaVariablePairs.push_back(variablePair); + result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first)); + result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second)); result.allGlobalVariables.insert(variable.getExpressionVariable()); } @@ -345,6 +354,9 @@ namespace storm { storm::dd::Add variableIdentity = result.manager->template getIdentity(variablePair.first).equals(result.manager->template getIdentity(variablePair.second)).template toAdd(); result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity); + result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first)); + result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second)); + result.rowColumnMetaVariablePairs.push_back(variablePair); result.allGlobalVariables.insert(variable.getExpressionVariable()); } @@ -395,15 +407,13 @@ namespace storm { template EdgeDestinationDd buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add const& guard, CompositionVariables const& variables) { - storm::dd::Add transitions = variables.manager->template getAddOne(); + storm::dd::Add transitions = variables.rowExpressionAdapter->translateExpression(destination.getProbability()); STORM_LOG_TRACE("Translating edge destination."); - auto t1 = std::chrono::high_resolution_clock::now(); // Iterate over all assignments (boolean and integer) and build the DD for it. std::set assignedVariables; for (auto const& assignment : destination.getAssignments()) { - std::cout << "assignment to variable " << assignment.getExpressionVariable().getName() << " expr " << assignment.getAssignedExpression() << std::endl; // Record the variable as being written. STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName()); assignedVariables.insert(assignment.getExpressionVariable()); @@ -415,35 +425,19 @@ namespace storm { // Translate the expression that is being assigned. storm::dd::Add assignedExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); - // Combine the update expression with the guard. + // Combine the assigned expression with the guard. storm::dd::Add result = assignedExpression * guard; - auto inner1 = std::chrono::high_resolution_clock::now(); // Combine the variable and the assigned expression. - storm::dd::Add tmp = result; result = result.equals(writtenVariable).template toAdd(); - auto inner2 = std::chrono::high_resolution_clock::now(); - std::cout << "inner-1 took " << std::chrono::duration_cast(inner2 - inner1).count() << "ms" << std::endl; - if (std::chrono::duration_cast(inner2 - inner1).count() > 30) { - writtenVariable.exportToDot("writtenVar.dot"); - tmp.exportToDot("result.dot"); - assignedExpression.exportToDot("assignedExpressions.dot"); - guard.exportToDot("guard.dot"); - exit(-1); - } - inner1 = std::chrono::high_resolution_clock::now(); result *= guard; - inner2 = std::chrono::high_resolution_clock::now(); - std::cout << "inner-2 took " << std::chrono::duration_cast(inner2 - inner1).count() << "ms" << std::endl; // Restrict the transitions to the range of the written variable. - result = result * variables.manager->getRange(primedMetaVariable).template toAdd(); + result = result * variables.variableToRangeMap.at(primedMetaVariable).template toAdd(); // Combine the assignment DDs. transitions *= result; } - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "assignments took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; // Compute the set of assigned global variables. std::set assignedGlobalVariables; @@ -851,7 +845,7 @@ namespace storm { */ EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { STORM_LOG_TRACE("Translating guard " << edge.getGuard()); - storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard()) * this->variables.automatonToRangeMap.at(automaton.getName()); + storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName()); STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); if (!guard.isZero()) { @@ -1107,7 +1101,6 @@ namespace storm { private: AutomatonDd composeInParallel(AutomatonDd const& automaton1, AutomatonDd const& automaton2, std::set const& synchronizingActionIndices) { - auto t1 = std::chrono::high_resolution_clock::now(); AutomatonDd result(automaton1); // Treat all actions of the first automaton. @@ -1152,9 +1145,6 @@ namespace storm { result.identity = automaton1.identity * automaton2.identity; - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "parallel composition took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; - return result; } @@ -1166,7 +1156,6 @@ namespace storm { // Cross-multiply the guards to the other fragments that write global variables and check for overlapping // parts. This finds illegal parts in which a global variable is written multiple times. - auto t1 = std::chrono::high_resolution_clock::now(); std::map> globalVariableToWritingFragment; for (auto& entry : action1.variableToWritingFragment) { entry.second &= guard2; @@ -1184,8 +1173,6 @@ namespace storm { globalVariableToWritingFragment[entry.first] = entry.second; } } - auto t2 = std::chrono::high_resolution_clock::now(); - totalTime += t2 - t1; return ActionDd(action1.guard * action2.guard, action1.transitions * action2.transitions, std::make_pair(std::min(action1.getLowestLocalNondeterminismVariable(), action2.getLowestLocalNondeterminismVariable()), std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable())), globalVariableToWritingFragment, illegalFragment); } @@ -1281,11 +1268,14 @@ namespace storm { EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) { STORM_LOG_TRACE("Translating guard " << edge.getGuard()); - storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard()) * this->variables.automatonToRangeMap.at(automaton.getName()); - STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); - if (!guard.isZero()) { - auto t1 = std::chrono::high_resolution_clock::now(); + // We keep the guard and a "ranged" version seperate, because building the destinations tends to be + // slower when the full range is applied. + storm::dd::Add guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard()); + storm::dd::Add rangedGuard = guard * this->variables.automatonToRangeMap.at(automaton.getName()); + STORM_LOG_WARN_COND(!rangedGuard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); + + if (!rangedGuard.isZero()) { // Create the DDs representing the individual updates. std::vector> destinationDds; for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { @@ -1294,11 +1284,9 @@ namespace storm { STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); } - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "building destinations took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; + // Now that we have built the destinations, we always take the full guard. + guard = rangedGuard; - t1 = std::chrono::high_resolution_clock::now(); - // Start by gathering all variables that were written in at least one destination. std::set globalVariablesInSomeDestination; @@ -1326,9 +1314,8 @@ namespace storm { // Now combine the destination DDs to the edge DD. storm::dd::Add transitions = this->variables.manager->template getAddZero(); - auto destinationDdIt = destinationDds.begin(); - for (auto destinationIt = edge.getDestinations().begin(), destinationIte = edge.getDestinations().end(); destinationIt != destinationIte; ++destinationIt, ++destinationDdIt) { - transitions += destinationDdIt->transitions * this->variables.rowExpressionAdapter->translateExpression(destinationIt->getProbability()); + for (auto const& destinationDd : destinationDds) { + transitions += destinationDd.transitions; } // Add the source location and the guard. @@ -1344,9 +1331,6 @@ namespace storm { transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); } - t2 = std::chrono::high_resolution_clock::now(); - std::cout << "rest took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; - return EdgeDd(guard, guard * transitions, globalVariablesInSomeDestination); } else { return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); @@ -1355,15 +1339,12 @@ namespace storm { ActionDd buildActionDdForActionIndex(storm::jani::Automaton const& automaton, uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) { // Translate the individual edges. - auto t1 = std::chrono::high_resolution_clock::now(); std::vector edgeDds; for (auto const& edge : automaton.getEdges()) { if (edge.getActionId() == actionIndex) { edgeDds.push_back(buildEdgeDd(automaton, edge)); } } - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "building edges for index took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; // Now combine the edges to a single action. if (!edgeDds.empty()) { @@ -1402,7 +1383,6 @@ namespace storm { allTransitions += edgeDd.transitions; // Keep track of the fragment that is writing global variables. - auto t1 = std::chrono::high_resolution_clock::now(); for (auto const& variable : edgeDd.writtenGlobalVariables) { auto it = globalVariableToWritingFragment.find(variable); if (it != globalVariableToWritingFragment.end()) { @@ -1411,29 +1391,21 @@ namespace storm { globalVariableToWritingFragment[variable] = guardBdd; } } - auto t2 = std::chrono::high_resolution_clock::now(); - totalTime += t2 - t1; } return ActionDd(allGuards.template toAdd(), allTransitions, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } - mutable std::chrono::duration totalTime = std::chrono::duration(0); - void addToVariableWritingFragmentMap(std::map>& globalVariableToWritingFragment, storm::expressions::Variable const& variable, storm::dd::Bdd const& partToAdd) const { - auto t1 = std::chrono::high_resolution_clock::now(); auto it = globalVariableToWritingFragment.find(variable); if (it != globalVariableToWritingFragment.end()) { it->second |= partToAdd; } else { globalVariableToWritingFragment.emplace(variable, partToAdd); } - auto t2 = std::chrono::high_resolution_clock::now(); - totalTime += t2 - t1; } std::map> joinVariableWritingFragmentMaps(std::map> const& globalVariableToWritingFragment1, std::map> const& globalVariableToWritingFragment2) { - auto t1 = std::chrono::high_resolution_clock::now(); std::map> result = globalVariableToWritingFragment1; for (auto const& entry : globalVariableToWritingFragment2) { @@ -1444,8 +1416,6 @@ namespace storm { result[entry.first] = entry.second; } } - auto t2 = std::chrono::high_resolution_clock::now(); - totalTime += t2 - t1; return result; } @@ -1533,12 +1503,9 @@ namespace storm { choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * currentEdge.transitions; // Keep track of the written global variables of the fragment. - auto t1 = std::chrono::high_resolution_clock::now(); for (auto const& variable : currentEdge.writtenGlobalVariables) { addToVariableWritingFragmentMap(globalVariableToWritingFragment, variable, remainingGuardChoicesIntersection && indicesEncodedWithLocalNondeterminismVariables[k].first); } - auto t2 = std::chrono::high_resolution_clock::now(); - totalTime += t2 - t1; } // Remove overlapping parts from the command guard DD @@ -1565,7 +1532,6 @@ namespace storm { } AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map const& actionIndexToLocalNondeterminismVariableOffset) { - auto t1 = std::chrono::high_resolution_clock::now(); AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); @@ -1574,16 +1540,11 @@ namespace storm { if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { continue; } - auto inner1 = std::chrono::high_resolution_clock::now(); ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex)); result.actionIndexToAction[actionIndex] = actionDd; result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable())); result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable())); - auto inner2 = std::chrono::high_resolution_clock::now(); - std::cout << "building action " << action.getName() << " took " << std::chrono::duration_cast(inner2 - inner1).count() << "ms" << std::endl; } - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "building automaton " << automatonName << " took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; return result; } @@ -1615,18 +1576,14 @@ namespace storm { // Add missing global variable identities, action and nondeterminism encodings. for (auto& action : automaton.actionIndexToAction) { - auto t1 = std::chrono::high_resolution_clock::now(); illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); - auto t2 = std::chrono::high_resolution_clock::now(); - totalTime += t2 - t1; storm::dd::Add actionEncoding = encodeAction(action.first != this->model.getSilentActionIndex() ? boost::optional(action.first) : boost::none, this->variables); storm::dd::Add missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables); storm::dd::Add extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions; result += extendedTransitions; } - std::cout << "accumulated: " << std::chrono::duration_cast(totalTime).count() << "ms" << std::endl; return ComposerResult(result, illegalFragment, numberOfUsedNondeterminismVariables); } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { // Simply add all actions, but make sure to include the missing global variable identities. @@ -1722,7 +1679,7 @@ namespace storm { initialStates &= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, automaton.getInitialLocationIndex()); } for (auto const& metaVariable : variables.rowMetaVariables) { - initialStates &= variables.manager->getRange(metaVariable); + initialStates &= variables.variableToRangeMap.at(metaVariable); } return initialStates; } diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index eafbc77e6..147843c9c 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -407,7 +407,6 @@ namespace storm { * module is modified in place and will contain the composition after a call to this method. */ void composeInParallel(typename DdPrismModelBuilder::ModuleDecisionDiagram& left, typename DdPrismModelBuilder::ModuleDecisionDiagram& right, std::set const& synchronizationActionIndices) const { - auto t1 = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Composing two modules."); // Combine the tau action. @@ -468,9 +467,6 @@ namespace storm { // Keep track of the number of nondeterminism variables used. left.numberOfUsedNondeterminismVariables = std::max(left.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables); - - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "parallel composition took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; } typename DdPrismModelBuilder::GenerationInformation& generationInfo; @@ -592,11 +588,9 @@ namespace storm { STORM_LOG_TRACE("Translating update " << update); // Iterate over all assignments (boolean and integer) and build the DD for it. - auto t1 = std::chrono::high_resolution_clock::now(); std::vector assignments = update.getAssignments(); std::set assignedVariables; for (auto const& assignment : assignments) { - std::cout << "assignment to variable " << assignment.getVariable().getName() << " expr " << assignment.getExpression() << std::endl; // Record the variable as being written. STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap->at(assignment.getVariable()).getName()); assignedVariables.insert(assignment.getVariable()); @@ -612,6 +606,7 @@ namespace storm { storm::dd::Add result = updateExpression * guard; // Combine the variable and the assigned expression. + storm::dd::Add tmp = result; result = result.equals(writtenVariable).template toAdd(); result *= guard; @@ -620,8 +615,6 @@ namespace storm { updateDd *= result; } - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "assignments took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; // Compute the set of assigned global variables. std::set assignedGlobalVariables; @@ -701,7 +694,6 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) { std::vector commandDds; - auto t1 = std::chrono::high_resolution_clock::now(); for (storm::prism::Command const& command : module.getCommands()) { // Determine whether the command is relevant for the selected action. @@ -716,8 +708,6 @@ namespace storm { // At this point, the command is known to be relevant for the action. commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command)); } - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "building commands took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; ActionDecisionDiagram result(*generationInfo.manager); if (!commandDds.empty()) { @@ -985,7 +975,6 @@ namespace storm { template typename DdPrismModelBuilder::ModuleDecisionDiagram DdPrismModelBuilder::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap) { - auto t1 = std::chrono::high_resolution_clock::now(); // Start by creating the action DD for the independent action. ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, 0, 0); uint_fast64_t numberOfUsedNondeterminismVariables = independentActionDd.numberOfUsedNondeterminismVariables; @@ -993,17 +982,12 @@ namespace storm { // Create module DD for all synchronizing actions of the module. std::map actionIndexToDdMap; for (auto const& actionIndex : module.getSynchronizingActionIndices()) { - auto inner1 = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'."); ActionDecisionDiagram tmp = createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex)); numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, tmp.numberOfUsedNondeterminismVariables); actionIndexToDdMap.emplace(actionIndex, tmp); - auto inner2 = std::chrono::high_resolution_clock::now(); - std::cout << "building action " << generationInfo.program.getActionName(actionIndex) << " took " << std::chrono::duration_cast(inner2 - inner1).count() << "ms" << std::endl; } - auto t2 = std::chrono::high_resolution_clock::now(); - std::cout << "creating module " << module.getName() << " took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()), numberOfUsedNondeterminismVariables); }