From ca57e22abc34dff7059de3f7dfa7410718e22ee9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 7 Jun 2016 16:59:41 +0200 Subject: [PATCH] started profiling Former-commit-id: b7e034c16bbfce12c877fbc68982f9fb519688b5 --- src/builder/DdJaniModelBuilder.cpp | 262 +++++++++++++----- src/builder/DdPrismModelBuilder.cpp | 21 +- src/storage/jani/Automaton.cpp | 7 + src/storage/jani/Automaton.h | 10 +- .../builder/DdJaniModelBuilderTest.cpp | 13 +- .../coin2-2-illegalSynchronizingWrite.nm | 60 ++++ 6 files changed, 290 insertions(+), 83 deletions(-) create mode 100644 test/functional/builder/coin2-2-illegalSynchronizingWrite.nm diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 1f72ce280..92bea7da7 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -27,6 +27,7 @@ #include "src/utility/jani.h" #include "src/utility/dd.h" #include "src/utility/math.h" +#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidStateException.h" @@ -354,11 +355,12 @@ namespace storm { template struct ComposerResult { - ComposerResult(storm::dd::Add const& transitions, storm::dd::Bdd const& illegalFragment, uint64_t numberOfNondeterminismVariables = 0) : transitions(transitions), numberOfNondeterminismVariables(numberOfNondeterminismVariables) { + ComposerResult(storm::dd::Add const& transitions, storm::dd::Bdd const& illegalFragment, uint64_t numberOfNondeterminismVariables = 0) : transitions(transitions), illegalFragment(illegalFragment), numberOfNondeterminismVariables(numberOfNondeterminismVariables) { // Intentionally left empty. } storm::dd::Add transitions; + storm::dd::Bdd illegalFragment; uint64_t numberOfNondeterminismVariables; }; @@ -397,9 +399,11 @@ namespace storm { 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()); @@ -409,21 +413,37 @@ namespace storm { storm::dd::Add writtenVariable = variables.manager->template getIdentity(primedMetaVariable); // Translate the expression that is being assigned. - storm::dd::Add updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + storm::dd::Add assignedExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); // Combine the update expression with the guard. - storm::dd::Add result = updateExpression * 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(); // 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; @@ -445,7 +465,41 @@ namespace storm { } } - return EdgeDestinationDd(variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd() * transitions * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables); + transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationId()).template toAdd(); + + return EdgeDestinationDd(transitions, assignedGlobalVariables); + } + + template + storm::dd::Add encodeAction(boost::optional const& actionIndex, CompositionVariables const& variables) { + storm::dd::Add encoding = variables.manager->template getAddOne(); + + 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(); + } else { + encoding *= variables.manager->getEncoding(it->second, 0).template toAdd(); + } + } + + return encoding; + } + + template + storm::dd::Add encodeIndex(uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables const& variables) { + storm::dd::Add result = variables.manager->template getAddZero(); + + std::map metaVariableNameToValueMap; + 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(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 0); + } + } + + result.setValue(metaVariableNameToValueMap, 1); + return result; } template @@ -493,8 +547,7 @@ namespace storm { ComposerResult compose() override { AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::none)); - // FIXME: use correct illegal fragment. - return buildSystem(this->model, globalAutomaton, this->variables.manager->getBddZero(), this->variables); + return buildSystemFromAutomaton(globalAutomaton); } boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { @@ -691,7 +744,23 @@ namespace storm { } } - ComposerResult buildSystem(AutomatonDd& automatonDd) { + storm::dd::Bdd computeIllegalFragmentFromEdges(std::map> const& actionIndexToEdges) { + // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times. + storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); + for (auto const& action : actionIndexToEdges) { + for (auto const& edge : action.second) { + if (!edge.globalVariablesWrittenMultipleTimes.empty()) { + for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) { + STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised."); + illegalFragment |= edge.guard.toBdd(); + } + } + } + } + return illegalFragment; + } + + ComposerResult buildSystemFromAutomaton(AutomatonDd& automatonDd) { // If the model is an MDP, we need to encode the nondeterminism using additional variables. if (this->model.getModelType() == storm::jani::ModelType::MDP) { std::map>> actionIndexToUsedVariablesAndDd; @@ -707,16 +776,16 @@ namespace storm { storm::dd::Add result = this->variables.manager->template getAddZero(); for (auto const& element : actionIndexToUsedVariablesAndDd) { - result += element.second.second * encodeAction(element.first, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); + result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables); } - return ComposerResult(result, result.sumAbstract(this->variables.columnMetaVariables), highestNumberOfUsedNondeterminismVariables); + return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables); } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) { storm::dd::Add result = this->variables.manager->template getAddZero(); for (auto const& action : automatonDd.actionIndexToEdges) { result += combineEdgesBySummation(action.second, this->variables); } - return ComposerResult(result, result.sumAbstract(this->variables.columnMetaVariables)); + return ComposerResult(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); @@ -793,7 +862,7 @@ namespace storm { STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); } - + // Start by gathering all variables that were written in at least one update. std::set globalVariablesInSomeUpdate; @@ -837,7 +906,6 @@ namespace storm { if (edge.hasRate()) { transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); } - return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); } else { return EdgeDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero()); @@ -895,6 +963,10 @@ namespace storm { uint64_t getHighestLocalNondeterminismVariable() const { return localNondeterminismVariables.second; } + + std::pair const& getLocalNondeterminismVariables() const { + return localNondeterminismVariables; + } // A DD that represents all states that have this edge enabled. storm::dd::Add guard; @@ -936,6 +1008,11 @@ namespace storm { localNondeterminismVariables.second = newValue; } + void extendLocalNondeterminismVariables(std::pair const& localNondeterminismVariables) { + setLowestLocalNondeterminismVariable(std::min(localNondeterminismVariables.first, getLowestLocalNondeterminismVariable())); + setHighestLocalNondeterminismVariable(std::max(localNondeterminismVariables.second, getHighestLocalNondeterminismVariable())); + } + // A mapping from action indices to the action DDs. std::map actionIndexToAction; @@ -1030,6 +1107,7 @@ 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. @@ -1038,22 +1116,23 @@ namespace storm { if (synchronizingActionIndices.find(action1.first) != synchronizingActionIndices.end()) { auto action2It = automaton2.actionIndexToAction.find(action1.first); if (action2It != automaton2.actionIndexToAction.end()) { - result.actionIndexToAction[action1.first] = combineSynchronizingActions(action1.second, action2It->second); - std::cout << "synchonizing: " << result.actionIndexToAction[action1.first].transitions.getNonZeroCount() << "nnz" << std::endl; + ActionDd newAction = combineSynchronizingActions(action1.second, action2It->second); + result.actionIndexToAction[action1.first] = newAction; + result.extendLocalNondeterminismVariables(newAction.getLocalNondeterminismVariables()); } } else { // If we don't synchronize over this action, we need to construct the interleaving. - // If both modules contain the action, we need to mutually multiply the other identity. + // If both automata contain the action, we need to combine the actions in an unsynchronized way. auto action2It = automaton2.actionIndexToAction.find(action1.first); if (action2It != automaton2.actionIndexToAction.end()) { - result.actionIndexToAction[action1.first] = combineUnsynchronizedActions(action1.second, action2It->second, automaton1.identity, automaton2.identity); - std::cout << "not-synchonizing (1): index " << action1.first << ", " << result.actionIndexToAction[action1.first].transitions.getNonZeroCount() << "nnz" << std::endl; + ActionDd newAction = combineUnsynchronizedActions(action1.second, action2It->second, automaton1.identity, automaton2.identity); + result.actionIndexToAction[action1.first] = newAction; + result.extendLocalNondeterminismVariables(newAction.getLocalNondeterminismVariables()); } else { // If only the first automaton has this action, we only need to apply the identity of the // second automaton. result.actionIndexToAction[action1.first] = ActionDd(action1.second.guard, action1.second.transitions * automaton2.identity, action1.second.localNondeterminismVariables, action1.second.variableToWritingFragment, action1.second.illegalFragment); - std::cout << "not-synchonizing (2): index " << action1.first << ", " << result.actionIndexToAction[action1.first].transitions.getNonZeroCount() << "nnz" << std::endl; } } } @@ -1067,15 +1146,15 @@ namespace storm { // If only the second automaton has this action, we only need to apply the identity of the // first automaton. result.actionIndexToAction[action2.first] = ActionDd(action2.second.guard, action2.second.transitions * automaton1.identity, action2.second.localNondeterminismVariables, action2.second.variableToWritingFragment, action2.second.illegalFragment); - std::cout << "not-synchonizing (3): index " << action2.first << ", " << result.actionIndexToAction[action2.first].transitions.getNonZeroCount() << "nnz" << std::endl; } } - result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), action2.second.getLowestLocalNondeterminismVariable())); - result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), action2.second.getHighestLocalNondeterminismVariable())); } 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; } @@ -1087,6 +1166,7 @@ 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; @@ -1096,12 +1176,16 @@ namespace storm { entry.second &= guard1; auto it = globalVariableToWritingFragment.find(entry.first); if (it != globalVariableToWritingFragment.end()) { - illegalFragment |= it->second && entry.second; - it->second |= entry.second; + auto action1LocalNondeterminismVariableSet = std::set(this->variables.localNondeterminismVariables.begin() + action1.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action1.getHighestLocalNondeterminismVariable()); + auto action2LocalNondeterminismVariableSet = std::set(this->variables.localNondeterminismVariables.begin() + action2.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action2.getHighestLocalNondeterminismVariable()); + illegalFragment |= it->second.existsAbstract(action1LocalNondeterminismVariableSet) && entry.second.existsAbstract(action2LocalNondeterminismVariableSet); + it->second &= entry.second; } else { 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); } @@ -1201,6 +1285,7 @@ namespace storm { STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable."); if (!guard.isZero()) { + auto t1 = std::chrono::high_resolution_clock::now(); // Create the DDs representing the individual updates. std::vector> destinationDds; for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) { @@ -1209,24 +1294,29 @@ namespace storm { STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); } - // Start by gathering all variables that were written in at least one update. - std::set globalVariablesInSomeUpdate; + auto t2 = std::chrono::high_resolution_clock::now(); + std::cout << "building destinations took " << std::chrono::duration_cast(t2 - t1).count() << "ms" << std::endl; + + t1 = std::chrono::high_resolution_clock::now(); + + // Start by gathering all variables that were written in at least one destination. + std::set globalVariablesInSomeDestination; // 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()) { for (auto const& edgeDestinationDd : destinationDds) { - globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); + globalVariablesInSomeDestination.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); } } else { - globalVariablesInSomeUpdate = this->variables.allGlobalVariables; + globalVariablesInSomeDestination = this->variables.allGlobalVariables; } // Then, multiply the missing identities. for (auto& destinationDd : destinationDds) { std::set missingIdentities; - std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); + std::set_difference(globalVariablesInSomeDestination.begin(), globalVariablesInSomeDestination.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."); @@ -1236,15 +1326,16 @@ namespace storm { // Now combine the destination DDs to the edge DD. storm::dd::Add transitions = this->variables.manager->template getAddZero(); - for (auto const& destinationDd : destinationDds) { - transitions += destinationDd.transitions; + 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()); } // Add the source location and the guard. transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd() * guard; // If we multiply the ranges of global variables, make sure everything stays within its bounds. - if (!globalVariablesInSomeUpdate.empty()) { + if (!globalVariablesInSomeDestination.empty()) { transitions *= this->variables.globalVariableRanges; } @@ -1253,7 +1344,10 @@ namespace storm { transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate()); } - return EdgeDd(guard, transitions, globalVariablesInSomeUpdate); + 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()); } @@ -1261,12 +1355,15 @@ 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()) { @@ -1305,6 +1402,7 @@ 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()) { @@ -1313,22 +1411,29 @@ namespace storm { globalVariableToWritingFragment[variable] = guardBdd; } } + auto t2 = std::chrono::high_resolution_clock::now(); + totalTime += t2 - t1; } - std::cout << "combining edges to action yields " << allTransitions.getNonZeroCount() << " nnz" << std::endl; 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) { @@ -1339,6 +1444,8 @@ namespace storm { result[entry.first] = entry.second; } } + auto t2 = std::chrono::high_resolution_clock::now(); + totalTime += t2 - t1; return result; } @@ -1352,7 +1459,7 @@ namespace storm { addToVariableWritingFragmentMap(globalVariableToWritingFragment, variable, edge.guard.toBdd()); } } - return ActionDd(guard, transitions, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); + return ActionDd(guard, transitions, std::make_pair(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero()); } ActionDd combineEdgesToActionMdp(std::vector const& edges, uint64_t localNondeterminismVariableOffset) { @@ -1379,6 +1486,11 @@ namespace storm { storm::dd::Bdd equalsNumberOfChoicesDd; std::vector> choiceDds(maxChoices, this->variables.manager->template getAddZero()); std::vector> remainingDds(maxChoices, this->variables.manager->getBddZero()); + std::vector, storm::dd::Add>> indicesEncodedWithLocalNondeterminismVariables; + for (uint64_t j = 0; j < maxChoices; ++j) { + storm::dd::Add indexEncoding = encodeIndex(j, localNondeterminismVariableOffset, numberOfBinaryVariables, this->variables); + indicesEncodedWithLocalNondeterminismVariables.push_back(std::make_pair(indexEncoding.toBdd(), indexEncoding)); + } for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. @@ -1421,9 +1533,12 @@ 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 && encodeIndex(j, 0, numberOfBinaryVariables, this->variables).toBdd()); + 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 @@ -1438,7 +1553,7 @@ namespace storm { // 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, this->variables) * choiceDds[j]; + allEdges += indicesEncodedWithLocalNondeterminismVariables[j].second * choiceDds[j]; } // Delete currentChoices out of overlapping DD @@ -1450,17 +1565,25 @@ 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); for (auto const& action : this->model.getActions()) { uint64_t actionIndex = this->model.getActionIndex(action.getName()); + if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { + continue; + } + auto inner1 = std::chrono::high_resolution_clock::now(); ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex)); - std::cout << "action DD for action " << action.getName() << " (" << actionIndex << ") has " << actionDd.transitions.getNonZeroCount() << " nnz" << std::endl; 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; } @@ -1483,7 +1606,28 @@ namespace storm { ComposerResult buildSystemFromAutomaton(AutomatonDd& automaton) { // If the model is an MDP, we need to encode the nondeterminism using additional variables. if (this->model.getModelType() == storm::jani::ModelType::MDP) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); + storm::dd::Add result = this->variables.manager->template getAddZero(); + storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); + + // First, determine the highest number of nondeterminism variables that is used in any action and make + // all actions use the same amout of nondeterminism variables. + uint64_t numberOfUsedNondeterminismVariables = automaton.getHighestLocalNondeterminismVariable(); + + // 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. @@ -1491,14 +1635,10 @@ namespace storm { storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); for (auto& action : automaton.actionIndexToAction) { illegalFragment |= action.second.illegalFragment; - std::cout << "adding" << action.second.transitions.getNonZeroCount() << std::endl; addMissingGlobalVariableIdentities(action.second); result += action.second.transitions; } - std::cout << "result, nnz: " << result.getNonZeroCount() << ", nodes: " << result.getNodeCount() << std::endl; - result.exportToDot("trans.dot"); - return ComposerResult(result, illegalFragment, 0); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); @@ -1506,38 +1646,6 @@ namespace storm { } }; - template - storm::dd::Add encodeAction(boost::optional const& actionIndex, CompositionVariables const& variables) { - storm::dd::Add encoding = variables.manager->template getAddOne(); - - 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(); - } else { - encoding *= variables.manager->getEncoding(it->second, 0).template toAdd(); - } - } - - return encoding; - } - - template - storm::dd::Add encodeIndex(uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables const& variables) { - storm::dd::Add result = variables.manager->template getAddZero(); - - std::map metaVariableNameToValueMap; - 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(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 0); - } - } - - result.setValue(metaVariableNameToValueMap, 1); - return result; - } - template struct ModelComponents { storm::dd::Bdd reachableStates; @@ -1695,6 +1803,10 @@ namespace storm { } modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); + // Check that the reachable fragment does not overlap with the illegal fragment. + storm::dd::Bdd reachableIllegalFragment = modelComponents.reachableStates && system.illegalFragment; + STORM_LOG_THROW(reachableIllegalFragment.isZero(), storm::exceptions::WrongFormatException, "There are reachable states in the model that have synchronizing edges enabled that write the same global variable."); + // Cut transitions to reachable states. storm::dd::Add reachableStatesAdd = modelComponents.reachableStates.template toAdd(); modelComponents.transitionMatrix = system.transitions * reachableStatesAdd; diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index bd2d89aa7..eafbc77e6 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -407,6 +407,7 @@ 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. @@ -467,6 +468,9 @@ 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; @@ -588,9 +592,11 @@ 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()); @@ -614,6 +620,8 @@ 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; @@ -693,6 +701,7 @@ 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. @@ -707,7 +716,9 @@ 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()) { switch (generationInfo.program.getModelType()){ @@ -974,6 +985,7 @@ 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; @@ -981,12 +993,17 @@ 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); } diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 4815262bc..adf74855e 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -154,6 +154,9 @@ namespace storm { for (uint64_t locationIndex = edge.getSourceLocationId() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) { ++locationToStartingIndex[locationIndex]; } + + // Update the set of action indices of this automaton. + actionIndices.insert(edge.getActionId()); } std::vector& Automaton::getEdges() { @@ -192,5 +195,9 @@ namespace storm { this->initialStatesExpression = initialStatesExpression; } + bool Automaton::hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const { + return actionIndices.find(actionIndex) != actionIndices.end(); + } + } } \ No newline at end of file diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index a63292290..61e94a00f 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -225,6 +225,11 @@ namespace storm { */ void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression); + /*! + * Retrieves whether there is an edge labeled with the action with the given index in this automaton. + */ + bool hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const; + private: /// The name of the automaton. std::string name; @@ -248,8 +253,11 @@ namespace storm { /// The index of the initial location. uint64_t initialLocationIndex; - // The expression characterizing the legal initial values of the variables of the automaton. + /// The expression characterizing the legal initial values of the variables of the automaton. storm::expressions::Expression initialStatesExpression; + + /// The set of action indices that label some action in this automaton. + std::set actionIndices; }; } diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index b75ae5a84..60fe8ddf4 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -63,8 +63,6 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - std::cout << "brp starts here -----" << std::endl; - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); @@ -72,8 +70,6 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - // exit(-1); - program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); @@ -262,7 +258,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(169ul, mdp->getNumberOfStates()); EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); EXPECT_EQ(254ul, mdp->getNumberOfChoices()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); janiModel = program.toJani(true); builder = storm::builder::DdJaniModelBuilder(janiModel); @@ -322,4 +318,11 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(37ul, mdp->getNumberOfStates()); EXPECT_EQ(59ul, mdp->getNumberOfTransitions()); EXPECT_EQ(59ul, mdp->getNumberOfChoices()); +} + +TEST(DdJaniModelBuilderTest_Cudd, IllegalFragment) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm"); + storm::jani::Model janiModel = program.toJani(true); + storm::builder::DdJaniModelBuilder builder(janiModel); + EXPECT_THROW(std::shared_ptr> model = builder.translate(), storm::exceptions::WrongFormatException); } \ No newline at end of file diff --git a/test/functional/builder/coin2-2-illegalSynchronizingWrite.nm b/test/functional/builder/coin2-2-illegalSynchronizingWrite.nm new file mode 100644 index 000000000..3dd136929 --- /dev/null +++ b/test/functional/builder/coin2-2-illegalSynchronizingWrite.nm @@ -0,0 +1,60 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=2; +const int K=2; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3)&(counter'=counter); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2] endmodule + +// labels +label "finished" = pc1=3 & pc2=3 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 ; +label "all_coins_equal_1" = coin1=1 & coin2=1 ; +label "agree" = coin1=coin2 ; + +// rewards +rewards "steps" + true : 1; +endrewards +