diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 1d46e2f50..41adb09a2 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; @@ -115,9 +118,11 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd(); + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).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. @@ -184,17 +190,18 @@ namespace storm { }; template - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() { + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() { // Intentionally left empty. } template - DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()) { + DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates() { this->preserveFormula(formula); + this->setTerminalStatesFromFormula(formula); } template - DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() { + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -202,6 +209,9 @@ namespace storm { for (auto const& formula : formulas) { this->preserveFormula(*formula); } + if (formulas.size() == 1) { + this->setTerminalStatesFromFormula(*formulas.front()); + } } } @@ -234,6 +244,30 @@ namespace storm { } } + template + void DdPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + if (formula.isAtomicExpressionFormula()) { + terminalStates = formula.asAtomicExpressionFormula().getExpression(); + } else if (formula.isAtomicLabelFormula()) { + terminalStates = formula.asAtomicLabelFormula().getLabel(); + } else if (formula.isEventuallyFormula()) { + storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); + if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } else if (formula.isUntilFormula()) { + storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(right); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } + } + template void DdPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { std::map newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); @@ -262,7 +296,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 +307,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 +329,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 +343,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 +359,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 +427,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 +441,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 +502,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 +528,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 +553,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 +620,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 +671,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 +724,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 +808,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); @@ -902,6 +1023,19 @@ namespace storm { if (program.getModelType() == storm::prism::Program::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); } + + // If we were asked to treat some states as terminal states, we cut away their transitions now. + if (options.terminalStates) { + storm::expressions::Expression terminalExpression; + if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { + terminalExpression = boost::get(options.terminalStates.get()); + } else { + std::string const& labelName = boost::get(options.terminalStates.get()); + terminalExpression = preparedProgram.getLabelExpression(labelName); + } + // TODO + } + storm::dd::Bdd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd); storm::dd::Add reachableStatesAdd = reachableStates.toAdd(); transitionMatrix *= reachableStatesAdd; @@ -924,6 +1058,10 @@ namespace storm { // want to attach a lot of self-loops to the deadlock states. storm::dd::Add action = generationInfo.manager->getAddOne(); std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), [&action,&generationInfo] (storm::expressions::Variable const& metaVariable) { action *= !generationInfo.manager->getIdentity(metaVariable); } ); + // Make sure that global variables do not change along the introduced self-loops. + for (auto const& var : generationInfo.allGlobalVariables) { + action *= generationInfo.variableToIdentityMap.at(var); + } transitionMatrix += deadlockStates * globalModule.identity * action; } } else { @@ -991,7 +1129,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..20f6e76f0 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -71,6 +71,16 @@ namespace storm { */ void preserveFormula(storm::logic::Formula const& formula); + /*! + * Analyzes the given formula and sets an expression for the states states of the model that can be + * treated as terminal states. Note that this may interfere with checking properties different than the + * one provided. + * + * @param formula The formula used to (possibly) derive an expression for the terminal states of the + * model. + */ + void setTerminalStatesFromFormula(storm::logic::Formula const& formula); + // A flag that indicates whether or not all reward models are to be build. bool buildAllRewardModels; @@ -88,6 +98,10 @@ namespace storm { // An optional set of expressions for which labels need to be built. boost::optional> expressionLabels; + + // An optional expression or label that characterizes the terminal states of the model. If this is set, + // the outgoing transitions of these states are replaced with a self-loop. + boost::optional> terminalStates; }; /*! @@ -100,17 +114,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 +156,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 +205,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..f4efe7195 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -181,7 +181,7 @@ namespace storm { } else { preparedProgram = program; } - + // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. #ifdef STORM_HAVE_CARL // If the program either has undefined constants or we are building a parametric model, but the parameters @@ -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. diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index fd3f95f02..340400dde 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -55,7 +55,7 @@ namespace storm { template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); - out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl; + out << "Choices: \t" << this->getNumberOfChoices() << std::endl; this->printModelInformationFooterToStream(out); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 648b455ef..f10035c71 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -22,7 +22,6 @@ namespace storm { // An enumeration of all engines. enum class Engine { Sparse, Hybrid, Dd }; - /*! * Creates a new set of general settings that is managed by the given manager. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 18888c646..9859df52a 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -20,7 +20,7 @@ namespace storm { globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), - labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), + labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() { @@ -325,6 +325,12 @@ namespace storm { return this->labels; } + storm::expressions::Expression const& Program::getLabelExpression(std::string const& label) const { + auto const& labelIndexPair = labelToIndexMap.find(label); + STORM_LOG_THROW(labelIndexPair != labelToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve expression for unknown label '" << label << "'."); + return this->labels[labelIndexPair->second].getStatePredicateExpression(); + } + std::size_t Program::getNumberOfLabels() const { return this->getLabels().size(); } @@ -382,6 +388,9 @@ namespace storm { for (uint_fast64_t formulaIndex = 0; formulaIndex < this->getNumberOfFormulas(); ++formulaIndex) { this->formulaToIndexMap[this->getFormulas()[formulaIndex].getName()] = formulaIndex; } + for (uint_fast64_t labelIndex = 0; labelIndex < this->getNumberOfLabels(); ++labelIndex) { + this->labelToIndexMap[this->getLabels()[labelIndex].getName()] = labelIndex; + } for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) { this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex; } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index eea245684..e4f64af8a 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -345,6 +345,13 @@ namespace storm { */ std::vector