From 9f70e7cb3b2249fecbc3e49ee4429cce2156d5f4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 25 Aug 2015 19:07:27 +0200 Subject: [PATCH] adapted DD-based model exploration to the new policy regarding writing to global variables Former-commit-id: 272cb04813a1cb088f03f1bdd54e89da975139d8 --- src/builder/DdPrismModelBuilder.cpp | 217 +++++++++++++++------- src/builder/DdPrismModelBuilder.h | 35 +++- src/builder/ExplicitPrismModelBuilder.cpp | 1 + 3 files changed, 185 insertions(+), 68 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 1d46e2f50..c0b540c96 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -28,7 +28,7 @@ namespace storm { template class DdPrismModelBuilder::GenerationInformation { public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() { + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); @@ -70,7 +70,10 @@ namespace storm { // DDs representing the identity for each variable. std::map> variableToIdentityMap; - + + // A set of all meta variables that correspond to global variables. + std::set allGlobalVariables; + // DDs representing the identity for each module. std::map> moduleToIdentityMap; @@ -118,6 +121,8 @@ namespace storm { storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd(); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); + + allGlobalVariables.insert(integerVariable.getExpressionVariable()); } for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); @@ -134,6 +139,7 @@ namespace storm { variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); + allGlobalVariables.insert(booleanVariable.getExpressionVariable()); } // Create meta variables for each of the modules' variables. @@ -262,7 +268,7 @@ namespace storm { }; template - storm::dd::Add DdPrismModelBuilder::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Add const& guard, storm::prism::Update const& update) { + typename DdPrismModelBuilder::UpdateDecisionDiagram DdPrismModelBuilder::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Add const& guard, storm::prism::Update const& update) { storm::dd::Add updateDd = generationInfo.manager->getAddOne(); STORM_LOG_TRACE("Translating update " << update); @@ -273,7 +279,7 @@ namespace storm { for (auto const& assignment : assignments) { // Record the variable as being written. STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap.at(assignment.getVariable()).getName()); - assignedVariables.insert(generationInfo.variableToRowMetaVariableMap.at(assignment.getVariable())); + assignedVariables.insert(assignment.getVariable()); // Translate the written variable. auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap.at(assignment.getVariable()); @@ -295,30 +301,13 @@ namespace storm { updateDd *= result; } - // This works under the assumption that global variables are only written in non-synchronzing commands, but - // is not checked here. - for (auto const& booleanVariable : generationInfo.program.getGlobalBooleanVariables()) { - storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(booleanVariable.getExpressionVariable()); - - if (assignedVariables.find(metaVariable) == assignedVariables.end()) { - STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName()); - updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable()); - } - } - - // All unused global integer variables do not change - for (auto const& integerVariable : generationInfo.program.getGlobalIntegerVariables()) { - storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(integerVariable.getExpressionVariable()); - if (assignedVariables.find(metaVariable) == assignedVariables.end()) { - STORM_LOG_TRACE("Multiplying identity of variable " << integerVariable.getName()); - updateDd *= generationInfo.variableToIdentityMap.at(integerVariable.getExpressionVariable()); - } - } + // Compute the set of assigned global variables. + std::set assignedGlobalVariables; + std::set_intersection(assignedVariables.begin(), assignedVariables.end(), generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); // All unassigned boolean variables need to keep their value. for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { - storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(booleanVariable.getExpressionVariable()); - if (assignedVariables.find(metaVariable) == assignedVariables.end()) { + if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) { STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName()); updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable()); } @@ -326,14 +315,13 @@ namespace storm { // All unassigned integer variables need to keep their value. for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { - storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(integerVariable.getExpressionVariable()); - if (assignedVariables.find(metaVariable) == assignedVariables.end()) { + if (assignedVariables.find(integerVariable.getExpressionVariable()) == assignedVariables.end()) { STORM_LOG_TRACE("Multiplying identity of variable " << integerVariable.getName()); updateDd *= generationInfo.variableToIdentityMap.at(integerVariable.getExpressionVariable()); } } - return updateDd; + return UpdateDecisionDiagram(updateDd, assignedGlobalVariables); } template @@ -343,19 +331,46 @@ namespace storm { STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); if (!guardDd.isZero()) { - storm::dd::Add commandDd = generationInfo.manager->getAddZero(); + // Create the DDs representing the individual updates. + std::vector updateResults; for (storm::prism::Update const& update : command.getUpdates()) { - storm::dd::Add updateDd = createUpdateDecisionDiagram(generationInfo, module, guardDd, update); - - STORM_LOG_WARN_COND(!updateDd.isZero(), "Update '" << update << "' does not have any effect."); + updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guardDd, update)); - storm::dd::Add probabilityDd = generationInfo.rowExpressionAdapter->translateExpression(update.getLikelihoodExpression()); - updateDd *= probabilityDd; - - commandDd += updateDd; + STORM_LOG_WARN_COND(!updateResults.back().updateDd.isZero(), "Update '" << update << "' does not have any effect."); + } + + // Start by gathering all variables that were written in at least one update. + std::set globalVariablesInSomeUpdate; + + // If the command is labeled, 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 command is not labeled, + // we can already multiply the identities of all global variables. + if (command.isLabeled()) { + std::for_each(updateResults.begin(), updateResults.end(), [&globalVariablesInSomeUpdate] (UpdateDecisionDiagram const& update) { globalVariablesInSomeUpdate.insert(update.assignedGlobalVariables.begin(), update.assignedGlobalVariables.end()); } ); + } else { + globalVariablesInSomeUpdate = generationInfo.allGlobalVariables; + } + + // Then, multiply the missing identities. + for (auto& updateResult : updateResults) { + std::set missingIdentities; + std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), updateResult.assignedGlobalVariables.begin(), updateResult.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); + + for (auto const& variable : missingIdentities) { + STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << "[" << variable.getIndex() << "] to update."); + updateResult.updateDd *= generationInfo.variableToIdentityMap.at(variable); + } + } + + // Now combine the update DDs to the command DD. + storm::dd::Add commandDd = generationInfo.manager->getAddZero(); + auto updateResultsIt = updateResults.begin(); + for (auto updateIt = command.getUpdates().begin(), updateIte = command.getUpdates().end(); updateIt != updateIte; ++updateIt, ++updateResultsIt) { + storm::dd::Add probabilityDd = generationInfo.rowExpressionAdapter->translateExpression(updateIt->getLikelihoodExpression()); + commandDd += updateResultsIt->updateDd * probabilityDd; } - return ActionDecisionDiagram(guardDd, guardDd * commandDd); + return ActionDecisionDiagram(guardDd, guardDd * commandDd, globalVariablesInSomeUpdate); } else { return ActionDecisionDiagram(*generationInfo.manager); } @@ -384,7 +399,7 @@ namespace storm { switch (generationInfo.program.getModelType()){ case storm::prism::Program::ModelType::DTMC: case storm::prism::Program::ModelType::CTMC: - result = combineCommandsToActionDTMC(generationInfo, commandDds); + result = combineCommandsToActionMarkovChain(generationInfo, commandDds); break; case storm::prism::Program::ModelType::MDP: result = combineCommandsToActionMDP(generationInfo, commandDds, nondeterminismVariableOffset); @@ -398,12 +413,60 @@ namespace storm { } template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector const& commandDds) { + std::set DdPrismModelBuilder::equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2) { + // Start by gathering all variables that were written in at least one action DD. + std::set globalVariablesInActionDd; + std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(globalVariablesInActionDd, globalVariablesInActionDd.begin())); + + std::set missingIdentitiesInAction1; + std::set_difference(globalVariablesInActionDd.begin(), globalVariablesInActionDd.end(), action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), std::inserter(missingIdentitiesInAction1, missingIdentitiesInAction1.begin())); + for (auto const& variable : missingIdentitiesInAction1) { + action1.transitionsDd *= generationInfo.variableToIdentityMap.at(variable); + } + + std::set missingIdentitiesInAction2; + std::set_difference(globalVariablesInActionDd.begin(), globalVariablesInActionDd.end(), action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), std::inserter(missingIdentitiesInAction2, missingIdentitiesInAction2.begin())); + for (auto const& variable : missingIdentitiesInAction2) { + action2.transitionsDd *= generationInfo.variableToIdentityMap.at(variable); + } + + return globalVariablesInActionDd; + } + + template + std::set DdPrismModelBuilder::equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, std::vector& actionDds) { + // Start by gathering all variables that were written in at least one action DD. + std::set globalVariablesInActionDd; + for (auto const& commandDd : actionDds) { + globalVariablesInActionDd.insert(commandDd.assignedGlobalVariables.begin(), commandDd.assignedGlobalVariables.end()); + } + + STORM_LOG_TRACE("Equalizing assigned global variables."); + + // Then multiply the transitions of each action with the missing identities. + for (auto& actionDd : actionDds) { + STORM_LOG_TRACE("Equalizing next action."); + std::set missingIdentities; + std::set_difference(globalVariablesInActionDd.begin(), globalVariablesInActionDd.end(), actionDd.assignedGlobalVariables.begin(), actionDd.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); + for (auto const& variable : missingIdentities) { + STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName() << "."); + actionDd.transitionsDd *= generationInfo.variableToIdentityMap.at(variable); + } + } + return globalVariablesInActionDd; + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMarkovChain(GenerationInformation& generationInfo, std::vector& commandDds) { storm::dd::Add allGuards = generationInfo.manager->getAddZero(); storm::dd::Add allCommands = generationInfo.manager->getAddZero(); storm::dd::Add temporary; - for (auto const& commandDd : commandDds) { + // Make all command DDs assign to the same global variables. + std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, commandDds); + + // Then combine the commands to the full action DD and multiply missing identities along the way. + for (auto& commandDd : commandDds) { // Check for overlapping guards. temporary = commandDd.guardDd * allGuards; @@ -411,10 +474,10 @@ namespace storm { STORM_LOG_WARN_COND(temporary.isZero() || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC, "Guard of a command overlaps with previous guards."); allGuards += commandDd.guardDd; - allCommands += commandDd.guardDd * commandDd.transitionsDd; + allCommands += commandDd.guardDd * commandDd.transitionsDd ; } - return ActionDecisionDiagram(allGuards, allCommands); + return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables); } template @@ -437,10 +500,13 @@ namespace storm { } template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector const& commandDds, uint_fast64_t nondeterminismVariableOffset) { + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector& commandDds, uint_fast64_t nondeterminismVariableOffset) { storm::dd::Add allGuards = generationInfo.manager->getAddZero(); storm::dd::Add allCommands = generationInfo.manager->getAddZero(); + // Make all command DDs assign to the same global variables. + std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, commandDds); + // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. storm::dd::Add sumOfGuards = generationInfo.manager->getAddZero(); for (auto const& commandDd : commandDds) { @@ -459,7 +525,7 @@ namespace storm { for (auto const& commandDd : commandDds) { allCommands += commandDd.transitionsDd; } - return ActionDecisionDiagram(sumOfGuards, allCommands); + return ActionDecisionDiagram(sumOfGuards, allCommands, assignedGlobalVariables); } else { // Calculate number of required variables to encode the nondeterminism. uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); @@ -526,27 +592,34 @@ namespace storm { sumOfGuards = sumOfGuards * !equalsNumberOfChoicesDd; } - return ActionDecisionDiagram(allGuards, allCommands, nondeterminismVariableOffset + numberOfBinaryVariables); + return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); } } template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { - return ActionDecisionDiagram(action1.guardDd * action2.guardDd, action1.transitionsDd * action2.transitionsDd, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables)); + std::set assignedGlobalVariables; + std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); + return ActionDecisionDiagram(action1.guardDd * action2.guardDd, action1.transitionsDd * action2.transitionsDd, assignedGlobalVariables, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables)); } template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2) { + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2) { storm::dd::Add action1Extended = action1.transitionsDd * identityDd2; storm::dd::Add action2Extended = action2.transitionsDd * identityDd1; + STORM_LOG_TRACE("Combining unsynchronized actions."); + + // Make both action DDs write to the same global variables. + std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, action1, action2); + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, 0); + return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, assignedGlobalVariables, 0); } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { if (action1.transitionsDd.isZero()) { - return ActionDecisionDiagram(action2.guardDd, action2Extended, action2.numberOfUsedNondeterminismVariables); + return ActionDecisionDiagram(action2.guardDd, action2Extended, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables); } else if (action2.transitionsDd.isZero()) { - return ActionDecisionDiagram(action1.guardDd, action1Extended, action1.numberOfUsedNondeterminismVariables); + return ActionDecisionDiagram(action1.guardDd, action1Extended, assignedGlobalVariables, action1.numberOfUsedNondeterminismVariables); } // Bring both choices to the same number of variables that encode the nondeterminism. @@ -570,7 +643,7 @@ namespace storm { // Add a new variable that resolves the nondeterminism between the two choices. storm::dd::Add combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).toAdd().ite(action2Extended, action1Extended); - return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1); + return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); } @@ -623,21 +696,39 @@ namespace storm { // all actions use the same amout of nondeterminism variables. uint_fast64_t numberOfUsedNondeterminismVariables = module.numberOfUsedNondeterminismVariables; + // Compute missing global variable identities in independent action. + std::set missingIdentities; + std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), module.independentAction.assignedGlobalVariables.begin(), module.independentAction.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); + storm::dd::Add identityEncoding = generationInfo.manager->getAddOne(); + for (auto const& variable : missingIdentities) { + STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to independent action."); + identityEncoding *= generationInfo.variableToIdentityMap.at(variable); + } + // Add variables to independent action DD. storm::dd::Add nondeterminismEncoding = generationInfo.manager->getAddOne(); for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).toAdd(); } - result = module.independentAction.transitionsDd * nondeterminismEncoding; + result = identityEncoding * module.independentAction.transitionsDd * nondeterminismEncoding; // Add variables to synchronized action DDs. std::map> synchronizingActionToDdMap; for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { + // Compute missing global variable identities in synchronizing actions. + missingIdentities = std::set(); + std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), synchronizingAction.second.assignedGlobalVariables.begin(), synchronizingAction.second.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin())); + identityEncoding = generationInfo.manager->getAddOne(); + for (auto const& variable : missingIdentities) { + STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to synchronizing action '" << synchronizingAction.first << "'."); + identityEncoding *= generationInfo.variableToIdentityMap.at(variable); + } + nondeterminismEncoding = generationInfo.manager->getAddOne(); for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).toAdd(); } - synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding); + synchronizingActionToDdMap.emplace(synchronizingAction.first, identityEncoding * synchronizingAction.second.transitionsDd * nondeterminismEncoding); } // Add variables for synchronization. @@ -689,33 +780,35 @@ namespace storm { } } - ModuleDecisionDiagram nextModule = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap); + ModuleDecisionDiagram currentModuleDd = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap); // Combine the non-synchronizing action. - uint_fast64_t numberOfUsedNondeterminismVariables = nextModule.numberOfUsedNondeterminismVariables; - system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, nextModule.independentAction, system.identity, nextModule.identity); + uint_fast64_t numberOfUsedNondeterminismVariables = currentModuleDd.numberOfUsedNondeterminismVariables; + system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, currentModuleDd.independentAction, system.identity, currentModuleDd.identity); numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.independentAction.numberOfUsedNondeterminismVariables); + ActionDecisionDiagram emptyAction(*generationInfo.manager); + // For all synchronizing actions that the next module does not have, we need to multiply the identity of the next module. for (auto& action : system.synchronizingActionToDecisionDiagramMap) { - if (!nextModule.hasSynchronizingAction(action.first)) { - action.second = combineUnsynchronizedActions(generationInfo, action.second, ActionDecisionDiagram(*generationInfo.manager), system.identity, nextModule.identity); + if (!currentModuleDd.hasSynchronizingAction(action.first)) { + action.second = combineUnsynchronizedActions(generationInfo, action.second, emptyAction, system.identity, currentModuleDd.identity); } } // Combine synchronizing actions. for (auto const& actionIndex : currentModule.getSynchronizingActionIndices()) { if (system.hasSynchronizingAction(actionIndex)) { - system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]); + system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], currentModuleDd.synchronizingActionToDecisionDiagramMap[actionIndex]); numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables); } else { - system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, ActionDecisionDiagram(*generationInfo.manager), nextModule.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, nextModule.identity); + system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, emptyAction, currentModuleDd.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, currentModuleDd.identity); numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables); } } // Combine identity matrices. - system.identity = system.identity * nextModule.identity; + system.identity = system.identity * currentModuleDd.identity; // Keep track of the number of nondeterminism variables used. system.numberOfUsedNondeterminismVariables = std::max(system.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables); @@ -991,7 +1084,7 @@ namespace storm { bool changed = true; uint_fast64_t iteration = 0; do { - STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states."); + STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis."); changed = false; storm::dd::Bdd tmp = reachableStates.andExists(transitionBdd, generationInfo.rowMetaVariables); tmp = tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs); diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index a815ddf06..44fb6d2f8 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -100,17 +100,34 @@ namespace storm { static std::shared_ptr> translateProgram(storm::prism::Program const& program, Options const& options = Options()); private: + // This structure can store the decision diagrams representing a particular action. + struct UpdateDecisionDiagram { + UpdateDecisionDiagram() : updateDd(), assignedGlobalVariables() { + // Intentionally left empty. + } + + UpdateDecisionDiagram(storm::dd::Add const& updateDd, std::set const& assignedGlobalVariables) : updateDd(updateDd), assignedGlobalVariables(assignedGlobalVariables) { + // Intentionally left empty. + } + + // The DD representing the update behaviour. + storm::dd::Add updateDd; + + // Keep track of the global variables that were written by this update. + std::set assignedGlobalVariables; + }; + // This structure can store the decision diagrams representing a particular action. struct ActionDecisionDiagram { ActionDecisionDiagram() : guardDd(), transitionsDd(), numberOfUsedNondeterminismVariables(0) { // Intentionally left empty. } - ActionDecisionDiagram(storm::dd::DdManager const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getAddZero()), transitionsDd(manager.getAddZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + ActionDecisionDiagram(storm::dd::DdManager const& manager, std::set const& assignedGlobalVariables = std::set(), uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getAddZero()), transitionsDd(manager.getAddZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables), assignedGlobalVariables(assignedGlobalVariables) { // Intentionally left empty. } - ActionDecisionDiagram(storm::dd::Add guardDd, storm::dd::Add transitionsDd, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(guardDd), transitionsDd(transitionsDd), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + ActionDecisionDiagram(storm::dd::Add guardDd, storm::dd::Add transitionsDd, std::set const& assignedGlobalVariables = std::set(), uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(guardDd), transitionsDd(transitionsDd), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables), assignedGlobalVariables(assignedGlobalVariables) { // Intentionally left empty. } @@ -125,6 +142,9 @@ namespace storm { // The number of variables that are used to encode the nondeterminism. uint_fast64_t numberOfUsedNondeterminismVariables; + + // Keep track of the global variables that were written by this action. + std::set assignedGlobalVariables; }; // This structure holds all decision diagrams related to a module. @@ -171,22 +191,25 @@ namespace storm { */ struct SystemResult; private: + static std::set equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2); + + static std::set equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, std::vector& actionDds); static storm::dd::Add encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value); - static storm::dd::Add createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Add const& guard, storm::prism::Update const& update); + static UpdateDecisionDiagram createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Add const& guard, storm::prism::Update const& update); static ActionDecisionDiagram createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command); static ActionDecisionDiagram createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset); - static ActionDecisionDiagram combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector const& commandDds); + static ActionDecisionDiagram combineCommandsToActionMarkovChain(GenerationInformation& generationInfo, std::vector& commandDds); - static ActionDecisionDiagram combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector const& commandDds, uint_fast64_t nondeterminismVariableOffset); + static ActionDecisionDiagram combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector& commandDds, uint_fast64_t nondeterminismVariableOffset); static ActionDecisionDiagram combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2); - static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2); + static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2); static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap); diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 89cdb7525..3b9fb23a9 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -576,6 +576,7 @@ namespace storm { storm::storage::BitVector currentState = stateQueue.front(); stateQueue.pop(); IndexType stateIndex = stateInformation.stateStorage.getValue(currentState); + STORM_LOG_TRACE("Exploring state with id " << stateIndex << "."); unpackStateIntoEvaluator(currentState, variableInformation, evaluator); // Retrieve all choices for the current state.