Fixed bug in restriction of a program to certain commands. Also, modules may now have an action without actually having a command labeled with the action and the explicit model adapter now handles this correctly.

Former-commit-id: 6bbb4b807c

src/adapters/ExplicitModelAdapter.h

@@ -233,6 +233,13 @@ namespace storm {
                     }
                     
                     std::set<uint_fast64_t> const& commandIndices = module.getCommandsByAction(action);
+                    
+                    // If the module contains the action, but there is no command in the module that is labeled with
+                    // this action, we don't have any feasible command combinations.
+                    if (commandIndices.empty()) {
+                        return boost::optional<std::vector<std::list<storm::ir::Command>>>();
+                    }
+                    
                     std::list<storm::ir::Command> commands;
                     
                     // Look up commands by their indices and add them if the guard evaluates to true in the given state.

src/ir/Module.cpp

@@ -169,11 +169,16 @@ namespace storm {
             if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {
                 return actionsCommandSetPair->second;
             }
+            
             LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module.");
             throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module.";
         }
         
         void Module::collectActions() {
+            // Clear the current mapping.
+            this->actionsToCommandIndexMap.clear();
+            
+            // Add the mapping for all commands.
             for (unsigned int id = 0; id < this->commands.size(); id++) {
                 std::string const& action = this->commands[id].getActionName();
                 if (action != "") {
@@ -184,9 +189,18 @@ namespace storm {
                     this->actions.insert(action);
                 }
             }
+            
+            // For all actions that are "in the module", but for which no command exists, we add the mapping to an empty
+            // set of commands.
+            for (auto const& action : this->actions) {
+                if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) {
+                    this->actionsToCommandIndexMap[action] = std::set<uint_fast64_t>();
+                }
+            }
         }
         
         void Module::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) {
+            // First construct the new vector of commands.
             std::vector<storm::ir::Command> newCommands;
             for (auto const& command : commands) {
                 if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) {
@@ -194,6 +208,9 @@ namespace storm {
                 }
             }
             commands = std::move(newCommands);
+            
+            // Then refresh the internal mappings.
+            this->collectActions();
         }
         
     } // namespace ir

src/ir/Module.h

@@ -188,8 +188,8 @@ namespace storm {
              * @param indexSet The set of indices for which to keep the commands.
              */
             void restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet);
-        private:
             
+        private:
             /*!
              * Computes the locally maintained mappings for fast data retrieval.
              */
@@ -217,11 +217,7 @@ namespace storm {
             std::set<std::string> actions;
             
             // A map of actions to the set of commands labeled with this action.
-#ifdef LINUX
-            boost::container::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
-#else
             std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
-#endif
         };
         
     } // namespace ir