From ebb47aaa132c97ea4bde0e71caf3e2e9cae03966 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 18 May 2016 17:53:43 +0200 Subject: [PATCH] working on making model composition in PRISM work again Former-commit-id: 080a6d80cd6676faf1d213abbd2b3cd3f1442626 --- src/builder/DdPrismModelBuilder.cpp | 498 +++++++++++------- src/builder/DdPrismModelBuilder.h | 12 + .../prism/InterleavingParallelComposition.cpp | 2 +- .../prism/InterleavingParallelComposition.h | 4 - src/storage/prism/Program.cpp | 27 +- src/storage/prism/Program.h | 7 + .../prism/RestrictedParallelComposition.cpp | 2 +- .../prism/RestrictedParallelComposition.h | 2 - .../SynchronizingParallelComposition.cpp | 2 +- .../prism/SynchronizingParallelComposition.h | 4 - 10 files changed, 343 insertions(+), 217 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 2bb3328cd..d34ed80f3 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1,5 +1,7 @@ #include "src/builder/DdPrismModelBuilder.h" +#include + #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" @@ -9,12 +11,13 @@ #include "src/settings/SettingsManager.h" #include "src/exceptions/InvalidStateException.h" - +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/utility/prism.h" #include "src/utility/math.h" #include "src/storage/prism/Program.h" +#include "src/storage/prism/Compositions.h" #include "src/storage/dd/Add.h" #include "src/storage/dd/cudd/CuddAddIterator.h" @@ -27,107 +30,148 @@ 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(), allGlobalVariables(), moduleToIdentityMap() { - // Initializes variables and identity DDs. - createMetaVariablesAndIdentities(); - - rowExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToRowMetaVariableMap)); - columnExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToColumnMetaVariableMap)); - } - - // The program that is currently translated. - storm::prism::Program const& program; - - // The manager used to build the decision diagrams. - std::shared_ptr> manager; - - // The meta variables for the row encoding. - std::set rowMetaVariables; - std::map variableToRowMetaVariableMap; - std::shared_ptr> rowExpressionAdapter; - - // The meta variables for the column encoding. - std::set columnMetaVariables; - std::map variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; - - // All pairs of row/column meta variables. - std::vector> rowColumnMetaVariablePairs; - - // The meta variables used to encode the nondeterminism. - std::vector nondeterminismMetaVariables; - - // The meta variables used to encode the synchronization. - std::vector synchronizationMetaVariables; + public: + 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(); - // A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization - // variables). This is handy to abstract from this variable set. - std::set allNondeterminismVariables; + rowExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToRowMetaVariableMap)); + columnExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToColumnMetaVariableMap)); + } + + // The program that is currently translated. + storm::prism::Program const& program; + + // The manager used to build the decision diagrams. + std::shared_ptr> manager; + + // The meta variables for the row encoding. + std::set rowMetaVariables; + std::map variableToRowMetaVariableMap; + std::shared_ptr> rowExpressionAdapter; + + // The meta variables for the column encoding. + std::set columnMetaVariables; + std::map variableToColumnMetaVariableMap; + std::shared_ptr> columnExpressionAdapter; + + // All pairs of row/column meta variables. + std::vector> rowColumnMetaVariablePairs; + + // The meta variables used to encode the nondeterminism. + std::vector nondeterminismMetaVariables; + + // The meta variables used to encode the synchronization. + std::vector synchronizationMetaVariables; + + // A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization + // variables). This is handy to abstract from this variable set. + std::set allNondeterminismVariables; + + // As set of all variables used for encoding the synchronization. + std::set allSynchronizationMetaVariables; - // As set of all variables used for encoding the synchronization. - std::set allSynchronizationMetaVariables; + // DDs representing the identity for each variable. + std::map> variableToIdentityMap; - // DDs representing the identity for each variable. - std::map> variableToIdentityMap; + // A set of all meta variables that correspond to global variables. + std::set allGlobalVariables; - // A set of all meta variables that correspond to global variables. - std::set allGlobalVariables; + // DDs representing the identity for each module. + std::map> moduleToIdentityMap; - // DDs representing the identity for each module. - std::map> moduleToIdentityMap; + // DDs representing the valid ranges of the variables of each module. + std::map> moduleToRangeMap; + + private: + /*! + * Creates the required meta variables and variable/module identities. + */ + void createMetaVariablesAndIdentities() { + // Add synchronization variables. + for (auto const& actionIndex : program.getSynchronizingActionIndices()) { + std::pair variablePair = manager->addMetaVariable(program.getActionName(actionIndex)); + synchronizationMetaVariables.push_back(variablePair.first); + allSynchronizationMetaVariables.insert(variablePair.first); + allNondeterminismVariables.insert(variablePair.first); + } - // DDs representing the valid ranges of the variables of each module. - std::map> moduleToRangeMap; + // Add nondeterminism variables (number of modules + number of commands). + uint_fast64_t numberOfNondeterminismVariables = program.getModules().size(); + for (auto const& module : program.getModules()) { + numberOfNondeterminismVariables += module.getNumberOfCommands(); + } + for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { + std::pair variablePair = manager->addMetaVariable("nondet" + std::to_string(i)); + nondeterminismMetaVariables.push_back(variablePair.first); + allNondeterminismVariables.insert(variablePair.first); + } - private: - /*! - * Creates the required meta variables and variable/module identities. - */ - void createMetaVariablesAndIdentities() { - // Add synchronization variables. - for (auto const& actionIndex : program.getSynchronizingActionIndices()) { - std::pair variablePair = manager->addMetaVariable(program.getActionName(actionIndex)); - synchronizationMetaVariables.push_back(variablePair.first); - allSynchronizationMetaVariables.insert(variablePair.first); - allNondeterminismVariables.insert(variablePair.first); - } + // Create meta variables for global program variables. + for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) { + int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); + int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); + std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); - // Add nondeterminism variables (number of modules + number of commands). - uint_fast64_t numberOfNondeterminismVariables = program.getModules().size(); - for (auto const& module : program.getModules()) { - numberOfNondeterminismVariables += module.getNumberOfCommands(); - } - for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { - std::pair variablePair = manager->addMetaVariable("nondet" + std::to_string(i)); - nondeterminismMetaVariables.push_back(variablePair.first); - allNondeterminismVariables.insert(variablePair.first); - } + STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - // Create meta variables for global program variables. - for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) { + storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template 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()); + + STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd(); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + + rowColumnMetaVariablePairs.push_back(variablePair); + allGlobalVariables.insert(booleanVariable.getExpressionVariable()); + } + + // Create meta variables for each of the modules' variables. + for (storm::prism::Module const& module : program.getModules()) { + storm::dd::Bdd moduleIdentity = manager->getBddOne(); + storm::dd::Bdd moduleRange = manager->getBddOne(); + + for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); + STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - rowMetaVariables.insert(variablePair.first); variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); - rowColumnMetaVariablePairs.push_back(variablePair); + storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); + variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd()); + moduleIdentity &= variableIdentity; + moduleRange &= manager->getRange(variablePair.first); - allGlobalVariables.insert(integerVariable.getExpressionVariable()); + rowColumnMetaVariablePairs.push_back(variablePair); } - for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { + for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - - STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); rowMetaVariables.insert(variablePair.first); variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); @@ -135,60 +179,163 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd(); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd()); + moduleIdentity &= variableIdentity; + moduleRange &= manager->getRange(variablePair.first); rowColumnMetaVariablePairs.push_back(variablePair); - allGlobalVariables.insert(booleanVariable.getExpressionVariable()); } + moduleToIdentityMap[module.getName()] = moduleIdentity.template toAdd(); + moduleToRangeMap[module.getName()] = moduleRange.template toAdd(); + } + } + }; + + template + class ModuleComposer : public storm::prism::CompositionVisitor { + public: + ModuleComposer(typename DdPrismModelBuilder::GenerationInformation& generationInfo) : generationInfo(generationInfo) { + for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { + synchronizingActionToOffsetMap[actionIndex] = 0; + } + } + + typename DdPrismModelBuilder::ModuleDecisionDiagram compose(storm::prism::Composition const& composition) { + std::cout << "composing the system " << composition << std::endl; + return boost::any_cast::ModuleDecisionDiagram>(composition.accept(*this)); + } + + virtual boost::any visit(storm::prism::ModuleComposition const& composition) override { + STORM_LOG_TRACE("Translating module '" << composition.getModuleName() << "'."); + typename DdPrismModelBuilder::ModuleDecisionDiagram result = DdPrismModelBuilder::createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(composition.getModuleName()), synchronizingActionToOffsetMap); + + // Update the offset indices. + for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { + if (result.hasSynchronizingAction(actionIndex)) { + synchronizingActionToOffsetMap[actionIndex] = result.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables; + } + } + + return result; + } + + virtual boost::any visit(storm::prism::RenamingComposition const& composition) override { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Renaming is currently not supported in symbolic model building."); + } + + virtual boost::any visit(storm::prism::HidingComposition const& composition) override { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hiding is currently not supported in symbolic model building."); + } + + virtual boost::any visit(storm::prism::SynchronizingParallelComposition const& composition) override { + // First, we translate the subcompositions. + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this)); + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this)); + + // Then, determine the action indices on which we need to synchronize. + std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); + for (auto const& entry : leftSynchronizationActionIndices) { + std::cout << "entry 1: " << entry << std::endl; + } + std::set rightSynchronizationActionIndices = right.getSynchronizingActionIndices(); + for (auto const& entry : rightSynchronizationActionIndices) { + std::cout << "entry 2: " << entry << std::endl; + } + std::set synchronizationActionIndices; + std::set_intersection(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), std::inserter(synchronizationActionIndices, synchronizationActionIndices.begin())); + + // Finally, we compose the subcompositions to create the result. For this, we modify the left + // subcomposition in place and later return it. + composeInParallel(left, right, synchronizationActionIndices); + return left; + } + + virtual boost::any visit(storm::prism::InterleavingParallelComposition const& composition) override { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Interleaving is currently not supported in symbolic model building."); + } + + virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition) override { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Restricted parallel composition is currently not supported in symbolic model building."); + } - // Create meta variables for each of the modules' variables. - for (storm::prism::Module const& module : program.getModules()) { - storm::dd::Bdd moduleIdentity = manager->getBddOne(); - storm::dd::Bdd moduleRange = manager->getBddOne(); - - for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { - int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); - std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); - STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd()); - moduleIdentity &= variableIdentity; - moduleRange &= manager->getRange(variablePair.first); - - rowColumnMetaVariablePairs.push_back(variablePair); - } - for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { - std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + private: + /*! + * Composes the given modules while synchronizing over the provided action indices. As a result, the first + * 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) { + + std::vector actionNames; + for (auto const& actionIndex : synchronizationActionIndices) { + actionNames.push_back(generationInfo.program.getActionName(actionIndex)); + } + STORM_LOG_TRACE("Composing two modules over the actions '" << boost::join(actionNames, ", ") << "'."); + + // Combine the tau action. + uint_fast64_t numberOfUsedNondeterminismVariables = right.independentAction.numberOfUsedNondeterminismVariables; + left.independentAction = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, left.independentAction, right.independentAction, left.identity, right.identity); + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.independentAction.numberOfUsedNondeterminismVariables); - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd()); - moduleIdentity &= variableIdentity; - moduleRange &= manager->getRange(variablePair.first); + // Create an empty action for the case where one of the modules does not have a certain action. + typename DdPrismModelBuilder::ActionDecisionDiagram emptyAction(*generationInfo.manager); - rowColumnMetaVariablePairs.push_back(variablePair); + // Treat all non-tau actions of the left module. + for (auto& action : left.synchronizingActionToDecisionDiagramMap) { + // If we need to synchronize over this action index, we try to do so now. + if (synchronizationActionIndices.find(action.first) != synchronizationActionIndices.end()) { + // If we are to synchronize over an action that does not exist in the second module, the result + // is that the synchronization is the empty action. + if (right.hasSynchronizingAction(action.first)) { + action.second = emptyAction; + } else { + // Otherwise, the actions of the modules are synchronized. + action.second = DdPrismModelBuilder::combineSynchronizingActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first]); + } + } 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 (right.hasSynchronizingAction(action.first)) { + action.second = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first], left.identity, right.identity); + } else { + // If only the first module has this action, we need to use a dummy action decision diagram + // for the second module. + action.second = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, emptyAction, left.identity, right.identity); } - moduleToIdentityMap[module.getName()] = moduleIdentity.template toAdd(); - moduleToRangeMap[module.getName()] = moduleRange.template toAdd(); } + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, action.second.numberOfUsedNondeterminismVariables); } - }; + + // Treat all non-tau actions of the right module. + for (auto const& actionIndex : right.getSynchronizingActionIndices()) { + // Here, we only need to treat actions that the first module does not have, because we have handled + // this case earlier. + if (!left.hasSynchronizingAction(actionIndex)) { + if (synchronizationActionIndices.find(actionIndex) != synchronizationActionIndices.end()) { + // If we are to synchronize over this action that does not exist in the first module, the + // result is that the synchronization is the empty action. + left.synchronizingActionToDecisionDiagramMap[actionIndex] = emptyAction; + } else { + // If only the second module has this action, we need to use a dummy action decision diagram + // for the first module. + left.synchronizingActionToDecisionDiagramMap[actionIndex] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, emptyAction, right.synchronizingActionToDecisionDiagramMap[actionIndex], left.identity, right.identity); + } + } + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables); + } + + // Combine identity matrices. + left.identity = left.identity * right.identity; + + // Keep track of the number of nondeterminism variables used. + left.numberOfUsedNondeterminismVariables = std::max(left.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables); + } + typename DdPrismModelBuilder::GenerationInformation& generationInfo; + std::map synchronizingActionToOffsetMap; + }; + template DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. @@ -224,7 +371,7 @@ namespace storm { if (negatedTerminalStates) { negatedTerminalStates.reset(); } - + // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { std::set referencedRewardModels = formula.getReferencedRewardModels(); @@ -369,7 +516,7 @@ namespace storm { 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; @@ -386,7 +533,7 @@ namespace storm { 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); @@ -448,7 +595,7 @@ namespace storm { // 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) { @@ -460,7 +607,7 @@ namespace storm { for (auto const& variable : missingIdentitiesInAction2) { action2.transitionsDd *= generationInfo.variableToIdentityMap.at(variable); } - + return globalVariablesInActionDd; } @@ -473,7 +620,7 @@ namespace storm { } 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."); @@ -545,7 +692,7 @@ namespace storm { allGuards |= commandDd.guardDd.toBdd(); } uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); - + STORM_LOG_TRACE("Found " << maxChoices << " local choices."); // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. @@ -626,7 +773,7 @@ namespace storm { return ActionDecisionDiagram(allGuards.template toAdd(), allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); } } - + template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { std::set assignedGlobalVariables; @@ -638,7 +785,7 @@ namespace storm { 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. @@ -679,7 +826,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); } } - + template typename DdPrismModelBuilder::ModuleDecisionDiagram DdPrismModelBuilder::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap) { // Start by creating the action DD for the independent action. @@ -726,7 +873,7 @@ namespace storm { // 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. 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())); @@ -742,7 +889,7 @@ namespace storm { nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); } result = identityEncoding * module.independentAction.transitionsDd * nondeterminismEncoding; - + // Add variables to synchronized action DDs. std::map> synchronizingActionToDdMap; for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { @@ -773,7 +920,7 @@ namespace storm { for (auto const& synchronizingAction : synchronizingActionToDdMap) { result += synchronizingAction.second; } - + return result; } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { // Simply add all actions. @@ -789,67 +936,14 @@ namespace storm { template typename DdPrismModelBuilder::SystemResult DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { - // Create the initial offset mapping. - std::map synchronizingActionToOffsetMap; - for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { - synchronizingActionToOffsetMap[actionIndex] = 0; - } - - // Start by creating DDs for the first module. - STORM_LOG_TRACE("Translating (first) module '" << generationInfo.program.getModule(0).getName() << "'."); - ModuleDecisionDiagram system = createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(0), synchronizingActionToOffsetMap); - - // Now translate module by module and combine it with the system created thus far. - for (uint_fast64_t i = 1; i < generationInfo.program.getNumberOfModules(); ++i) { - storm::prism::Module const& currentModule = generationInfo.program.getModule(i); - STORM_LOG_TRACE("Translating module '" << currentModule.getName() << "'."); - - // Update the offset index. - for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { - if (system.hasSynchronizingAction(actionIndex)) { - synchronizingActionToOffsetMap[actionIndex] = system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables; - } - } - - ModuleDecisionDiagram currentModuleDd = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap); - - // Combine the non-synchronizing action. - 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 (!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], currentModuleDd.synchronizingActionToDecisionDiagramMap[actionIndex]); - numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables); - } else { - 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 * currentModuleDd.identity; - - // Keep track of the number of nondeterminism variables used. - system.numberOfUsedNondeterminismVariables = std::max(system.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables); - } + ModuleComposer composer(generationInfo); + ModuleDecisionDiagram system = composer.compose(generationInfo.program.specifiesSystemComposition() ? generationInfo.program.getSystemCompositionConstruct().getSystemComposition() : *generationInfo.program.getDefaultSystemComposition()); storm::dd::Add result = createSystemFromModule(generationInfo, system); - + // Create an auxiliary DD that is used later during the construction of reward models. storm::dd::Add stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables); - + // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { result = result / stateActionDd; @@ -892,7 +986,7 @@ namespace storm { // Next, build the state-action reward vector. boost::optional> stateActionRewards; if (rewardModel.hasStateActionRewards()) { - stateActionRewards = generationInfo.manager->template getAddZero(); + stateActionRewards = generationInfo.manager->template getAddZero(); for (auto const& stateActionReward : rewardModel.getStateActionRewards()) { storm::dd::Add states = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getStatePredicateExpression()); @@ -980,7 +1074,7 @@ namespace storm { return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); } - + template storm::prism::Program const& DdPrismModelBuilder::getTranslatedProgram() const { return preparedProgram.get(); @@ -1017,7 +1111,7 @@ namespace storm { // Start by initializing the structure used for storing all information needed during the model generation. // In particular, this creates the meta variables used to encode the model. GenerationInformation generationInfo(*preparedProgram); - + SystemResult system = createSystemDecisionDiagram(generationInfo); storm::dd::Add transitionMatrix = system.allTransitionsDd; @@ -1037,7 +1131,7 @@ namespace storm { std::string const& labelName = boost::get(options.terminalStates.get()); terminalExpression = preparedProgram->getLabelExpression(labelName); } - + // If the expression refers to constants of the model, we need to substitute them. terminalExpression = terminalExpression.substitute(constantsSubstitution); @@ -1078,7 +1172,7 @@ namespace storm { // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); storm::dd::Add deadlockStates = (reachableStates && !statesWithTransition).template toAdd(); - + if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. if (!storm::settings::getModule().isDontFixDeadlocksSet()) { @@ -1088,7 +1182,7 @@ namespace storm { for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) { STORM_LOG_INFO((*it).first.toPrettyString(generationInfo.rowMetaVariables) << std::endl); } - + if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { // For DTMCs, we can simply add the identity of the global module for all deadlock states. transitionMatrix += deadlockStates * globalModule.identity; @@ -1175,7 +1269,7 @@ namespace storm { changed = false; storm::dd::Bdd tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); storm::dd::Bdd newReachableStates = tmp && (!reachableStates); - + // Check whether new states were indeed discovered. if (!newReachableStates.isZero()) { changed = true; @@ -1192,7 +1286,7 @@ namespace storm { // Explicitly instantiate the symbolic model builder. template class DdPrismModelBuilder; template class DdPrismModelBuilder; - + } // namespace adapters } // namespace storm diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 3a468d6bc..44e9fdb9a 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -188,6 +188,14 @@ namespace storm { return synchronizingActionToDecisionDiagramMap.find(actionIndex) != synchronizingActionToDecisionDiagramMap.end(); } + std::set getSynchronizingActionIndices() const { + std::set result; + for (auto const& entry : synchronizingActionToDecisionDiagramMap) { + result.insert(entry.first); + } + return result; + } + // The decision diagram for the independent action. ActionDecisionDiagram independentAction; @@ -210,7 +218,11 @@ namespace storm { * Structure to store the result of the system creation phase. */ struct SystemResult; + private: + template + friend class ModuleComposer; + static std::set equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2); static std::set equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, std::vector& actionDds); diff --git a/src/storage/prism/InterleavingParallelComposition.cpp b/src/storage/prism/InterleavingParallelComposition.cpp index 311b7eede..3c5de8f8e 100644 --- a/src/storage/prism/InterleavingParallelComposition.cpp +++ b/src/storage/prism/InterleavingParallelComposition.cpp @@ -12,7 +12,7 @@ namespace storm { } void InterleavingParallelComposition::writeToStream(std::ostream& stream) const { - stream << "(" << *left << " ||| " << *right << ")"; + stream << "(" << this->getLeftSubcomposition() << " ||| " << this->getRightSubcomposition() << ")"; } } diff --git a/src/storage/prism/InterleavingParallelComposition.h b/src/storage/prism/InterleavingParallelComposition.h index 883323bbf..42c8ca771 100644 --- a/src/storage/prism/InterleavingParallelComposition.h +++ b/src/storage/prism/InterleavingParallelComposition.h @@ -13,10 +13,6 @@ namespace storm { protected: virtual void writeToStream(std::ostream& stream) const override; - - private: - std::shared_ptr left; - std::shared_ptr right; }; } } diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 3ca4675e8..57fd2a471 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -27,11 +27,21 @@ namespace storm { } bool isValid(Composition const& composition) { - return boost::any_cast(composition.accept(*this)); + bool isValid = boost::any_cast(composition.accept(*this)); + if (appearingModules.size() != program.getNumberOfModules()) { + isValid = false; + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Not every module is used in the system composition."); + } + return isValid; } virtual boost::any visit(ModuleComposition const& composition) override { - return program.hasModule(composition.getModuleName()); + bool isValid = program.hasModule(composition.getModuleName()); + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" referred to in the system composition does not exist."); + isValid = appearingModules.find(composition.getModuleName()) == appearingModules.end(); + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" is referred to more than once in the system composition."); + appearingModules.insert(composition.getModuleName()); + return isValid; } virtual boost::any visit(RenamingComposition const& composition) override { @@ -56,6 +66,7 @@ namespace storm { private: storm::prism::Program const& program; + std::set appearingModules; }; Program::Program(std::shared_ptr manager, ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::map const& actionToIndexMap, std::vector const& rewardModels, std::vector