label unlabelled commands

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<uint64_t, std::string> const& suggestions, uint64_t& newId, std::map<std::string, uint64_t>& nameToIdMapping) const {
+            std::vector<Command> 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<storm::expressions::Variable> const& undefinedConstantVariables) const {
             for (auto const& booleanVariable : this->getBooleanVariables()) {

src/storm/storage/prism/Module.h

@@ -251,8 +251,22 @@ namespace storm {
              */
             Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> 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<uint64_t, std::string> const& suggestions, uint64_t& newId, std::map<std::string, uint64_t>& nameToIdMapping) const;
+
             /*!
              * Checks whether the given variables only appear in the update probabilities of the module and nowhere else.
              *

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<uint64_t, std::string> 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<Module> newModules;
+            std::vector<RewardModel> newRewardModels;
+            std::map<std::string, uint64_t> 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<std::pair<uint64_t, std::string>> 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.

src/storm/storage/prism/Program.h

@@ -703,6 +703,10 @@ namespace storm {
              */
             Program flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::shared_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory())) const;
 
+
+            Program labelUnlabelledCommands(std::map<uint64_t,std::string> const& nameSuggestions) const;
+
+
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
 
             /*!

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<std::pair<uint64_t, std::string>> const& newActions) const {
+            std::vector<StateActionReward> newStateActionRewards;
+            std::vector<TransitionReward> 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() != "") {

src/storm/storage/prism/RewardModel.h

@@ -97,7 +97,9 @@ namespace storm {
              * @return The resulting reward model.
              */
             RewardModel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
-            
+
+            RewardModel labelUnlabelledCommands(std::vector<std::pair<uint64_t, std::string>> const& newActionNames) const;
+
             /*!
              * Checks whether any of the given variables only appear in the expressions defining the reward value.
              *