From 6b914853829233d24ddf4506618dc7248f096297 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 11:35:16 +0200 Subject: [PATCH] Removed redundant file --- src/storm/builder/DdPrismModelBuilder.cp | 1429 ---------------------- 1 file changed, 1429 deletions(-) delete mode 100644 src/storm/builder/DdPrismModelBuilder.cp diff --git a/src/storm/builder/DdPrismModelBuilder.cp b/src/storm/builder/DdPrismModelBuilder.cp deleted file mode 100644 index 26308f45b..000000000 --- a/src/storm/builder/DdPrismModelBuilder.cp +++ /dev/null @@ -1,1429 +0,0 @@ -#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 - -