worked on human readable representations of prism command sets

src/storm/generator/PrismNextStateGenerator.cpp

@@ -14,6 +14,7 @@
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/WrongFormatException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace generator {
@@ -636,8 +637,47 @@ namespace storm {
             std::vector<std::string> identifierToInfoMapping(currentIdentifier);
             for (auto const& setIdPair : commandSetToIdentifierMap) {
                 identifierToCommandSetMapping[setIdPair.second] = setIdPair.first;
-                // Todo: Make these identifiers unique
-                identifierToInfoMapping[setIdPair.second] = "Choice made from " + std::to_string(setIdPair.first.size()) + " commands";
+                
+                // Get a string representation of this command set.
+                std::stringstream commandSetName;
+                if (setIdPair.first.empty()) {
+                    commandSetName << "No origin";
+                } else {
+                    //process the first command in the set
+                    auto commandIndexIt = setIdPair.first.begin();
+                    std::string actionName;
+                    auto moduleCommandPair = program.getModuleCommandIndexByGlobalCommandIndex(*commandIndexIt);
+                    storm::prism::Module const& firstModule = program.getModule(moduleCommandPair.first);
+                    storm::prism::Command const& firstCommand = firstModule.getCommand(moduleCommandPair.second);
+                    actionName = firstCommand.getActionName();
+                    commandSetName << actionName;
+                    bool commandSetHasModuleDetails = false;
+                    if (firstModule.getCommandIndicesByActionIndex(firstCommand.getActionIndex()).size() != 1) {
+                        commandSetHasModuleDetails = true;
+                        commandSetName << " (" << firstModule.getName() << ": " << firstCommand;
+                    }
+                    
+                    // now process the remaining commands
+                    for (; commandIndexIt != setIdPair.first.end(); ++commandIndexIt) {
+                        moduleCommandPair = program.getModuleCommandIndexByGlobalCommandIndex(*commandIndexIt);
+                        storm::prism::Module const& module = program.getModule(moduleCommandPair.first);
+                        storm::prism::Command const& command = module.getCommand(moduleCommandPair.second);
+                        STORM_LOG_THROW(command.getActionName() == actionName, storm::exceptions::UnexpectedException, "Inconsistent action names for choice origin");
+                        if (module.getCommandIndicesByActionIndex(command.getActionIndex()).size() != 1) {
+                            if (commandSetHasModuleDetails) {
+                                commandSetName << "    ";
+                            } else {
+                                commandSetHasModuleDetails = true;
+                                commandSetName << " (";
+                            }
+                            commandSetName << module.getName() << ": " << command;
+                        }
+                    }
+                    if (commandSetHasModuleDetails) {
+                        commandSetName << ")";
+                    }
+                }
+                identifierToInfoMapping[setIdPair.second] = commandSetName.str();
             }
             
             return std::make_shared<storm::storage::sparse::PrismChoiceOrigins>(std::make_shared<storm::prism::Program>(program), std::move(identifiers), std::move(identifierToInfoMapping), std::move(identifierToCommandSetMapping));

src/storm/storage/prism/Program.cpp

@@ -566,6 +566,23 @@ namespace storm {
             return variableNameToModuleIndexPair->second;
         }
         
+        std::pair<uint_fast64_t, uint_fast64_t> Program::getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const {
+            uint_fast64_t moduleIndex = 0;
+            for (auto const& module : modules) {
+                uint_fast64_t commandIndex = 0;
+                for (auto const& command : module.getCommands()) {
+                    if (command.getGlobalIndex() == globalCommandIndex) {
+                        return std::pair<uint_fast64_t, uint_fast64_t>(moduleIndex, commandIndex);
+                    }
+                    ++commandIndex;
+                }
+                ++moduleIndex;
+            }
+            // This point should not be reached if the globalCommandIndex is valid
+            STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Global command index '" << globalCommandIndex << "' does not exist.");
+            return std::pair<uint_fast64_t, uint_fast64_t>(0, 0);
+        }
+        
         bool Program::hasRewardModel() const {
             return !this->rewardModels.empty();
         }

src/storm/storage/prism/Program.h

@@ -409,6 +409,19 @@ namespace storm {
              */
             uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
             
+            /*!
+             * Retrieves the index of the module and the (local) index of the command with the given global command index.
+             *
+             * An exception is thrown if the command index is invalid.
+             *
+             * @note if (x,y) is the result of this method, we have
+             * <code> getModule(x).getCommand(y).getGlobalIndex() == globalCommandIndex </code>
+             *
+             * @param globalCommandIndex the global command index specifying the command that is to be found
+             * @return the index of the module and the (local) index of the found command
+             */
+            std::pair<uint_fast64_t, uint_fast64_t> getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const;
+            
             /*!
              * Retrieves whether the program has reward models.
              *