diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 6085d5271..592df613d 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -516,7 +516,7 @@ namespace storm { } template - std::pair, storm::dd::Dd> DdPrismModelBuilder::createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, storm::dd::Dd transitionMatrix) { + std::pair, storm::dd::Dd> DdPrismModelBuilder::createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Dd const& fullTransitionMatrix) { // Start by creating the state reward vector. storm::dd::Dd stateRewards = generationInfo.manager->getZero(); for (auto const& stateReward : rewardModel.getStateRewards()) { @@ -539,19 +539,22 @@ namespace storm { for (auto const& transitionReward : rewardModel.getTransitionRewards()) { storm::dd::Dd states = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getStatePredicateExpression()); storm::dd::Dd rewards = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getRewardValueExpression()); - + storm::dd::Dd synchronization; + storm::dd::Dd transitions; if (transitionReward.isLabeled()) { - synchronization = getSynchronizationDecisionDiagram(generationInfo); - } else { synchronization = getSynchronizationDecisionDiagram(generationInfo, transitionReward.getActionIndex()); + transitions = globalModule.synchronizingActionToDecisionDiagramMap.at(transitionReward.getActionIndex()).transitionsDd; + } else { + synchronization = getSynchronizationDecisionDiagram(generationInfo); + transitions = globalModule.independentAction.transitionsDd; } storm::dd::Dd transitionRewardDd = synchronization * states * rewards; if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - transitionRewardDd += transitionMatrix.notZero() * transitionRewardDd; + transitionRewardDd += transitions.notZero() * transitionRewardDd; } else { - transitionRewardDd += transitionMatrix * transitionRewardDd; + transitionRewardDd += transitions * transitionRewardDd; } // Perform some sanity checks. @@ -562,14 +565,11 @@ namespace storm { transitionRewards += transitionRewardDd; } - // Scale transition rewards for DTMCs + // Scale transition rewards for DTMCs. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { - for (uint_fast64_t i = 0; i < generationInfo.program.getRewardModels().size(); ++i){ - // Divide transition rewards through transition matrix - transitionRewardsDds[i] = transitionRewardsDds[i] / systemDds.independentActionDd.commandsDd; - } + transitionRewards /= fullTransitionMatrix; } - + return std::make_pair(stateRewards, transitionRewards); } @@ -608,12 +608,33 @@ namespace storm { auto totalTimeStart = std::chrono::high_resolution_clock::now(); std::pair, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); - auto totalTimeEnd = std::chrono::high_resolution_clock::now(); - std::cout << "building matrix took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; - storm::dd::Dd transitionMatrix = transitionMatrixModulePair.first; ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second; + // Finally, we build the DDs for a reward structure, if requested. It is important to do this now, because + // we still have the uncut transition matrix, which is needed for the reward computation. This is because + // the reward computation might divide by the transition probabilities, which must therefore never be 0. + // However, cutting it to the reachable fragment, there might be zero probability transitions. + boost::optional, storm::dd::Dd>> stateAndTransitionRewards; + if (options.buildRewards) { + // If a specific reward model was selected or one with the empty name exists, select it. + storm::prism::RewardModel rewardModel = storm::prism::RewardModel(); + if (options.rewardModelName) { + rewardModel = preparedProgram.getRewardModel(options.rewardModelName.get()); + } else if (preparedProgram.hasRewardModel("")) { + rewardModel = preparedProgram.getRewardModel(""); + } else if (preparedProgram.hasRewardModel()) { + // Otherwise, we select the first one. + rewardModel = preparedProgram.getRewardModel(0); + } + + STORM_LOG_TRACE("Building reward structure."); + stateAndTransitionRewards = createRewardDecisionDiagrams(generationInfo, rewardModel, globalModule, transitionMatrix); + } + + auto totalTimeEnd = std::chrono::high_resolution_clock::now(); + std::cout << "building matrices and vectors took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; + // Cut the transition matrix to the reachable fragment of the state space. totalTimeStart = std::chrono::high_resolution_clock::now(); storm::dd::Dd reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix); @@ -655,24 +676,6 @@ namespace storm { std::cout << reachableStates.getNonZeroCount() << " states and " << transitionMatrix.getNonZeroCount() << " transitions." << std::endl; - // Finally, we build the DDs for a reward structure, if requested. - boost::optional, storm::dd::Dd>> stateAndTransitionRewards; - if (options.buildRewards) { - // If a specific reward model was selected or one with the empty name exists, select it. - storm::prism::RewardModel rewardModel = storm::prism::RewardModel(); - if (options.rewardModelName) { - rewardModel = preparedProgram.getRewardModel(options.rewardModelName.get()); - } else if (preparedProgram.hasRewardModel("")) { - rewardModel = preparedProgram.getRewardModel(""); - } else if (preparedProgram.hasRewardModel()) { - // Otherwise, we select the first one. - rewardModel = preparedProgram.getRewardModel(0); - } - - STORM_LOG_TRACE("Building reward structure."); - stateAndTransitionRewards = createRewardDecisionDiagrams(generationInfo, rewardModel, transitionMatrix); - } - return std::make_pair(reachableStates, transitionMatrix); } @@ -720,1059 +723,6 @@ namespace storm { return reachableStatesBdd; } -// template -// storm::dd::Dd SymbolicModelAdapter::createSystemDecisionDiagramm(GenerationInformation & generationInfo){ -// -// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size(); -// -// // System DDs -// SystemComponentDecisionDiagram systemDds(0); -// SystemComponentDecisionDiagram systemDds1(0); -// SystemComponentDecisionDiagram systemDds2(0); -// -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// -// // Initialize usedNondetVariablesVector -// // TODO: Formulate simpler. -// std::vector usedNondetVariablesVector(numberOfSynchronizingActions); -// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j) { -// usedNondetVariablesVector[j] = 0; -// } -// -// // Create DD for first module -// systemDds = createSystemComponentDecisionDiagramm(generationInfo, generationInfo.program.getModule(0), usedNondetVariablesVector); -// -// for (uint_fast64_t i = 1; i < generationInfo.program.getNumberOfModules(); ++i) { -// -// // Create new usedNondetVariablesVector -// std::vector newUsedNondetVariablesVector(numberOfSynchronizingActions); -// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j) { -// // Check if systemDds contains action -// if (std::find(systemDds.allSynchronizingActions.begin(), systemDds.allSynchronizingActions.end(), generationInfo.allSynchronizingActions[j]) != systemDds.allSynchronizingActions.end()) { -// newUsedNondetVariablesVector[j] = systemDds.synchronizingActionDds[j].usedNondetVariables; -// } -// else{ -// newUsedNondetVariablesVector[j] = usedNondetVariablesVector[j]; -// } -// } -// -// // Create DD for next module -// systemDds2 = createSystemComponentDecisionDiagramm(generationInfo, generationInfo.program.getModule(i), newUsedNondetVariablesVector); -// -// // SystemDds1 stores the previous modules (already combined) -// systemDds1 = SystemComponentDecisionDiagram(systemDds); -// -// // SystemDds is used to store combination of SystemDds1 and SystemDds2 -// systemDds = SystemComponentDecisionDiagram(numberOfSynchronizingActions); -// -// // Combine non-synchronizing/independent actions -// systemDds.independentActionDd = combineModules(generationInfo, false, systemDds1.independentActionDd, systemDds2.independentActionDd, systemDds1.identityMatrix, systemDds2.identityMatrix); -// -// // Combine synchronizing actions -// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j){ -// // Check if both modules contain the current action -// if (std::find(systemDds1.allSynchronizingActions.begin(), systemDds1.allSynchronizingActions.end(), generationInfo.allSynchronizingActions[j]) != systemDds1.allSynchronizingActions.end() && -// std::find(systemDds2.allSynchronizingActions.begin(), systemDds2.allSynchronizingActions.end(), generationInfo.allSynchronizingActions[j]) != systemDds2.allSynchronizingActions.end()) { -// // Both modules contain action -// systemDds.synchronizingActionDds[j] = combineModules(generationInfo, true, systemDds1.synchronizingActionDds[j], systemDds2.synchronizingActionDds[j], systemDds1.identityMatrix, systemDds2.identityMatrix); -// } -// else { -// // Only one or no module contains current action -// systemDds.synchronizingActionDds[j] = combineModules(generationInfo, false, systemDds1.synchronizingActionDds[j], systemDds2.synchronizingActionDds[j], systemDds1.identityMatrix, systemDds2.identityMatrix); -// } -// } -// -// // Combine identity matrix -// systemDds.identityMatrix = systemDds1.identityMatrix * systemDds2.identityMatrix; -// -// // Combine list of synchronizing actions -// systemDds.allSynchronizingActions.insert(systemDds1.allSynchronizingActions.begin(), systemDds1.allSynchronizingActions.end()); -// systemDds.allSynchronizingActions.insert(systemDds2.allSynchronizingActions.begin(), systemDds2.allSynchronizingActions.end()); -// } -// -// // Combine all DDs -// systemDds = combineSystem(generationInfo, systemDds); -// generationInfo.globalSystemDds = SystemComponentDecisionDiagram(systemDds); -// -// -// // Build state and transition rewards -// generationInfo.rewardDds = computeRewards(generationInfo, systemDds); -// -// // Create transition to action mapping for MDPs -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// generationInfo.transitionActionDd = computeTransitionAction(generationInfo, systemDds); -// } -// -// // Normalize each row for DTMCs -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { -// temporary = storm::dd::Dd(systemDds.independentActionDd.commandsDd); -// temporary = temporary.sumAbstract(generationInfo.columnMetaVariableNames); -// systemDds.independentActionDd.commandsDd = systemDds.independentActionDd.commandsDd / temporary; -// } -// -// // Get system transition matrix -// storm::dd::Dd systemTransitionMatrix = systemDds.independentActionDd.commandsDd; -// -// return systemTransitionMatrix; -// } -// -// template -// SystemComponentDecisionDiagram SymbolicModelAdapter::combineSystem(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram systemDds){ -// -// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size(); -// uint_fast64_t max = 0; -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// storm::dd::Dd variableDd = generationInfo.manager->getZero(); -// -// // Add non-determinism variables for MDPs -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// // Check DD variables -// -// // Look for maximal variable index -// max = systemDds.independentActionDd.usedNondetVariables; -// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){ -// if (systemDds.synchronizingActionDds[i].usedNondetVariables > max) { -// max = systemDds.synchronizingActionDds[i].usedNondetVariables; -// } -// } -// -// // Add variables to independent action DD (if required) -// if (max > systemDds.independentActionDd.usedNondetVariables) { -// temporary = generationInfo.manager->getOne(); -// for (uint_fast64_t i = systemDds.independentActionDd.usedNondetVariables+1; i <= max; ++i){ -// -// // Get variable and set to 0 -// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0); -// temporary = temporary * variableDd; -// -// } -// systemDds.independentActionDd.commandsDd = systemDds.independentActionDd.commandsDd * temporary; -// systemDds.independentActionDd.usedNondetVariables = max; -// } -// -// // Add variables to synchronized action DDs -// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j){ -// if (max > systemDds.synchronizingActionDds[j].usedNondetVariables) { -// temporary = generationInfo.manager->getOne(); -// for (uint_fast64_t i = systemDds.synchronizingActionDds[j].usedNondetVariables+1; i <= max; ++i){ -// -// // Get variable and set to 0 -// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0); -// temporary = temporary * variableDd; -// -// } -// systemDds.synchronizingActionDds[j].commandsDd = systemDds.synchronizingActionDds[j].commandsDd * temporary; -// systemDds.synchronizingActionDds[j].usedNondetVariables = max; -// } -// } -// -// // Set variables for synchronization -// temporary = generationInfo.manager->getOne(); -// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){ -// // Get sync variable -// variableDd = generationInfo.manager->getEncoding("sync" + std::to_string(i), 0); -// temporary = temporary * variableDd; -// } -// -// systemDds.independentActionDd.commandsDd = temporary * systemDds.independentActionDd.commandsDd; -// -// // Set variables for synchronized action DDs -// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){ -// temporary = generationInfo.manager->getOne(); -// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j){ -// // Enable synchronizing variable j iff current action i==j -// if (i == j) { -// variableDd = generationInfo.manager->getEncoding("sync" + std::to_string(j), 1); -// temporary = temporary * variableDd; -// } -// else { -// variableDd = generationInfo.manager->getEncoding("sync" + std::to_string(j), 0); -// temporary = temporary * variableDd; -// } -// } -// -// systemDds.synchronizingActionDds[i].commandsDd = temporary * systemDds.synchronizingActionDds[i].commandsDd; -// } -// -// } -// -// // Create transition matrix -// temporary = systemDds.independentActionDd.commandsDd; -// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){ -// temporary = temporary + systemDds.synchronizingActionDds[i].commandsDd; -// } -// -// // Store transition matrix in systemDDs structure -// systemDds.independentActionDd.commandsDd = temporary; -// -// return systemDds; -// } -// -// template -// ModuleDecisionDiagram SymbolicModelAdapter::combineModules(GenerationInformation const & generationInfo, bool synchronizing, ModuleDecisionDiagram moduleDd1, ModuleDecisionDiagram moduleDd2, storm::dd::Dd const& identityDd1, storm::dd::Dd const& identityDd2){ -// -// // Module DD -// ModuleDecisionDiagram moduleDd = ModuleDecisionDiagram(); -// -// if (synchronizing) { -// // Synchronizing actions -// -// // Combine guards (intersection) -// moduleDd.guardDd = moduleDd1.guardDd * moduleDd2.guardDd; -// -// // Combine transitions -// moduleDd.commandsDd = moduleDd1.commandsDd * moduleDd2.commandsDd; -// -// // Update min/max index -// moduleDd.usedNondetVariables = (moduleDd1.usedNondetVariables > moduleDd2.usedNondetVariables) ? moduleDd1.usedNondetVariables : moduleDd2.usedNondetVariables; -// -// } else { -// // Non-synchronizing actions -// -// // Multiply commands with identity matrix (because of non-synchronization) -// moduleDd1.commandsDd = moduleDd1.commandsDd * identityDd2; -// moduleDd2.commandsDd = moduleDd2.commandsDd * identityDd1; -// -// // Combine modules -// switch (generationInfo.program.getModelType()) { -// case storm::prism::Program::ModelType::DTMC: -// -// // No non-determinism, just sum up -// moduleDd.guardDd = moduleDd1.guardDd + moduleDd2.guardDd; -// moduleDd.commandsDd = moduleDd1.commandsDd + moduleDd2.commandsDd; -// moduleDd.usedNondetVariables = 0; -// break; -// case storm::prism::Program::ModelType::MDP: -// -// // Combine modules and solve non-determinism -// moduleDd = combineModulesMDP(generationInfo, moduleDd1, moduleDd2); -// break; -// default: -// STORM_LOG_ASSERT(false, "Illegal model type."); -// } -// } -// -// return moduleDd; -// } -// -// template -// ModuleDecisionDiagram SymbolicModelAdapter::combineModulesMDP(GenerationInformation const & generationInfo, ModuleDecisionDiagram moduleDd1, ModuleDecisionDiagram moduleDd2){ -// -// // Module DD -// ModuleDecisionDiagram moduleDd = ModuleDecisionDiagram(); -// -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// storm::dd::Dd variableDd = generationInfo.manager->getZero(); -// -// // Check if one command DD equals 0 -// if (moduleDd1.commandsDd.isZero()) { -// moduleDd.guardDd = moduleDd2.guardDd; -// moduleDd.commandsDd = moduleDd2.commandsDd; -// moduleDd.usedNondetVariables = moduleDd2.usedNondetVariables; -// return moduleDd; -// } -// if (moduleDd2.commandsDd.isZero()) { -// moduleDd.guardDd = moduleDd1.guardDd; -// moduleDd.commandsDd = moduleDd1.commandsDd; -// moduleDd.usedNondetVariables = moduleDd1.usedNondetVariables; -// return moduleDd; -// } -// -// // Solve non-determinism -// -// // Check index of DD variables -// if (moduleDd1.usedNondetVariables > moduleDd2.usedNondetVariables) { -// temporary = generationInfo.manager->getOne(); -// -// for (uint_fast64_t i = moduleDd2.usedNondetVariables+1; i <= moduleDd1.usedNondetVariables; ++i){ -// // Get variable and set to 0 -// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0); -// temporary = temporary * variableDd; -// } -// moduleDd2.commandsDd = moduleDd2.commandsDd * temporary; -// moduleDd2.usedNondetVariables = moduleDd1.usedNondetVariables; -// } -// if (moduleDd2.usedNondetVariables > moduleDd1.usedNondetVariables) { -// temporary = generationInfo.manager->getOne(); -// -// for (uint_fast64_t i = moduleDd1.usedNondetVariables+1; i <= moduleDd2.usedNondetVariables; ++i){ -// // Get variable and set to 0 -// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0); -// temporary = temporary * variableDd; -// } -// moduleDd1.commandsDd = moduleDd1.commandsDd * temporary; -// moduleDd1.usedNondetVariables = moduleDd2.usedNondetVariables; -// } -// -// // Get new nondet. variable -// variableDd = variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(moduleDd1.usedNondetVariables + 1), 1); -// -// // Set nondet. variable -// moduleDd2.commandsDd = moduleDd2.commandsDd * variableDd; -// moduleDd1.commandsDd = moduleDd1.commandsDd * (!variableDd); -// -// // Combine command DDs -// moduleDd.commandsDd = moduleDd1.commandsDd + moduleDd2.commandsDd; -// -// // Combine guard DDs -// moduleDd.guardDd = moduleDd1.guardDd || moduleDd2.guardDd; -// -// moduleDd.usedNondetVariables = moduleDd1.usedNondetVariables + 1; -// -// return moduleDd; -// } -// -// template -// SystemComponentDecisionDiagram SymbolicModelAdapter::createSystemComponentDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, std::vector usedNondetVariablesVector){ -// -// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size(); -// -// // System Component DD -// SystemComponentDecisionDiagram systemComponentDd(numberOfSynchronizingActions); -// -// // Create module DD for independent actions -// systemComponentDd.independentActionDd = createModuleDecisionDiagramm(generationInfo, module, "", 0); -// -// // Create module DD for synchronizing actions -// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){ -// -// if (module.hasAction(generationInfo.allSynchronizingActions[i])){ -// systemComponentDd.synchronizingActionDds[i] = createModuleDecisionDiagramm(generationInfo, module, generationInfo.allSynchronizingActions[i], usedNondetVariablesVector[i]); -// }else{ -// switch (generationInfo.program.getModelType()){ -// case storm::prism::Program::ModelType::DTMC: -// systemComponentDd.synchronizingActionDds[i] = ModuleDecisionDiagram(generationInfo.manager->getZero(), generationInfo.manager->getZero(), 0); -// break; -// case storm::prism::Program::ModelType::MDP: -// systemComponentDd.synchronizingActionDds[i] = ModuleDecisionDiagram(generationInfo.manager->getZero(), generationInfo.manager->getZero(), usedNondetVariablesVector[i]); -// break; -// default: -// STORM_LOG_ASSERT(false, "Illegal model type."); -// } -// } -// -// } -// -// // Get module identity matrix -// systemComponentDd.identityMatrix = generationInfo.moduleToIdentityDecisionDiagramMap.at(module.getName()); -// -// // Store all synchronizing actions -// systemComponentDd.allSynchronizingActions.insert(module.getActions().begin(), module.getActions().end()); -// -// return systemComponentDd; -// } -// -// // TODO -// std::map getMetaVariableMapping(std::vector metaVariables, uint_fast64_t value){ -// -// std::map metaVariableNameToValueMap = std::map(); -// -// for (uint_fast64_t i = 0; i < metaVariables.size(); ++i) { -// if (value & (1ull << (metaVariables.size() - i - 1))) { -// metaVariableNameToValueMap.insert(std::make_pair(metaVariables[i], 1)); -// } -// else { -// metaVariableNameToValueMap.insert(std::make_pair(metaVariables[i], 0)); -// } -// } -// -// return metaVariableNameToValueMap; -// } -// -// template -// ModuleDecisionDiagram SymbolicModelAdapter::combineCommandsMDP(std::shared_ptr> const & manager, uint_fast64_t numberOfCommands, std::vector> const& commandDds, std::vector> const & guardDds, uint_fast64_t usedNondetVariables){ -// -// // Module DD -// ModuleDecisionDiagram moduleDd = ModuleDecisionDiagram(); -// -// // Initialize DDs -// storm::dd::Dd guardRangeDd = manager->getZero(); -// storm::dd::Dd commandsDd = manager->getZero(); -// storm::dd::Dd temporaryDd = manager->getZero(); -// -// // Check for overlapping guards -// storm::dd::Dd overlappingGuardDd = manager->getZero(); -// -// for (uint_fast64_t i = 0; i < numberOfCommands; ++i) { -// overlappingGuardDd = overlappingGuardDd + guardDds[i]; -// guardRangeDd = guardRangeDd || guardDds[i]; -// } -// -// uint_fast64_t maxChoices = overlappingGuardDd.getMax(); -// -// // Check for no choice or no non-determinism -// if (maxChoices == 0 || maxChoices == 1) { -// -// if (maxChoices == 1) { -// // Sum up all command updates -// for (uint_fast64_t i = 0; i < numberOfCommands; ++i) { -// temporaryDd = guardDds[i] * commandDds[i]; -// commandsDd = commandsDd + temporaryDd; -// } -// } -// -// moduleDd.guardDd = guardRangeDd; -// moduleDd.commandsDd = commandsDd; -// moduleDd.usedNondetVariables = usedNondetVariables; -// -// return moduleDd; -// } -// -// // Calculate number of required variables (log2(maxChoices)) -// uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(log2(maxChoices))); -// -// // Allocate local nondet. choice variables -// std::vector nondetVariables(numberOfBinaryVariables); -// for (uint_fast64_t i = 1; i <= numberOfBinaryVariables; ++i) { -// nondetVariables[i-1] = "nondet" + std::to_string(usedNondetVariables + i); -// } -// -// // Initialize more DDs -// storm::dd::Dd equalsNumberOfChoicesDd = manager->getZero(); -// std::vector> choiceDds(maxChoices); -// std::vector> remainingDds(maxChoices); -// -// storm::dd::Dd temporaryDd1 = manager->getZero(); -// storm::dd::Dd temporaryDd2 = manager->getZero(); -// -// for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { -// -// // Check for paths with exactly i nondet. choices -// equalsNumberOfChoicesDd = overlappingGuardDd.equals(manager->getConstant(static_cast (currentChoices))); -// -// if (equalsNumberOfChoicesDd.isZero()) continue; -// -// // Reset DDs -// for (uint_fast64_t j = 0; j < currentChoices; ++j) { -// choiceDds[j] = manager->getZero(); -// remainingDds[j] = equalsNumberOfChoicesDd; -// } -// -// // Check all commands -// for (uint_fast64_t j = 0; j < numberOfCommands; ++j) { -// -// // Check if command guard overlaps with equalsNumberOfChoicesDd -// temporaryDd1 = guardDds[j] && equalsNumberOfChoicesDd; -// if (temporaryDd1.isZero()) continue; -// -// // Split nondet. choices -// for (uint_fast64_t k = 0; k < currentChoices; ++k) { -// -// // Calculate maximal overlapping parts of command guard and remaining DD (for current index) -// temporaryDd2 = temporaryDd1 && remainingDds[k]; -// -// // Check if we can add some overlapping parts to the current index -// if (temporaryDd2 != manager->getZero()) { -// -// // Remove overlapping parts from the remaining DD -// remainingDds[k] = remainingDds[k] && (!temporaryDd2); -// -// // Combine guard (overlapping parts) with command updates -// temporaryDd = temporaryDd2 * commandDds[j]; -// // Add command DD to the commands with current index -// choiceDds[k] = choiceDds[k] + temporaryDd; -// } -// -// // Remove overlapping parts from the command guard DD -// temporaryDd1 = temporaryDd1 && (!temporaryDd2); -// -// // Check if the command guard DD is already 0 -// if (temporaryDd1.isZero()) break; -// } -// } -// -// // Set nondet. choices for corresponding DDs -// for (uint_fast64_t j = 0; j < currentChoices; ++j) { -// -// temporaryDd1 = manager->getZero(); -// -// // Set chosen variables to value j -// temporaryDd1.setValue(getMetaVariableMapping(nondetVariables, j), 1); -// -// // Multiply setting of nondet. variables with corresponding commands -// temporaryDd = temporaryDd1 * choiceDds[j]; -// // Sum up all DDs (no non-determinism any more) -// commandsDd = commandsDd + temporaryDd; -// } -// -// // Delete currentChoices out of overlapping DD -// overlappingGuardDd = overlappingGuardDd * (!equalsNumberOfChoicesDd); -// } -// -// moduleDd.guardDd = guardRangeDd; -// moduleDd.commandsDd = commandsDd; -// moduleDd.usedNondetVariables = usedNondetVariables + numberOfBinaryVariables; -// -// return moduleDd; -// } -// -// template -// ModuleDecisionDiagram SymbolicModelAdapter::createModuleDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, std::string const& synchronizingAction, uint_fast64_t usedNondetVariables){ -// -// // Module DD -// ModuleDecisionDiagram moduleDd; -// -// // Set up vectors -// uint_fast64_t numberOfCommands = module.getNumberOfCommands(); -// std::vector> guardDds(numberOfCommands); -// std::vector> commandDds(numberOfCommands); -// -// for (uint_fast64_t j = 0; j < numberOfCommands; ++j) { -// -// storm::prism::Command const& command = module.getCommand(j); -// -// // Check if command action matches requested synchronizing action -// if (synchronizingAction == command.getActionName()) { -// -// // Translate guard -// guardDds[j] = storm::adapters::SymbolicExpressionAdapter::translateExpression(command.getGuardExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager); -// -// if (guardDds[j].isZero()){ -// LOG4CPLUS_WARN(logger, "A guard is unsatisfiable."); -// } -// -// // Create command DD -// commandDds[j] = createCommandDecisionDiagramm(generationInfo, module, guardDds[j], command); -// -// commandDds[j] = commandDds[j] * guardDds[j]; -// -// // check negative probabilities/rates -// if (commandDds[j].getMin() < 0){ -// LOG4CPLUS_WARN(logger, "Negative probabilites/rates in command " << (j + 1) << "."); -// } -// } -// else { -// // Otherwise use zero DDs -// guardDds[j] = generationInfo.manager->getZero(); -// commandDds[j] = generationInfo.manager->getZero(); -// } -// } -// -// // combine command DDs with guard DDs -// switch (generationInfo.program.getModelType()){ -// case storm::prism::Program::ModelType::DTMC: -// moduleDd = combineCommandsDTMC(generationInfo.manager, numberOfCommands, commandDds, guardDds); -// break; -// case storm::prism::Program::ModelType::MDP: -// moduleDd = combineCommandsMDP(generationInfo.manager, numberOfCommands, commandDds, guardDds, usedNondetVariables); -// break; -// default: -// STORM_LOG_ASSERT(false, "Illegal model type."); -// } -// -// return moduleDd; -// } -// -// template -// storm::dd::Dd SymbolicModelAdapter::createCommandDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Command const& command){ -// -// // Command DD -// storm::dd::Dd commandDd = generationInfo.manager->getZero(); -// -// for (uint_fast64_t i = 0; i < command.getNumberOfUpdates(); ++i) { -// -// // Create update DD -// storm::dd::Dd updateDd = createUpdateDecisionDiagramm(generationInfo, module, guard, command.getUpdate(i)); -// -// if (updateDd.isZero()){ -// LOG4CPLUS_WARN(logger, "Update " << (i + 1) << " does not do anything."); -// } -// -// // Multiply likelihood expression (MDP: transition probability) -// double p = command.getUpdate(i).getLikelihoodExpression().evaluateAsDouble(); -// -// updateDd = updateDd * generationInfo.manager->getConstant(p); -// -// commandDd = commandDd + updateDd; -// } -// -// return commandDd; -// } -// -// template -// storm::dd::Dd SymbolicModelAdapter::createUpdateDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update){ -// -// // Update DD -// storm::dd::Dd updateDd = generationInfo.manager->getOne(); -// -// // Assignments (integer and boolean) -// std::vector assignments = update.getAssignments(); -// for (auto singleAssignment : assignments) { -// -// // Translate first part of assignment -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// -// temporary = generationInfo.manager->getIdentity(singleAssignment.getVariableName() + "'"); -// -// // Translate second part of assignment -// storm::dd::Dd updateExpr = storm::adapters::SymbolicExpressionAdapter::translateExpression(singleAssignment.getExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager); -// -// storm::dd::Dd result = updateExpr * guard; -// // Combine first and second part of the assignment -// result = result.equals(temporary); -// result = result * guard; -// -// // Filter range -// result = result * generationInfo.manager->getRange(singleAssignment.getVariableName() + "'"); -// -// updateDd = updateDd * result; -// } -// -// // All unused global boolean variables do not change -// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalBooleanVariables().size(); ++i) { -// storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(i); -// if (update.getAssignmentMapping().find(booleanVariable.getName()) == update.getAssignmentMapping().end()) { -// // Multiply identity matrix -// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(booleanVariable.getName()); -// } -// } -// -// // All unused global integer variables do not change -// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalIntegerVariables().size(); ++i) { -// storm::prism::IntegerVariable const& integerVariable = generationInfo.program.getGlobalIntegerVariables().at(i); -// if (update.getAssignmentMapping().find(integerVariable.getName()) == update.getAssignmentMapping().end()) { -// // Multiply identity matrix -// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName()); -// } -// } -// -// // All unused boolean variables do not change -// for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); ++i) { -// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(i); -// if (update.getAssignmentMapping().find(booleanVariable.getName()) == update.getAssignmentMapping().end()) { -// // Multiply identity matrix -// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(booleanVariable.getName()); -// } -// } -// -// // All unused integer variables do not change -// for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); ++i) { -// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(i); -// if (update.getAssignmentMapping().find(integerVariable.getName()) == update.getAssignmentMapping().end()) { -// // Multiply identity matrix -// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName()); -// } -// } -// -// return updateDd; -// } -// -// template -// storm::dd::Dd SymbolicModelAdapter::getInitialStateDecisionDiagram(GenerationInformation const & generationInfo) { -// storm::dd::Dd initialStates = generationInfo.manager->getOne(); -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// -// // Global Boolean variables -// for (uint_fast64_t j = 0; j < generationInfo.program.getGlobalBooleanVariables().size(); ++j) { -// storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(j); -// temporary = generationInfo.manager->getEncoding(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool()); -// initialStates = initialStates * temporary; -// } -// -// // Global Integer variables -// for (uint_fast64_t j = 0; j < generationInfo.program.getGlobalIntegerVariables().size(); ++j) { -// storm::prism::IntegerVariable const& integerVariable = generationInfo.program.getGlobalIntegerVariables().at(j); -// temporary = generationInfo.manager->getEncoding(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt()); -// initialStates = initialStates * temporary; -// } -// -// for (uint_fast64_t i = 0; i < generationInfo.program.getNumberOfModules(); ++i) { -// storm::prism::Module const& module = generationInfo.program.getModule(i); -// -// // Boolean variables -// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { -// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(j); -// temporary = generationInfo.manager->getEncoding(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool()); -// initialStates = initialStates * temporary; -// } -// -// // Integer variables -// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { -// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(j); -// temporary = generationInfo.manager->getEncoding(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt()); -// initialStates = initialStates * temporary; -// } -// } -// -// return initialStates; -// } -// -// template -// storm::dd::Dd SymbolicModelAdapter::performReachability(GenerationInformation & generationInfo, storm::dd::Dd const& systemDd, storm::dd::Dd const& initialStateDd) { -// -// // Initialize the clock. -// auto clock = std::chrono::high_resolution_clock::now(); -// -// -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// storm::dd::Dd S; -// storm::dd::Dd U; -// -// // Get initial state -// storm::dd::Dd reachableStates = initialStateDd; -// -// // Copy current state -// storm::dd::Dd newReachableStates = reachableStates; -// -// std::set abstractVariables = std::set(); -// -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// // Synchronizing variables -// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) { -// abstractVariables.insert("sync" + std::to_string(i)); -// } -// } -// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) { -// // Nondet. variables -// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) { -// abstractVariables.insert("nondet" + std::to_string(i)); -// } -// } -// } -// -// // Create system BDD -// storm::dd::Dd systemBdd = systemDd.notZero(); -// -// // For MDPs, we need to abstract from the nondeterminism variables, but we can do so prior to the -// // reachability analysis. -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// // Abstract from synchronizing and nondet. variables (MDPs) -// systemBdd = systemBdd.existsAbstract(abstractVariables); -// } -// -// // Initialize variables and choose option -// bool changed; -// int iter = 0; -// int option = storm::settings::adapterSettings().getReachabilityMethod(); -// -// //TODO: Name reachability options. -// std::cout << "Reachability option: " << option << std::endl; -// -// if (option == 3 || option == 4){ -// -// S = storm::dd::Dd(initialStateDd); -// U = storm::dd::Dd(initialStateDd); -// -// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.notZero(); -// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.existsAbstract(abstractVariables); -// -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.notZero(); -// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.existsAbstract(abstractVariables); -// } -// } -// -// // Perform updates until nothing changes -// do { -// if (option == 1){ -// iter++; -// changed = true; -// -// newReachableStates = newReachableStates * systemBdd; -// -// // Abstract from row meta variables -// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames); -// -// // Swap column variables to row variables -// newReachableStates.swapVariables(generationInfo.metaVariablePairs); -// -// newReachableStates = newReachableStates * (!reachableStates); -// -// // Check if something has changed -// if (newReachableStates.isZero()) { -// changed = false; -// } -// -// // Update reachableStates DD -// reachableStates = reachableStates + newReachableStates; -// -// } else if (option == 2) { -// iter++; -// changed = false; -// -// newReachableStates = newReachableStates * systemBdd; -// -// // Abstract from row meta variables -// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames); -// -// // Swap column variables to row variables -// newReachableStates.swapVariables(generationInfo.metaVariablePairs); -// -// newReachableStates = newReachableStates || reachableStates; -// -// // Check if something has changed -// if (newReachableStates != reachableStates) { -// changed = true; -// } -// -// // Update reachableStates DD -// reachableStates = newReachableStates; -// -// } else if (option == 3) { -// iter++; -// changed = true; -// -// newReachableStates = generationInfo.manager->getZero(); -// -// temporary = U * generationInfo.globalSystemDds.independentActionDd.commandsDd; -// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames); -// newReachableStates.swapVariables(generationInfo.metaVariablePairs); -// newReachableStates = temporary; -// -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// temporary = U * generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd; -// temporary = temporary.existsAbstract(generationInfo.rowMetaVariableNames); -// temporary.swapVariables(generationInfo.metaVariablePairs); -// newReachableStates = newReachableStates || temporary; -// } -// -// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames); -// newReachableStates.swapVariables(generationInfo.metaVariablePairs); -// U = U || newReachableStates; -// -// if (U == S){ -// changed = false; -// reachableStates = S; -// break; -// } -// -// S = S || U; -// -// } -// else if (option == 4) { -// iter++; -// changed = true; -// -// temporary = U * generationInfo.globalSystemDds.independentActionDd.commandsDd; -// temporary = temporary.existsAbstract(generationInfo.rowMetaVariableNames); -// temporary.swapVariables(generationInfo.metaVariablePairs); -// U = U || temporary; -// -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// temporary = U * generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd; -// temporary = temporary.existsAbstract(generationInfo.rowMetaVariableNames); -// temporary.swapVariables(generationInfo.metaVariablePairs); -// U = U || temporary; -// } -// -// U = U * (!S); -// -// S = S + U; -// -// if (U.isZero()){ -// changed = false; -// reachableStates = S; -// } -// -// } -// } while (changed); -// -// std::cout << "Performed reachability (" << iter << " iterations) in " << std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl; -// -// return reachableStates; -// } -// -// template -// storm::dd::Dd SymbolicModelAdapter::findDeadlocks(GenerationInformation const & generationInfo, storm::dd::Dd systemDd, storm::dd::Dd const& reachableStatesDd) { -// -// // Initialize the clock. -// auto clock = std::chrono::high_resolution_clock::now(); -// -// storm::dd::Dd systemBdd = systemDd.notZero(); -// -// std::set abstractVariables = std::set(); -// -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// // Synchronizing variables -// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) { -// abstractVariables.insert("sync" + std::to_string(i)); -// } -// } -// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) { -// // Nondet. variables -// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) { -// abstractVariables.insert("nondet" + std::to_string(i)); -// } -// } -// } -// -// // Find states with at least one transition -// systemBdd = systemBdd.existsAbstract(generationInfo.columnMetaVariableNames); -// -// // For MDPs, we need to abstract from the nondeterminism variables -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// // Abstract from synchronizing and nondet. variables (MDPs) -// systemBdd = systemBdd.existsAbstract(abstractVariables); -// } -// -// systemBdd = reachableStatesDd * (!systemBdd); -// -// std::cout << "Deadlocks: " << systemBdd.getNonZeroCount() << " fixed." << std::endl; -// -// // Check if there are deadlocks -// if (!systemBdd.isZero()){ -// -// storm::dd::Dd temporary = generationInfo.manager->getOne(); -// -// // Get all variable identities -// for (auto variable : generationInfo.rowMetaVariableNames) { -// temporary = temporary * generationInfo.variableToIdentityDecisionDiagramMap.at(variable); -// } -// -// // Add synchronizing and nondet. variables to identity for MDPs (all set to 0) -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// // Synchronizing variables -// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) { -// temporary = temporary * generationInfo.manager->getEncoding("sync" + std::to_string(i),0); -// } -// } -// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) { -// // Nondet. variables -// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) { -// temporary = temporary * generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0); -// } -// } -// } -// -// temporary = temporary * systemBdd; -// -// // Add self-loops to transition matrix -// systemDd = systemDd + temporary; -// } -// -// std::cout << "Fixed deadlocks in " << std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl; -// -// return systemDd; -// } -// -// template -// std::pair>, std::vector>> SymbolicModelAdapter::computeRewards(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram const& systemDds) { -// -// // Get number of reward modules and synchronizing actions -// uint_fast64_t numberOfRewardModules = generationInfo.program.getRewardModels().size(); -// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size(); -// -// // State reward DD -// std::vector> stateRewardsDds = std::vector>(numberOfRewardModules); -// // Transition reward DD -// std::vector> transitionRewardsDds = std::vector>(numberOfRewardModules); -// -// // Initialize DDs -// for (uint_fast64_t i = 0; i < numberOfRewardModules; ++i) { -// stateRewardsDds[i] = generationInfo.manager->getConstant(0); -// transitionRewardsDds[i] = generationInfo.manager->getConstant(0); -// } -// -// storm::dd::Dd statesDd = generationInfo.manager->getZero(); -// storm::dd::Dd rewardsDd = generationInfo.manager->getZero(); -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// -// // Loop through all reward models -// for (uint_fast64_t i = 0; i < numberOfRewardModules; ++i) { -// storm::prism::RewardModel const& currentRewardModule = generationInfo.program.getRewardModels().at(i); -// -// // State rewards -// for (auto stateReward : currentRewardModule.getStateRewards()) { -// -// // Translate state and reward expression -// statesDd = storm::adapters::SymbolicExpressionAdapter::translateExpression(stateReward.getStatePredicateExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager); -// rewardsDd = storm::adapters::SymbolicExpressionAdapter::translateExpression(stateReward.getRewardValueExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager); -// -// // Restrict rewards to states -// temporary = statesDd * rewardsDd; -// -// // Check for negative rewards -// if (temporary.getMin() < 0){ -// LOG4CPLUS_WARN(logger, "Negative state reward in reward model " << (i + 1) << "."); -// } -// -// if(temporary.isZero()) { -// LOG4CPLUS_WARN(logger, "Only zero rewards in reward model " << (i + 1) << "."); -// } -// -// // Combine all rewards -// stateRewardsDds[i] = stateRewardsDds[i] + temporary; -// } -// -// // Transition rewards -// for (auto transitionReward : currentRewardModule.getTransitionRewards()) { -// -// // Translate state and reward expression -// statesDd = storm::adapters::SymbolicExpressionAdapter::translateExpression(transitionReward.getStatePredicateExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager); -// rewardsDd = storm::adapters::SymbolicExpressionAdapter::translateExpression(transitionReward.getRewardValueExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager); -// -// // Get action name of the transition -// std::string const& rewardAction = transitionReward.getActionName(); -// -// if (rewardAction == "") { -// // Take independent action module -// temporary = systemDds.independentActionDd.commandsDd; -// }else { -// // Get module corresponding to the reward action -// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j) { -// if (generationInfo.allSynchronizingActions[j] == rewardAction) { -// temporary = systemDds.synchronizingActionDds[j].commandsDd; -// break; -// } -// } -// } -// -// // Convert to BDD for MDPs (DTMC need exact values for scaling) -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// temporary = temporary.notZero(); -// } -// -// // Restrict to states and multiply reward values -// temporary = temporary * statesDd; -// temporary = temporary * rewardsDd; -// -// // Check for negative rewards -// if (temporary.getMin() < 0){ -// LOG4CPLUS_WARN(logger, "Negative transition reward in reward model " << (i + 1) << "."); -// } -// -// // Combine all rewards -// transitionRewardsDds[i] = transitionRewardsDds[i] + temporary; -// } -// } -// -// // Scale transition rewards for DTMCs -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { -// for (uint_fast64_t i = 0; i < generationInfo.program.getRewardModels().size(); ++i){ -// // Divide transition rewards through transition matrix -// transitionRewardsDds[i] = transitionRewardsDds[i] / systemDds.independentActionDd.commandsDd; -// } -// } -// -// // Pair to store state and transition rewards -// return std::make_pair(stateRewardsDds, transitionRewardsDds); -// } -// -// template -// storm::dd::Dd SymbolicModelAdapter::computeTransitionAction(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram const& systemDds){ -// -// // Transition actions DD -// storm::dd::Dd transitionActionDd = generationInfo.manager->getZero(); -// storm::dd::Dd temporary = generationInfo.manager->getZero(); -// -// // Store action labels for each transition (0 iff no action/tau/epsilon) -// storm::dd::Dd commandsBdd = generationInfo.manager->getZero(); -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i){ -// // Get action transition matrix as BDD -// commandsBdd = systemDds.synchronizingActionDds[i].commandsDd.notZero(); -// commandsBdd = commandsBdd.existsAbstract(generationInfo.columnMetaVariableNames); -// -// // Add action index -// temporary = commandsBdd * generationInfo.manager->getConstant(i + 1); -// transitionActionDd = transitionActionDd + temporary; -// } -// -// return transitionActionDd; -// } - // Explicitly instantiate the symbolic expression adapter template class DdPrismModelBuilder; diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 63670b259..e621cf5ca 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -299,7 +299,7 @@ namespace storm { static storm::dd::Dd createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static std::pair, storm::dd::Dd>createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, storm::dd::Dd transitionMatrix); + static std::pair, storm::dd::Dd> createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Dd const& fullTransitionMatrix); static std::pair, ModuleDecisionDiagram> createSystemDecisionDiagram(GenerationInformation& generationInfo); @@ -307,30 +307,6 @@ namespace storm { static storm::dd::Dd computeReachableStates(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions); -// /*! -// * Calculates the reachable states of the given transition matrix -// * -// * @param systemDd The transition matrix DD -// * @param initialStateDd All initial states -// * @return A DD representing all reachable states -// */ -// static storm::dd::Dd performReachability(GenerationInformation & generationInfo, storm::dd::Dd const& systemDd, storm::dd::Dd const& initialStateDd); -// -// /*! -// * Adds a self-loop to deadlock states -// * -// * @param systemDd The given DD -// * @param reachableStatesDd DD representing all reachable states -// * @return A DD with fixed deadlocks. -// */ -// static storm::dd::Dd findDeadlocks(GenerationInformation const & generationInfo, storm::dd::Dd systemDd, storm::dd::Dd const& reachableStatesDd); -// -// /*! -// * Computes state and transition rewards -// * -// * @param systemDds System DDs -// */ -// static std::pair>, std::vector>> computeRewards(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram const& systemDds); }; } // namespace adapters