From 52cd48c247d174febad28c979d99fb8127998efd Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 23 Mar 2014 17:19:39 +0100
Subject: [PATCH] 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: 6bbb4b807cbe6ed7f005a0b645c5a3b094854d20
---
 src/adapters/ExplicitModelAdapter.h |  7 +++++++
 src/ir/Module.cpp                   | 17 +++++++++++++++++
 src/ir/Module.h                     |  6 +-----
 3 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index a2932b9c9..f1ef50396 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/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.
diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp
index 6b67ee579..5724db8df 100644
--- a/src/ir/Module.cpp
+++ b/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
diff --git a/src/ir/Module.h b/src/ir/Module.h
index e6762bb8d..d9570c652 100644
--- a/src/ir/Module.h
+++ b/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