diff --git a/CMakeLists.txt b/CMakeLists.txt index bc5d1696e..3e17a4a08 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -77,6 +77,8 @@ message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}") if (STORM_DEVELOPER) set(CMAKE_BUILD_TYPE "DEBUG") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DSTORM_DEV") +else() + set(STORM_LOG_DISABLE_DEBUG ON) endif() message(STATUS "Storm - Building ${CMAKE_BUILD_TYPE} version.") diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 12e3ef19f..7cf58f2f1 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -31,6 +31,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/JaniExportSettings.h" +#include "storm/settings/modules/ResourceSettings.h" /*! * Initialize the settings manager. @@ -45,6 +46,7 @@ void initializeSettings() { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } diff --git a/src/storm/builder/DdPrismModelBuilder.cp b/src/storm/builder/DdPrismModelBuilder.cp new file mode 100644 index 000000000..26308f45b --- /dev/null +++ b/src/storm/builder/DdPrismModelBuilder.cp @@ -0,0 +1,1429 @@ +#include "storm/builder/DdPrismModelBuilder.h" + +#include + +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Ctmc.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" + +#include "storm/settings/SettingsManager.h" + +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InvalidArgumentException.h" + +#include "storm/utility/prism.h" +#include "storm/utility/math.h" +#include "storm/utility/dd.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/prism/Program.h" +#include "storm/storage/prism/Compositions.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/cudd/CuddAddIterator.h" +#include "storm/storage/dd/Bdd.h" + +#include "storm/settings/modules/CoreSettings.h" + +namespace storm { + namespace builder { + + template + class DdPrismModelBuilder::GenerationInformation { + public: + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { + // Initializes variables and identity DDs. + createMetaVariablesAndIdentities(); + } + + // 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::shared_ptr> variableToRowMetaVariableMap; + std::shared_ptr> rowExpressionAdapter; + + // The meta variables for the column encoding. + std::set columnMetaVariables; + std::shared_ptr> 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; + + // 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; + + // 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); + } + + // 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); + } + + // 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); + + 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); + + 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() << "]"); + + 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() << "]"); + + 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); + + rowColumnMetaVariablePairs.push_back(variablePair); + } + 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) { + // Intentionally left empty. + } + + typename DdPrismModelBuilder::ModuleDecisionDiagram compose(storm::prism::Composition const& composition) { + return boost::any_cast::ModuleDecisionDiagram>(composition.accept(*this, newSynchronizingActionToOffsetMap())); + } + + std::map newSynchronizingActionToOffsetMap() const { + std::map result; + for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) { + result[actionIndex] = 0; + } + return result; + } + + std::map updateSynchronizingActionToOffsetMap(typename DdPrismModelBuilder::ModuleDecisionDiagram const& sub, std::map const& oldMapping) const { + std::map result = oldMapping; + for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) { + result[action.first] = action.second.numberOfUsedNondeterminismVariables; + } + return result; + } + + virtual boost::any visit(storm::prism::ModuleComposition const& composition, boost::any const& data) override { + STORM_LOG_TRACE("Translating module '" << composition.getModuleName() << "'."); + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + + typename DdPrismModelBuilder::ModuleDecisionDiagram result = DdPrismModelBuilder::createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(composition.getModuleName()), synchronizingActionToOffsetMap); + + return result; + } + + virtual boost::any visit(storm::prism::RenamingComposition const& composition, boost::any const& data) override { + // Create the mapping from action indices to action indices. + std::map renaming; + for (auto const& namePair : composition.getActionRenaming()) { + STORM_LOG_THROW(generationInfo.program.hasAction(namePair.first), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.first << "'."); + STORM_LOG_THROW(generationInfo.program.hasAction(namePair.second), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.second << "'."); + renaming.emplace(generationInfo.program.getActionIndex(namePair.first), generationInfo.program.getActionIndex(namePair.second)); + } + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& indexPair : renaming) { + auto it = synchronizingActionToOffsetMap.find(indexPair.second); + STORM_LOG_THROW(it != synchronizingActionToOffsetMap.end(), storm::exceptions::InvalidArgumentException, "Invalid action index " << indexPair.second << "."); + newSynchronizingActionToOffsetMap[indexPair.first] = it->second; + } + + // Then, we translate the subcomposition. + typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); + + // Perform the renaming and return result. + return rename(sub, renaming); + } + + virtual boost::any visit(storm::prism::HidingComposition const& composition, boost::any const& data) override { + // Create the mapping from action indices to action indices. + std::set actionIndicesToHide; + for (auto const& action : composition.getActionsToHide()) { + STORM_LOG_THROW(generationInfo.program.hasAction(action), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << action << "'."); + actionIndicesToHide.insert(generationInfo.program.getActionIndex(action)); + } + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& index : actionIndicesToHide) { + newSynchronizingActionToOffsetMap[index] = 0; + } + + // Then, we translate the subcomposition. + typename DdPrismModelBuilder::ModuleDecisionDiagram sub = boost::any_cast::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); + + // Perform the hiding and return result. + hide(sub, actionIndicesToHide); + return sub; + } + + virtual boost::any visit(storm::prism::SynchronizingParallelComposition const& composition, boost::any const& data) override { + // First, we translate the subcompositions. + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& action : left.synchronizingActionToDecisionDiagramMap) { + newSynchronizingActionToOffsetMap[action.first] = action.second.numberOfUsedNondeterminismVariables; + } + + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); + + // Then, determine the action indices on which we need to synchronize. + std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); + std::set rightSynchronizationActionIndices = right.getSynchronizingActionIndices(); + 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. + composeInParallel(left, right, synchronizationActionIndices); + return left; + } + + virtual boost::any visit(storm::prism::InterleavingParallelComposition const& composition, boost::any const& data) override { + // First, we translate the subcompositions. + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); + + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, data)); + + // Finally, we compose the subcompositions to create the result. + composeInParallel(left, right, std::set()); + return left; + } + + virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition, boost::any const& data) override { + // Construct the synchronizing action indices from the synchronizing action names. + std::set synchronizingActionIndices; + for (auto const& action : composition.getSynchronizingActions()) { + synchronizingActionIndices.insert(generationInfo.program.getActionIndex(action)); + } + + // Then, we translate the subcompositions. + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this, data)); + + // Prepare the new offset mapping. + std::map const& synchronizingActionToOffsetMap = boost::any_cast const&>(data); + std::map newSynchronizingActionToOffsetMap = synchronizingActionToOffsetMap; + for (auto const& actionIndex : synchronizingActionIndices) { + auto it = left.synchronizingActionToDecisionDiagramMap.find(actionIndex); + if (it != left.synchronizingActionToDecisionDiagramMap.end()) { + newSynchronizingActionToOffsetMap[actionIndex] = it->second.numberOfUsedNondeterminismVariables; + } + } + + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this, newSynchronizingActionToOffsetMap)); + + std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); + bool isContainedInLeft = std::includes(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end()); + STORM_LOG_WARN_COND(isContainedInLeft, "Left subcomposition of composition '" << composition << "' does not include all actions over which to synchronize."); + + std::set rightSynchronizationActionIndices = right.getSynchronizingActionIndices(); + bool isContainedInRight = std::includes(rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end()); + STORM_LOG_WARN_COND(isContainedInRight, "Right subcomposition of composition '" << composition << "' does not include all actions over which to synchronize."); + + // Finally, we compose the subcompositions to create the result. + composeInParallel(left, right, synchronizingActionIndices); + return left; + } + + private: + /*! + * Hides the actions of the given module according to the given set. As a result, the module is modified in + * place. + */ + void hide(typename DdPrismModelBuilder::ModuleDecisionDiagram& sub, std::set const& actionIndicesToHide) const { + STORM_LOG_TRACE("Hiding actions."); + + for (auto const& actionIndex : actionIndicesToHide) { + auto it = sub.synchronizingActionToDecisionDiagramMap.find(actionIndex); + if (it != sub.synchronizingActionToDecisionDiagramMap.end()) { + sub.independentAction = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, sub.independentAction, it->second); + sub.numberOfUsedNondeterminismVariables = std::max(sub.numberOfUsedNondeterminismVariables, sub.independentAction.numberOfUsedNondeterminismVariables); + sub.synchronizingActionToDecisionDiagramMap.erase(it); + } + } + } + + /*! + * Renames the actions of the given module according to the given renaming. + */ + typename DdPrismModelBuilder::ModuleDecisionDiagram rename(typename DdPrismModelBuilder::ModuleDecisionDiagram& sub, std::map const& renaming) const { + STORM_LOG_TRACE("Renaming actions."); + std::map::ActionDecisionDiagram> actionIndexToDdMap; + + // Go through all action DDs with a synchronizing label and rename them if they appear in the renaming. + for (auto& action : sub.synchronizingActionToDecisionDiagramMap) { + auto renamingIt = renaming.find(action.first); + if (renamingIt != renaming.end()) { + // If the action is to be renamed and an action with the target index already exists, we need + // to combine the action DDs. + auto itNewActions = actionIndexToDdMap.find(renamingIt->second); + if (itNewActions != actionIndexToDdMap.end()) { + actionIndexToDdMap[renamingIt->second] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second); + + } else { + // In this case, we can simply copy the action over. + actionIndexToDdMap[renamingIt->second] = action.second; + } + } else { + // If the action is not to be renamed, we need to copy it over. However, if some other action + // was renamed to the very same action name before, we need to combine the transitions. + auto itNewActions = actionIndexToDdMap.find(action.first); + if (itNewActions != actionIndexToDdMap.end()) { + actionIndexToDdMap[action.first] = DdPrismModelBuilder::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second); + } else { + // In this case, we can simply copy the action over. + actionIndexToDdMap[action.first] = action.second; + } + } + } + + return typename DdPrismModelBuilder::ModuleDecisionDiagram(sub.independentAction, actionIndexToDdMap, sub.identity, sub.numberOfUsedNondeterminismVariables); + } + + /*! + * 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) const { + STORM_LOG_TRACE("Composing two modules."); + + // 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); + + // Create an empty action for the case where one of the modules does not have a certain action. + typename DdPrismModelBuilder::ActionDecisionDiagram emptyAction(*generationInfo.manager); + + // 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(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); + } + } + 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; + }; + + template + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + // Intentionally left empty. + } + + template + DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set()), terminalStates(), negatedTerminalStates() { + this->preserveFormula(formula); + this->setTerminalStatesFromFormula(formula); + } + + template + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + if (formulas.empty()) { + this->buildAllRewardModels = true; + this->buildAllLabels = true; + } else { + for (auto const& formula : formulas) { + this->preserveFormula(*formula); + } + if (formulas.size() == 1) { + this->setTerminalStatesFromFormula(*formulas.front()); + } + } + } + + template + void DdPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { + // If we already had terminal states, we need to erase them. + if (terminalStates) { + terminalStates.reset(); + } + 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(); + rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); + } + + // Extract all the labels used in the formula. + std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); + for (auto const& formula : atomicLabelFormulas) { + if (!labelsToBuild) { + labelsToBuild = std::set(); + } + labelsToBuild.get().insert(formula.get()->getLabel()); + } + } + + 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().getRightSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(right); + } + storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); + if (left.isAtomicExpressionFormula()) { + negatedTerminalStates = left.asAtomicExpressionFormula().getExpression(); + } else if (left.isAtomicLabelFormula()) { + negatedTerminalStates = left.asAtomicLabelFormula().getLabel(); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } + } + + template + struct DdPrismModelBuilder::SystemResult { + SystemResult(storm::dd::Add const& allTransitionsDd, DdPrismModelBuilder::ModuleDecisionDiagram const& globalModule, storm::dd::Add const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) { + // Intentionally left empty. + } + + storm::dd::Add allTransitionsDd; + typename DdPrismModelBuilder::ModuleDecisionDiagram globalModule; + storm::dd::Add stateActionDd; + }; + + template + 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->template getAddOne(); + + STORM_LOG_TRACE("Translating update " << update); + + // Iterate over all assignments (boolean and integer) and build the DD for it. + std::vector assignments = update.getAssignments(); + std::set assignedVariables; + 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(assignment.getVariable()); + + // Translate the written variable. + auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap->at(assignment.getVariable()); + storm::dd::Add writtenVariable = generationInfo.manager->template getIdentity(primedMetaVariable); + + // Translate the expression that is being assigned. + storm::dd::Add updateExpression = generationInfo.rowExpressionAdapter->translateExpression(assignment.getExpression()); + + // Combine the update expression with the guard. + storm::dd::Add result = updateExpression * guard; + + // Combine the variable and the assigned expression. + storm::dd::Add tmp = result; + result = result.equals(writtenVariable).template toAdd(); + result *= guard; + + // Restrict the transitions to the range of the written variable. + result = result * generationInfo.manager->getRange(primedMetaVariable).template toAdd(); + + updateDd *= result; + } + + // 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()) { + if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) { + STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName()); + updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable()); + } + } + + // All unassigned integer variables need to keep their value. + for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { + if (assignedVariables.find(integerVariable.getExpressionVariable()) == assignedVariables.end()) { + STORM_LOG_TRACE("Multiplying identity of variable " << integerVariable.getName()); + updateDd *= generationInfo.variableToIdentityMap.at(integerVariable.getExpressionVariable()); + } + } + + return UpdateDecisionDiagram(updateDd, assignedGlobalVariables); + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) { + STORM_LOG_TRACE("Translating guard " << command.getGuardExpression()); + storm::dd::Add guard = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; + STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); + + if (!guard.isZero()) { + // Create the DDs representing the individual updates. + std::vector updateResults; + for (storm::prism::Update const& update : command.getUpdates()) { + updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guard, update)); + + 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->template 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(guard, guard * commandDd, globalVariablesInSomeUpdate); + } else { + return ActionDecisionDiagram(*generationInfo.manager); + } + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, uint_fast64_t synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) { + std::vector commandDds; + for (storm::prism::Command const& command : module.getCommands()) { + + // Determine whether the command is relevant for the selected action. + bool relevant = (synchronizationActionIndex == 0 && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex); + + if (!relevant) { + continue; + } + + STORM_LOG_TRACE("Translating command " << command); + + // At this point, the command is known to be relevant for the action. + commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command)); + } + + ActionDecisionDiagram result(*generationInfo.manager); + if (!commandDds.empty()) { + switch (generationInfo.program.getModelType()){ + case storm::prism::Program::ModelType::DTMC: + case storm::prism::Program::ModelType::CTMC: + result = combineCommandsToActionMarkovChain(generationInfo, commandDds); + break; + case storm::prism::Program::ModelType::MDP: + result = combineCommandsToActionMDP(generationInfo, commandDds, nondeterminismVariableOffset); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type."); + } + } + + return result; + } + + template + 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->template getAddZero(); + storm::dd::Add allCommands = generationInfo.manager->template getAddZero(); + storm::dd::Add temporary; + + // 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; + + // Issue a warning if there are overlapping guards in a non-CTMC model. + 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.transitionsDd; + } + + return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables); + } + + template + storm::dd::Add DdPrismModelBuilder::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) { + storm::dd::Add result = generationInfo.manager->template getAddZero(); + + STORM_LOG_TRACE("Encoding " << value << " with " << numberOfBinaryVariables << " binary variable(s) starting from offset " << nondeterminismVariableOffset << "."); + + std::map metaVariableNameToValueMap; + for (uint_fast64_t i = nondeterminismVariableOffset; i < nondeterminismVariableOffset + numberOfBinaryVariables; ++i) { + if (value & (1ull << (numberOfBinaryVariables - i - 1))) { + metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 1); + } else { + metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 0); + } + } + + result.setValue(metaVariableNameToValueMap, ValueType(1)); + return result; + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector& commandDds, uint_fast64_t nondeterminismVariableOffset) { + storm::dd::Bdd allGuards = generationInfo.manager->getBddZero(); + storm::dd::Add allCommands = generationInfo.manager->template 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->template getAddZero(); + for (auto const& commandDd : commandDds) { + sumOfGuards += commandDd.guardDd; + 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. + if (maxChoices == 0) { + return ActionDecisionDiagram(*generationInfo.manager); + } else if (maxChoices == 1) { + // Sum up all commands. + for (auto const& commandDd : commandDds) { + allCommands += commandDd.transitionsDd; + } + 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))); + + storm::dd::Bdd equalsNumberOfChoicesDd; + std::vector> choiceDds(maxChoices, generationInfo.manager->template getAddZero()); + std::vector> remainingDds(maxChoices, generationInfo.manager->getBddZero()); + + for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { + // Determine the set of states with exactly currentChoices choices. + equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(ValueType(currentChoices))); + + // If there is no such state, continue with the next possible number of choices. + if (equalsNumberOfChoicesDd.isZero()) { + continue; + } + + // Reset the previously used intermediate storage. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + choiceDds[j] = generationInfo.manager->template getAddZero(); + remainingDds[j] = equalsNumberOfChoicesDd; + } + + for (std::size_t j = 0; j < commandDds.size(); ++j) { + // Check if command guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices + // choices such that one outgoing choice is given by the j-th command. + storm::dd::Bdd guardChoicesIntersection = commandDds[j].guardDd.toBdd() && equalsNumberOfChoicesDd; + + // If there is no such state, continue with the next command. + if (guardChoicesIntersection.isZero()) { + continue; + } + + // Split the nondeterministic choices. + for (uint_fast64_t k = 0; k < currentChoices; ++k) { + // Calculate the overlapping part of command guard and the remaining DD. + storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; + + // Check if we can add some overlapping parts to the current index. + if (!remainingGuardChoicesIntersection.isZero()) { + // Remove overlapping parts from the remaining DD. + remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; + + // Combine the overlapping part of the guard with command updates and add it to the resulting DD. + choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * commandDds[j].transitionsDd; + } + + // Remove overlapping parts from the command guard DD + guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; + + // If the guard DD has become equivalent to false, we can stop here. + if (guardChoicesIntersection.isZero()) { + break; + } + } + } + + // Add the meta variables that encode the nondeterminisim to the different choices. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + allCommands += encodeChoice(generationInfo, nondeterminismVariableOffset, numberOfBinaryVariables, j) * choiceDds[j]; + } + + // Delete currentChoices out of overlapping DD + sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); + } + + return ActionDecisionDiagram(allGuards.template toAdd(), allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); + } + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { + 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& action1, ActionDecisionDiagram& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2) { + + // First extend the action DDs by the other identities. + STORM_LOG_TRACE("Multiplying identities to combine unsynchronized actions."); + action1.transitionsDd = action1.transitionsDd * identityDd2; + action2.transitionsDd = action2.transitionsDd * identityDd1; + + // Then combine the extended action DDs. + return combineUnsynchronizedActions(generationInfo, action1, action2); + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2) { + 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, action1.transitionsDd + action2.transitionsDd, assignedGlobalVariables, 0); + } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + if (action1.transitionsDd.isZero()) { + return ActionDecisionDiagram(action2.guardDd, action2.transitionsDd, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables); + } else if (action2.transitionsDd.isZero()) { + return ActionDecisionDiagram(action1.guardDd, action1.transitionsDd, assignedGlobalVariables, action1.numberOfUsedNondeterminismVariables); + } + + // Bring both choices to the same number of variables that encode the nondeterminism. + uint_fast64_t numberOfUsedNondeterminismVariables = std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables); + if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) { + storm::dd::Add nondeterminismEncoding = generationInfo.manager->template getAddOne(); + + for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) { + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); + } + action2.transitionsDd *= nondeterminismEncoding; + } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) { + storm::dd::Add nondeterminismEncoding = generationInfo.manager->template getAddOne(); + + for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) { + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); + } + action1.transitionsDd *= nondeterminismEncoding; + } + + // Add a new variable that resolves the nondeterminism between the two choices. + storm::dd::Add combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2.transitionsDd, action1.transitionsDd); + + return ActionDecisionDiagram((action1.guardDd.toBdd() || action2.guardDd.toBdd()).template toAdd(), combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1); + } else { + 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. + ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, 0, 0); + uint_fast64_t numberOfUsedNondeterminismVariables = independentActionDd.numberOfUsedNondeterminismVariables; + + // Create module DD for all synchronizing actions of the module. + std::map actionIndexToDdMap; + for (auto const& actionIndex : module.getSynchronizingActionIndices()) { + STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'."); + ActionDecisionDiagram tmp = createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex)); + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, tmp.numberOfUsedNondeterminismVariables); + actionIndexToDdMap.emplace(actionIndex, tmp); + } + + return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()), numberOfUsedNondeterminismVariables); + } + + template + storm::dd::Add DdPrismModelBuilder::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, uint_fast64_t actionIndex) { + storm::dd::Add synchronization = generationInfo.manager->template getAddOne(); + if (actionIndex != 0) { + for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { + if ((actionIndex - 1) == i) { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1).template toAdd(); + } else { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).template toAdd(); + } + } + } else { + for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).template toAdd(); + } + } + return synchronization; + } + + template + storm::dd::Add DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) { + // If the model is an MDP, we need to encode the nondeterminism using additional variables. + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + storm::dd::Add result = generationInfo.manager->template getAddZero(); + + // 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())); + storm::dd::Add identityEncoding = generationInfo.manager->template 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->template getAddOne(); + for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { + 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) { + // 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->template 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->template getAddOne(); + for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd(); + } + synchronizingActionToDdMap.emplace(synchronizingAction.first, identityEncoding * synchronizingAction.second.transitionsDd * nondeterminismEncoding); + } + + // Add variables for synchronization. + result *= getSynchronizationDecisionDiagram(generationInfo); + + for (auto& synchronizingAction : synchronizingActionToDdMap) { + synchronizingAction.second *= getSynchronizationDecisionDiagram(generationInfo, synchronizingAction.first); + } + + // Now, we can simply add all synchronizing actions to the result. + 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, but make sure to include the missing global variable identities. + + // 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->template getAddOne(); + for (auto const& variable : missingIdentities) { + STORM_LOG_TRACE("Multiplying identity of global variable " << variable.getName() << " to independent action."); + identityEncoding *= generationInfo.variableToIdentityMap.at(variable); + } + + storm::dd::Add result = identityEncoding * module.independentAction.transitionsDd; + + 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->template 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); + } + + result += identityEncoding * synchronizingAction.second.transitionsDd; + } + return result; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); + } + } + + template + typename DdPrismModelBuilder::SystemResult DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { + 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_LOG_TRACE("Counting: " << result.getNonZeroCount() << " // " << result.getNodeCount()); + 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; + } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + // For MDPs, we need to throw away the nondeterminism variables from the generation information that + // were never used. + for (uint_fast64_t index = system.numberOfUsedNondeterminismVariables; index < generationInfo.nondeterminismMetaVariables.size(); ++index) { + generationInfo.allNondeterminismVariables.erase(generationInfo.nondeterminismMetaVariables[index]); + } + generationInfo.nondeterminismMetaVariables.resize(system.numberOfUsedNondeterminismVariables); + } + + return SystemResult(result, system, stateActionDd); + } + + template + storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { + + // Start by creating the state reward vector. + boost::optional> stateRewards; + if (rewardModel.hasStateRewards()) { + stateRewards = generationInfo.manager->template getAddZero(); + + for (auto const& stateReward : rewardModel.getStateRewards()) { + storm::dd::Add states = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getStatePredicateExpression()); + storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getRewardValueExpression()); + + // Restrict the rewards to those states that satisfy the condition. + rewards = reachableStatesAdd * states * rewards; + + // Perform some sanity checks. + STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states."); + STORM_LOG_WARN_COND(!rewards.isZero(), "The reward model does not assign any non-zero rewards."); + + // Add the rewards to the global state reward vector. + stateRewards.get() += rewards; + } + } + + // Next, build the state-action reward vector. + boost::optional> stateActionRewards; + if (rewardModel.hasStateActionRewards()) { + stateActionRewards = generationInfo.manager->template getAddZero(); + + for (auto const& stateActionReward : rewardModel.getStateActionRewards()) { + storm::dd::Add states = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getStatePredicateExpression()); + storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getRewardValueExpression()); + storm::dd::Add synchronization = generationInfo.manager->template getAddOne(); + + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + synchronization = getSynchronizationDecisionDiagram(generationInfo, stateActionReward.getActionIndex()); + } + ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction; + states *= actionDd.guardDd * reachableStatesAdd; + storm::dd::Add stateActionRewardDd = synchronization * states * rewards; + + // If we are building the state-action rewards for an MDP, we need to make sure that the encoding + // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the + // legal state-actions. + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + stateActionRewardDd *= stateActionDd; + } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { + // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action. + stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables); + } + + // Perform some sanity checks. + STORM_LOG_WARN_COND(stateActionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states."); + STORM_LOG_WARN_COND(!stateActionRewardDd.isZero(), "The reward model does not assign any non-zero rewards."); + + // Add the rewards to the global transition reward matrix. + stateActionRewards.get() += stateActionRewardDd; + } + + // Scale state-action rewards for DTMCs and CTMCs. + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { + stateActionRewards.get() /= stateActionDd; + } + } + + // Then build the transition reward matrix. + boost::optional> transitionRewards; + if (rewardModel.hasTransitionRewards()) { + transitionRewards = generationInfo.manager->template getAddZero(); + + for (auto const& transitionReward : rewardModel.getTransitionRewards()) { + storm::dd::Add sourceStates = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getSourceStatePredicateExpression()); + storm::dd::Add targetStates = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getTargetStatePredicateExpression()); + storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getRewardValueExpression()); + + storm::dd::Add synchronization = generationInfo.manager->template getAddOne(); + + storm::dd::Add transitions; + if (transitionReward.isLabeled()) { + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + synchronization = getSynchronizationDecisionDiagram(generationInfo, transitionReward.getActionIndex()); + } + transitions = globalModule.synchronizingActionToDecisionDiagramMap.at(transitionReward.getActionIndex()).transitionsDd; + } else { + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + synchronization = getSynchronizationDecisionDiagram(generationInfo); + } + transitions = globalModule.independentAction.transitionsDd; + } + + storm::dd::Add transitionRewardDd = synchronization * sourceStates * targetStates * rewards; + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { + // For DTMCs we need to keep the weighting for the scaling that follows. + transitionRewardDd = transitions * transitionRewardDd; + } else { + // For all other model types, we do not scale the rewards. + transitionRewardDd = transitions.notZero().template toAdd() * transitionRewardDd; + } + + // Perform some sanity checks. + STORM_LOG_WARN_COND(transitionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states."); + STORM_LOG_WARN_COND(!transitionRewardDd.isZero(), "The reward model does not assign any non-zero rewards."); + + // Add the rewards to the global transition reward matrix. + transitionRewards.get() += transitionRewardDd; + } + + // Scale transition rewards for DTMCs. + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { + transitionRewards.get() /= stateActionDd; + } + } + + return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); + } + + template + std::shared_ptr> DdPrismModelBuilder::build(storm::prism::Program const& program, Options const& options) { + if (program.hasUndefinedConstants()) { + std::vector> undefinedConstants = program.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); + } + + STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl); + + // 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(program); + + SystemResult system = createSystemDecisionDiagram(generationInfo); + storm::dd::Add transitionMatrix = system.allTransitionsDd; + + ModuleDecisionDiagram const& globalModule = system.globalModule; + storm::dd::Add stateActionDd = system.stateActionDd; + + // If we were asked to treat some states as terminal states, we cut away their transitions now. + storm::dd::Bdd terminalStatesBdd = generationInfo.manager->getBddZero(); + if (options.terminalStates || options.negatedTerminalStates) { + std::map constantsSubstitution = program.getConstantsSubstitution(); + + 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()); + if (program.hasLabel(labelName)) { + terminalExpression = program.getLabelExpression(labelName); + } else { + STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + } + } + + if (terminalExpression.isInitialized()) { + // If the expression refers to constants of the model, we need to substitute them. + terminalExpression = terminalExpression.substitute(constantsSubstitution); + + STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); + terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); + } + } + if (options.negatedTerminalStates) { + storm::expressions::Expression negatedTerminalExpression; + if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) { + negatedTerminalExpression = boost::get(options.negatedTerminalStates.get()); + } else { + std::string const& labelName = boost::get(options.negatedTerminalStates.get()); + if (program.hasLabel(labelName)) { + negatedTerminalExpression = program.getLabelExpression(labelName); + } else { + STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + } + } + + if (negatedTerminalExpression.isInitialized()) { + // If the expression refers to constants of the model, we need to substitute them. + negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution); + + STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); + terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); + } + } + + transitionMatrix *= (!terminalStatesBdd).template toAdd(); + } + + std::cout << "trans matrix has size " << transitionMatrix.getNodeCount() << std::endl; + + // Cut the transitions and rewards to the reachable fragment of the state space. + storm::dd::Bdd initialStates = createInitialStatesDecisionDiagram(generationInfo); + + storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); + if (program.getModelType() == storm::prism::Program::ModelType::MDP) { + transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); + } + + storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionMatrixBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); + storm::dd::Add reachableStatesAdd = reachableStates.template toAdd(); + transitionMatrix *= reachableStatesAdd; + stateActionDd *= reachableStatesAdd; + + // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. + storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); + storm::dd::Bdd deadlockStates = reachableStates && !statesWithTransition; + + // If there are deadlocks, either fix them or raise an error. + if (!deadlockStates.isZero()) { + // If we need to fix deadlocks, we do so now. + if (!storm::settings::getModule().isDontFixDeadlocksSet()) { + STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); + + storm::dd::Add deadlockStatesAdd = deadlockStates.template toAdd(); + uint_fast64_t count = 0; + for (auto it = deadlockStatesAdd.begin(), ite = deadlockStatesAdd.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 || program.getModelType() == storm::prism::Program::ModelType::CTMC) { + storm::dd::Add identity = globalModule.identity; + + // Make sure that global variables do not change along the introduced self-loops. + for (auto const& var : generationInfo.allGlobalVariables) { + identity *= generationInfo.variableToIdentityMap.at(var); + } + + // For DTMCs, we can simply add the identity of the global module for all deadlock states. + transitionMatrix += deadlockStatesAdd * identity; + } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { + // For MDPs, however, we need to select an action associated with the self-loop, if we do not + // want to attach a lot of self-loops to the deadlock states. + storm::dd::Add action = generationInfo.manager->template getAddOne(); + for (auto const& metaVariable : generationInfo.allNondeterminismVariables) { + action *= generationInfo.manager->template 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 += deadlockStatesAdd * globalModule.identity * action; + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); + } + } + + // Reduce the deadlock states by the states that we did simply not explore. + deadlockStates = deadlockStates && !terminalStatesBdd; + + // Now build the reward models. + std::vector> selectedRewardModels; + + // First, we make sure that all selected reward models actually exist. + for (auto const& rewardModelName : options.rewardModelsToBuild) { + STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); + } + + for (auto const& rewardModel : program.getRewardModels()) { + if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) { + std::cout << "build all? " << buildAllRewardModels << std::endl; + selectedRewardModels.push_back(rewardModel); + } + } + // If no reward model was selected until now and a referenced reward model appears to be unique, we build + // the only existing reward model (given that no explicit name was given for the referenced reward model). + if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { + selectedRewardModels.push_back(program.getRewardModel(0)); + } + + std::unordered_map> rewardModels; + for (auto const& rewardModel : selectedRewardModels) { + rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, stateActionDd)); + } + + // Build the labels that can be accessed as a shortcut. + std::map labelToExpressionMapping; + for (auto const& label : program.getLabels()) { + labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression()); + } + + if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { + return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { + return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { + return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); + } + } + + template + storm::dd::Bdd DdPrismModelBuilder::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) { + storm::dd::Bdd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialStatesExpression()).toBdd(); + + for (auto const& metaVariable : generationInfo.rowMetaVariables) { + initialStates &= generationInfo.manager->getRange(metaVariable); + } + + return initialStates; + } + + // Explicitly instantiate the symbolic model builder. + template class DdPrismModelBuilder; + template class DdPrismModelBuilder; + + } // namespace adapters +} // namespace storm + + diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 988335cbb..0075f91f5 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -470,7 +470,7 @@ namespace storm { }; template - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. } @@ -482,16 +482,11 @@ namespace storm { template DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { - if (formulas.empty()) { - this->buildAllRewardModels = true; - this->buildAllLabels = true; - } else { - for (auto const& formula : formulas) { - this->preserveFormula(*formula); - } - if (formulas.size() == 1) { - this->setTerminalStatesFromFormula(*formulas.front()); - } + for (auto const& formula : formulas) { + this->preserveFormula(*formula); + } + if (formulas.size() == 1) { + this->setTerminalStatesFromFormula(*formulas.front()); } } @@ -553,13 +548,13 @@ namespace storm { template struct DdPrismModelBuilder::SystemResult { - SystemResult(storm::dd::Add const& allTransitionsDd, DdPrismModelBuilder::ModuleDecisionDiagram const& globalModule, storm::dd::Add const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) { + SystemResult(storm::dd::Add const& allTransitionsDd, DdPrismModelBuilder::ModuleDecisionDiagram const& globalModule, boost::optional> const& stateActionDd) : allTransitionsDd(allTransitionsDd), globalModule(globalModule), stateActionDd(stateActionDd) { // Intentionally left empty. } storm::dd::Add allTransitionsDd; typename DdPrismModelBuilder::ModuleDecisionDiagram globalModule; - storm::dd::Add stateActionDd; + boost::optional> stateActionDd; }; template @@ -1087,13 +1082,14 @@ namespace storm { 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); + boost::optional> stateActionDd; // 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; + stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables); + result = result / stateActionDd.get(); } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { // For MDPs, we need to throw away the nondeterminism variables from the generation information that // were never used. @@ -1107,7 +1103,7 @@ namespace storm { } template - storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { + storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& transitionMatrix, boost::optional> stateActionDd) { // Start by creating the state reward vector. boost::optional> stateRewards; @@ -1145,13 +1141,15 @@ namespace storm { } ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction; states *= actionDd.guardDd * reachableStatesAdd; - storm::dd::Add stateActionRewardDd = synchronization * states * rewards; + storm::dd::Add stateActionRewardDd = synchronization * (reachableStatesAdd * states * rewards); // If we are building the state-action rewards for an MDP, we need to make sure that the encoding // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the // legal state-actions. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - stateActionRewardDd *= stateActionDd; + // FIXME: get synchronization encoding differently. + // stateActionRewardDd *= stateActionDd; + stateActionRewardDd *= transitionMatrix.notZero().existsAbstract(generationInfo.columnMetaVariables).template toAdd(); } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action. stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables); @@ -1167,7 +1165,7 @@ namespace storm { // Scale state-action rewards for DTMCs and CTMCs. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - stateActionRewards.get() /= stateActionDd; + // stateActionRewards.get() /= stateActionDd; } } @@ -1215,7 +1213,7 @@ namespace storm { // Scale transition rewards for DTMCs. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - transitionRewards.get() /= stateActionDd; + transitionRewards.get() /= stateActionDd.get(); } } @@ -1240,7 +1238,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); } - STORM_LOG_DEBUG("Building representation of program:" << std::endl << program << std::endl); + STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl); // 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. @@ -1250,7 +1248,6 @@ namespace storm { storm::dd::Add transitionMatrix = system.allTransitionsDd; ModuleDecisionDiagram const& globalModule = system.globalModule; - storm::dd::Add stateActionDd = system.stateActionDd; // If we were asked to treat some states as terminal states, we cut away their transitions now. storm::dd::Bdd terminalStatesBdd = generationInfo.manager->getBddZero(); @@ -1314,7 +1311,9 @@ namespace storm { storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionMatrixBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); storm::dd::Add reachableStatesAdd = reachableStates.template toAdd(); transitionMatrix *= reachableStatesAdd; - stateActionDd *= reachableStatesAdd; + if (system.stateActionDd) { + system.stateActionDd.get() *= reachableStatesAdd; + } // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); @@ -1384,7 +1383,7 @@ namespace storm { std::unordered_map> rewardModels; for (auto const& rewardModel : selectedRewardModels) { - rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, stateActionDd)); + rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, reachableStatesAdd, transitionMatrix, system.stateActionDd)); } // Build the labels that can be accessed as a shortcut. diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index 5b1db357f..701a2ecdc 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -230,7 +230,7 @@ namespace storm { static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); + static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& transitionMatrix, boost::optional> stateActionDd); static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo); diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 93039e480..1f09fa687 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -550,7 +550,11 @@ namespace storm { // Next, we split the matrix into one for each group. Note that this only works if the group variables are // at the very top. - std::vector> groups = internalAdd.splitIntoGroups(ddGroupVariableIndices); + std::vector> internalAddGroups = internalAdd.splitIntoGroups(ddGroupVariableIndices); + std::vector> groups; + for (auto const& internalAdd : internalAddGroups) { + groups.push_back(Add(this->getDdManager(), internalAdd, rowAndColumnMetaVariables)); + } // Create the actual storage for the non-zero entries. std::vector> columnsAndValues(this->getNonZeroCount()); @@ -561,17 +565,20 @@ namespace storm { std::vector> statesWithGroupEnabled(groups.size()); InternalAdd stateToRowGroupCount = this->getDdManager().template getAddZero(); for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; + auto const& group = groups[i]; + auto groupNotZero = group.notZero(); - dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false); + std::vector tmpRowIndications = groupNotZero.template toAdd().sumAbstract(columnMetaVariables).toVector(rowOdd); + for (uint64_t offset = 0; offset < tmpRowIndications.size(); ++offset) { + rowIndications[rowGroupIndices[offset]] += tmpRowIndications[offset]; + } - statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).template toAdd(); - stateToRowGroupCount += statesWithGroupEnabled[i]; + statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd(); statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); } // Since we modified the rowGroupIndices, we need to restore the correct values. - stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); + stateToNumberOfChoices.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. tmp = 0; @@ -585,15 +592,15 @@ namespace storm { // Now actually fill the entry vector. for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; + auto const& group = groups[i]; - dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true); + group.internalAdd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true); statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); } // Since we modified the rowGroupIndices, we need to restore the correct values. - stateToRowGroupCount.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); + stateToNumberOfChoices.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::minus()); // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { @@ -674,7 +681,11 @@ namespace storm { std::vector explicitVector(rowGroupIndices.back()); // Next, we split the matrix into one for each group. Note that this only works if the group variables are at the very top. - std::vector, InternalAdd>> groups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices); + std::vector, InternalAdd>> internalAddGroups = internalAdd.splitIntoGroups(vector, ddGroupVariableIndices); + std::vector, Add>> groups; + for (auto const& internalAdd : internalAddGroups) { + groups.push_back(std::make_pair(Add(this->getDdManager(), internalAdd.first, rowAndColumnMetaVariables), Add(this->getDdManager(), internalAdd.second, rowMetaVariables))); + } // Create the actual storage for the non-zero entries. std::vector> columnsAndValues(this->getNonZeroCount()); @@ -685,12 +696,18 @@ namespace storm { std::vector> statesWithGroupEnabled(groups.size()); InternalAdd stateToRowGroupCount = this->getDdManager().template getAddZero(); for (uint_fast64_t i = 0; i < groups.size(); ++i) { - std::pair, InternalAdd> const& ddPair = groups[i]; - - ddPair.first.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false); - ddPair.second.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus()); + std::pair, Add> const& ddPair = groups[i]; + Bdd matrixDdNotZero = ddPair.first.notZero(); + Bdd vectorDdNotZero = ddPair.second.notZero(); + + std::vector tmpRowIndications = matrixDdNotZero.template toAdd().sumAbstract(columnMetaVariables).toVector(rowOdd); + for (uint64_t offset = 0; offset < tmpRowIndications.size(); ++offset) { + rowIndications[rowGroupIndices[offset]] += tmpRowIndications[offset]; + } + + ddPair.second.internalAdd.composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, explicitVector, std::plus()); - statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).template toAdd(); + statesWithGroupEnabled[i] = (matrixDdNotZero.existsAbstract(columnMetaVariables) || vectorDdNotZero).template toAdd(); stateToRowGroupCount += statesWithGroupEnabled[i]; statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); } @@ -712,8 +729,7 @@ namespace storm { for (uint_fast64_t i = 0; i < groups.size(); ++i) { auto const& dd = groups[i].first; - dd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true); - + dd.internalAdd.toMatrixComponents(rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, true); statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); } diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index 84a0db845..1341a8e3b 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -35,7 +35,7 @@ namespace storm { Bdd& operator=(Bdd const& other) = default; Bdd(Bdd&& other) = default; Bdd& operator=(Bdd&& other) = default; - + /*! * Constructs a BDD representation of all encodings that are in the requested relation with the given value. * diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index 3cd2539dd..9cca07b06 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -111,8 +111,17 @@ namespace storm { template Bdd DdManager::getCube(storm::expressions::Variable const& variable) const { - storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - return metaVariable.getCube(); + return getCube({variable}); + } + + template + Bdd DdManager::getCube(std::set const& variables) const { + Bdd result = this->getBddOne(); + for (auto const& variable : variables) { + storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); + result &= metaVariable.getCube(); + } + return result; } template diff --git a/src/storm/storage/dd/DdManager.h b/src/storm/storage/dd/DdManager.h index 0ab1ed1c9..7baffbcb8 100644 --- a/src/storm/storage/dd/DdManager.h +++ b/src/storm/storage/dd/DdManager.h @@ -125,7 +125,15 @@ namespace storm { * @return The cube of the meta variable. */ Bdd getCube(storm::expressions::Variable const& variable) const; - + + /*! + * Retrieves a BDD that is the cube of the variables representing the given meta variables. + * + * @param variables The expression variables associated with the meta variables. + * @return The cube of the meta variables. + */ + Bdd getCube(std::set const& variables) const; + /*! * Adds an integer meta variable with the given range. * diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 4cf197970..872ef4856 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -17,7 +17,7 @@ namespace storm { InternalAdd::InternalAdd(InternalDdManager const* ddManager, cudd::ADD cuddAdd) : ddManager(ddManager), cuddAdd(cuddAdd) { // Intentionally left empty. } - + template bool InternalAdd::operator==(InternalAdd const& other) const { return this->getCuddAdd() == other.getCuddAdd(); diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 5e5043246..08eb74bb1 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -14,6 +14,11 @@ namespace storm { namespace dd { + template + InternalAdd::InternalAdd() : ddManager(nullptr), sylvanMtbdd() { + // Intentionally left empty. + } + template InternalAdd::InternalAdd(InternalDdManager const* ddManager, sylvan::Mtbdd const& sylvanMtbdd) : ddManager(ddManager), sylvanMtbdd(sylvanMtbdd) { // Intentionally left empty. diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 17fd8eca2..d91374903 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -55,12 +55,12 @@ namespace storm { InternalAdd(InternalDdManager const* ddManager, sylvan::Mtbdd const& sylvanMtbdd); // Instantiate all copy/move constructors/assignments with the default implementation. - InternalAdd() = default; + InternalAdd(); InternalAdd(InternalAdd const& other) = default; InternalAdd& operator=(InternalAdd const& other) = default; InternalAdd(InternalAdd&& other) = default; InternalAdd& operator=(InternalAdd&& other) = default; - + /*! * Retrieves whether the two DDs represent the same function. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 7097ac999..5c297be99 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -18,6 +18,10 @@ namespace storm { namespace dd { + InternalBdd::InternalBdd() : ddManager(nullptr), sylvanBdd() { + // Intentionally left empty. + } + InternalBdd::InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) { // Intentionally left empty. } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index 930966c01..fbeb49c4b 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -35,7 +35,7 @@ namespace storm { InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd); // Instantiate all copy/move constructors/assignments with the default implementation. - InternalBdd() = default; + InternalBdd(); InternalBdd(InternalBdd const& other) = default; InternalBdd& operator=(InternalBdd const& other) = default; InternalBdd(InternalBdd&& other) = default; diff --git a/src/test/storage/JaniModelTest.cpp b/src/test/storage/JaniModelTest.cpp index 764bfe5bc..7c7f393b3 100644 --- a/src/test/storage/JaniModelTest.cpp +++ b/src/test/storage/JaniModelTest.cpp @@ -7,7 +7,7 @@ #include "storm/storage/jani/Model.h" #ifdef STORM_HAVE_MSAT -TEST(JaniModelTest, FlattenModules) { +TEST(JaniModelTest, FlattenComposition) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); storm::jani::Model janiModel = program.toJani(); @@ -19,7 +19,7 @@ TEST(JaniModelTest, FlattenModules) { EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) { +TEST(JaniModelTest, FlattenComposition_Wlan_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm")); storm::jani::Model janiModel = program.toJani(); @@ -31,7 +31,7 @@ TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) { EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Csma_Mathsat) { +TEST(JaniModelTest, FlattenComposition_Csma_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm")); storm::jani::Model janiModel = program.toJani(); @@ -43,7 +43,7 @@ TEST(JaniModelTest, FlattenModules_Csma_Mathsat) { EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) { +TEST(JaniModelTest, FlattenComposition_Firewire_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm")); storm::jani::Model janiModel = program.toJani(); @@ -55,7 +55,7 @@ TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) { EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Coin_Mathsat) { +TEST(JaniModelTest, FlattenComposition_Coin_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm")); storm::jani::Model janiModel = program.toJani(); @@ -67,7 +67,7 @@ TEST(JaniModelTest, FlattenModules_Coin_Mathsat) { EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Dice_Mathsat) { +TEST(JaniModelTest, FlattenComposition_Dice_Mathsat) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm")); storm::jani::Model janiModel = program.toJani(); @@ -81,7 +81,7 @@ TEST(JaniModelTest, FlattenModules_Dice_Mathsat) { #endif #ifdef STORM_HAVE_Z3 -TEST(JaniModelTest, FlattenModules_Leader_Z3) { +TEST(JaniModelTest, FlattenComposition_Leader_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); storm::jani::Model janiModel = program.toJani(); @@ -93,7 +93,7 @@ TEST(JaniModelTest, FlattenModules_Leader_Z3) { EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Wlan_Z3) { +TEST(JaniModelTest, FlattenComposition_Wlan_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm")); storm::jani::Model janiModel = program.toJani(); @@ -105,7 +105,7 @@ TEST(JaniModelTest, FlattenModules_Wlan_Z3) { EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Csma_Z3) { +TEST(JaniModelTest, FlattenComposition_Csma_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm")); storm::jani::Model janiModel = program.toJani(); @@ -117,7 +117,7 @@ TEST(JaniModelTest, FlattenModules_Csma_Z3) { EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Firewire_Z3) { +TEST(JaniModelTest, FlattenComposition_Firewire_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire.nm")); storm::jani::Model janiModel = program.toJani(); @@ -129,7 +129,7 @@ TEST(JaniModelTest, FlattenModules_Firewire_Z3) { EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Coin_Z3) { +TEST(JaniModelTest, FlattenComposition_Coin_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2.nm")); storm::jani::Model janiModel = program.toJani(); @@ -141,7 +141,7 @@ TEST(JaniModelTest, FlattenModules_Coin_Z3) { EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges()); } -TEST(JaniModelTest, FlattenModules_Dice_Z3) { +TEST(JaniModelTest, FlattenComposition_Dice_Z3) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm")); storm::jani::Model janiModel = program.toJani();