From 7beb99921954085a2c6be2f598ddb0c1ec1f1086 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 7 Mar 2021 23:03:29 -0800 Subject: [PATCH] label unlabelled commands --- src/storm/storage/prism/Module.cpp | 31 +++++++++++++++++++++++++ src/storm/storage/prism/Module.h | 14 +++++++++++ src/storm/storage/prism/Program.cpp | 31 ++++++++++++++++++++++++- src/storm/storage/prism/Program.h | 4 ++++ src/storm/storage/prism/RewardModel.cpp | 23 +++++++++++++++++- src/storm/storage/prism/RewardModel.h | 4 +++- 6 files changed, 104 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp index 3c9c8f698..232979c87 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -257,6 +257,37 @@ namespace storm { return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(), this->getLineNumber()); } + + Module Module::labelUnlabelledCommands(std::map const& suggestions, uint64_t& newId, std::map& nameToIdMapping) const { + std::vector newCommands; + newCommands.reserve(this->getNumberOfCommands()); + for (auto const& command : this->getCommands()) { + if (command.isLabeled()) { + newCommands.push_back(command); + } else { + if(suggestions.count(command.getGlobalIndex())) { + std::string newActionName = suggestions.at(command.getGlobalIndex()); + auto it = nameToIdMapping.find(newActionName); + uint64_t actionId = newId; + if (it == nameToIdMapping.end()) { + nameToIdMapping[newActionName] = newId; + newId++; + } else { + actionId = it->second; + } + newCommands.emplace_back(command.getGlobalIndex(), command.isMarkovian(), actionId, newActionName, command.getGuardExpression(), command.getUpdates(), command.getFilename(), command.getLineNumber()); + + } else { + std::string newActionName = getName() + "_cmd_" + std::to_string(command.getGlobalIndex()); + newCommands.emplace_back(command.getGlobalIndex(), command.isMarkovian(), newId, newActionName, command.getGuardExpression(), command.getUpdates(), command.getFilename(), command.getLineNumber()); + nameToIdMapping[newActionName] = newId; + newId++; + } + + } + } + return Module(this->getName(), booleanVariables, integerVariables, clockVariables, invariant, newCommands, this->getFilename(), this->getLineNumber()); + } bool Module::containsVariablesOnlyInUpdateProbabilities(std::set const& undefinedConstantVariables) const { for (auto const& booleanVariable : this->getBooleanVariables()) { diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index adeb94e01..803e5240b 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -251,8 +251,22 @@ namespace storm { */ Module substitute(std::map const& substitution) const; + /** + * Nonstandard predicates such as ExacltyOneOff etc can be substituted + * @return + */ Module substituteNonStandardPredicates() const; + /** + * Label unlabelled commands. + * + * @param suggestions Map from global index to names that is used to label unlabelled commands + * @param newId The new action ids to use are given sequentially from this number onwards (and the argument is updated) + * @param nameToIdMapping A mapping that is updated giving action indices to used names + * @return + */ + Module labelUnlabelledCommands(std::map const& suggestions, uint64_t& newId, std::map& nameToIdMapping) const; + /*! * Checks whether the given variables only appear in the update probabilities of the module and nowhere else. * diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index ca17bf607..8cfb8d991 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -892,7 +892,6 @@ namespace storm { Module const& module = this->getModule(moduleIndex); for (auto const& actionIndex : module.getSynchronizingActionIndices()) { - auto const& actionModuleIndicesPair = this->actionIndicesToModuleIndexMap.find(actionIndex); this->actionIndicesToModuleIndexMap[actionIndex].insert(moduleIndex); } @@ -1070,6 +1069,36 @@ namespace storm { return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(), newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility); } + Program Program::labelUnlabelledCommands(std::map const& nameSuggestions) const { + for (auto const& entry : nameSuggestions) { + STORM_LOG_THROW(!hasAction(entry.second), storm::exceptions::InvalidArgumentException, "Cannot suggest names already in the program."); + } + std::vector newModules; + std::vector newRewardModels; + std::map newActionNameToIndexMapping = getActionNameToIndexMapping(); + + uint64_t oldId = 1; + if (!getSynchronizingActionIndices().empty()) { + oldId = *(getSynchronizingActionIndices().rbegin()) + 1; + } + uint64_t newId = oldId; + for (auto const& module : modules) { + newModules.push_back(module.labelUnlabelledCommands(nameSuggestions, newId, newActionNameToIndexMapping)); + } + + std::vector> newActionNames; + for (auto const& entry : newActionNameToIndexMapping) { + if(!hasAction(entry.first)) { + newActionNames.emplace_back(entry.second, entry.first); + } + } + for (auto const& rewardModel : rewardModels) { + newRewardModels.push_back(rewardModel.labelUnlabelledCommands(newActionNames)); + } + + return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getPlayers(), newModules, newActionNameToIndexMapping, newRewardModels, this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility); + } + void Program::checkValidity(Program::ValidityCheckLevel lvl) const { // Start by checking the constant declarations. diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 697eb9e0f..e49925d5e 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -703,6 +703,10 @@ namespace storm { */ Program flattenModules(std::shared_ptr const& smtSolverFactory = std::shared_ptr(new storm::utility::solver::SmtSolverFactory())) const; + + Program labelUnlabelledCommands(std::map const& nameSuggestions) const; + + friend std::ostream& operator<<(std::ostream& stream, Program const& program); /*! diff --git a/src/storm/storage/prism/RewardModel.cpp b/src/storm/storage/prism/RewardModel.cpp index 96767a17d..61281529d 100644 --- a/src/storm/storage/prism/RewardModel.cpp +++ b/src/storm/storage/prism/RewardModel.cpp @@ -98,7 +98,28 @@ namespace storm { return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber()); } - + + RewardModel RewardModel::labelUnlabelledCommands(std::vector> const& newActions) const { + std::vector newStateActionRewards; + std::vector newTransitionRewards; + + for (auto const& reward : getStateActionRewards()) { + if(reward.getActionIndex() == 0) { + for (auto const& newAction : newActions) { + newStateActionRewards.emplace_back(newAction.first, newAction.second, reward.getStatePredicateExpression(), reward.getRewardValueExpression(), reward.getFilename(), reward.getLineNumber()); + } + } else { + newStateActionRewards.push_back(reward); + } + } + + assert(transitionRewards.empty()); // Not implemented. + + + return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber()); + } + + std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) { stream << "rewards"; if (rewardModel.getName() != "") { diff --git a/src/storm/storage/prism/RewardModel.h b/src/storm/storage/prism/RewardModel.h index c47b310c5..2ed2ce90b 100644 --- a/src/storm/storage/prism/RewardModel.h +++ b/src/storm/storage/prism/RewardModel.h @@ -97,7 +97,9 @@ namespace storm { * @return The resulting reward model. */ RewardModel substitute(std::map const& substitution) const; - + + RewardModel labelUnlabelledCommands(std::vector> const& newActionNames) const; + /*! * Checks whether any of the given variables only appear in the expressions defining the reward value. *