diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 7b929edfc..755c4c78a 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -188,10 +188,7 @@ namespace storm { std::vector newCommands; newCommands.reserve(this->getNumberOfCommands()); for (auto const& command : this->getCommands()) { - Command newCommand = command.substitute(substitution); - if (!newCommand.getGuardExpression().isFalse()) { - newCommands.emplace_back(newCommand); - } + newCommands.emplace_back(command.substitute(substitution)); } return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber()); diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index acb17a17e..cdc3d323a 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -717,7 +717,7 @@ namespace storm { } Program Program::substituteConstants() const { - // We start by creating the appropriate substitution + // We start by creating the appropriate substitution. std::map constantSubstitution; std::vector newConstants(this->getConstants()); for (uint_fast64_t constantIndex = 0; constantIndex < newConstants.size(); ++constantIndex) { @@ -734,12 +734,6 @@ namespace storm { } } - // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to - // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a] - // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will - // remove the forced synchronization that was there before. - std::set actionIndicesToDelete; - // Now we can substitute the constants in all expressions appearing in the program. std::vector newBooleanVariables; newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables()); @@ -763,9 +757,6 @@ namespace storm { newModules.reserve(this->getNumberOfModules()); for (auto const& module : this->getModules()) { newModules.emplace_back(module.substitute(constantSubstitution)); - - // Determine the set of action indices that have been deleted entirely. - std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin())); } std::vector newRewardModels; @@ -782,37 +773,7 @@ namespace storm { newLabels.emplace_back(label.substitute(constantSubstitution)); } - // If we have to delete whole actions, do so now. - std::map newActionToIndexMap; - if (!actionIndicesToDelete.empty()) { - boost::container::flat_set actionsToKeep; - std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin())); - - // Insert the silent action as this is not contained in the synchronizing action indices. - actionsToKeep.insert(0); - - std::vector cleanedModules; - cleanedModules.reserve(this->getNumberOfModules()); - for (auto const& module : newModules) { - cleanedModules.emplace_back(module.restrictCommands(actionsToKeep)); - } - newModules = std::move(cleanedModules); - - std::vector cleanedRewardModels; - cleanedRewardModels.reserve(this->getNumberOfRewardModels()); - for (auto const& rewardModel : newRewardModels) { - cleanedRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep)); - } - newRewardModels = std::move(cleanedRewardModels); - - for (auto const& entry : this->getActionNameToIndexMapping()) { - if (actionsToKeep.find(entry.second) != actionsToKeep.end()) { - newActionToIndexMap.emplace(entry.first, entry.second); - } - } - } - - return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, actionIndicesToDelete.empty() ? this->getActionNameToIndexMapping() : newActionToIndexMap, newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct()); + return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct()); } void Program::checkValidity(Program::ValidityCheckLevel lvl) const { @@ -1195,13 +1156,22 @@ namespace storm { // Start by substituting the constants, because this will potentially erase some commands or even actions. Program substitutedProgram = this->substituteConstants(); + // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to + // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a] + // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will + // remove the forced synchronization that was there before. + std::set actionIndicesToDelete; + std::vector newModules; std::vector newConstants = substitutedProgram.getConstants(); for (auto const& module : substitutedProgram.getModules()) { - // Remove identity assignments from the updates. + + // Discard all commands with a guard equivalent to false and remove identity assignments from the updates. std::vector newCommands; for (auto const& command : module.getCommands()) { - newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates()); + if (!command.getGuardExpression().isFalse()) { + newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates()); + } } // Substitute variables by global constants if possible. @@ -1214,38 +1184,44 @@ namespace storm { integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression()); } + // Collect all variables that are being written. These variables cannot be turned to constants. for (auto const& command : newCommands) { // Check all updates. for (auto const& update : command.getUpdates()) { // Check all assignments. for (auto const& assignment : update.getAssignments()) { - auto bit = booleanVars.find(assignment.getVariable()); - if (bit != booleanVars.end()) { - booleanVars.erase(bit); + if (assignment.getVariable().getType().isBooleanType()) { + auto it = booleanVars.find(assignment.getVariable()); + if (it != booleanVars.end()) { + booleanVars.erase(it); + } } else { - auto iit = integerVars.find(assignment.getVariable()); - if (iit != integerVars.end()) { - integerVars.erase(iit); + auto it = integerVars.find(assignment.getVariable()); + if (it != integerVars.end()) { + integerVars.erase(it); } } } } } - std::vector newBVars; + std::vector newBooleanVars; for (auto const& variable : module.getBooleanVariables()) { if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) { - newBVars.push_back(variable); + newBooleanVars.push_back(variable); } } - std::vector newIVars; + std::vector newIntegerVars; for (auto const& variable : module.getIntegerVariables()) { if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) { - newIVars.push_back(variable); + newIntegerVars.push_back(variable); } } - newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands); + newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands); + + // Determine the set of action indices that have been deleted entirely. + std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin())); for (auto const& entry : booleanVars) { newConstants.emplace_back(entry.first, entry.second); @@ -1256,11 +1232,36 @@ namespace storm { } } - return substitutedProgram.replaceModulesAndConstantsInProgram(newModules, newConstants); - } - - Program Program::replaceModulesAndConstantsInProgram(std::vector const& newModules, std::vector const& newConstants) { - return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, getActionNameToIndexMapping(), getRewardModels(), getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct()); + // If we have to delete whole actions, do so now. + std::map newActionToIndexMap; + std::vector newRewardModels; + if (!actionIndicesToDelete.empty()) { + boost::container::flat_set actionsToKeep; + std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin())); + + // Insert the silent action as this is not contained in the synchronizing action indices. + actionsToKeep.insert(0); + + std::vector cleanedModules; + cleanedModules.reserve(newModules.size()); + for (auto const& module : newModules) { + cleanedModules.emplace_back(module.restrictCommands(actionsToKeep)); + } + newModules = std::move(cleanedModules); + + newRewardModels.reserve(substitutedProgram.getNumberOfRewardModels()); + for (auto const& rewardModel : substitutedProgram.getRewardModels()) { + newRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep)); + } + + for (auto const& entry : this->getActionNameToIndexMapping()) { + if (actionsToKeep.find(entry.second) != actionsToKeep.end()) { + newActionToIndexMap.emplace(entry.first, entry.second); + } + } + } + + return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getInitialConstruct(), this->getOptionalSystemCompositionConstruct()); } Program Program::flattenModules(std::unique_ptr const& smtSolverFactory) const { diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 71719c583..8c30079e0 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -661,14 +661,6 @@ namespace storm { // A mapping from variable names to the modules in which they were declared. std::map variableToModuleIndexMap; - - /** - * Takes the current program and replaces all modules. As we reuse the expression manager, we recommend to not use the original program any further. - * @param newModules the modules which replace the old modules. - * @param newConstants the constants which replace the old constants. - * @return A program with the new modules and constants. - */ - Program replaceModulesAndConstantsInProgram(std::vector const& newModules, std::vector const& newConstants); }; std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);