Started improving performance of explicit model generation.

Former-commit-id: 318a97aedc

src/adapters/ExplicitModelAdapter.h

@@ -230,10 +230,10 @@ namespace storm {
              *
              * @param The program in which to search for active commands.
              * @param state The current state.
-             * @param action The action label to select.
+             * @param actionIndex The index of the action label to select.
              * @return A list of lists of active commands or nothing.
              */
-            static boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByAction(storm::prism::Program const& program, StateType const* state, std::string const& action) {
+            static boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> getActiveCommandsByAction(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) {
                 boost::optional<std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::list<std::reference_wrapper<storm::prism::Command const>>>()));
                 
                 // Iterate over all modules.
@@ -241,11 +241,11 @@ namespace storm {
                     storm::prism::Module const& module = program.getModule(i);
                     
                     // If the module has no command labeled with the given action, we can skip this module.
-                    if (!module.hasAction(action)) {
+                    if (!module.hasActionIndex(actionIndex)) {
                         continue;
                     }
                     
-                    std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByAction(action);
+                    std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
                     
                     // 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.
@@ -288,7 +288,7 @@ namespace storm {
                         storm::prism::Command const& command = module.getCommand(j);
                         
                         // Only consider unlabeled commands.
-                        if (command.getActionName() != "") continue;
+                        if (!command.isLabeled()) continue;
 
                         // Skip the command, if it is not enabled.
                         if (!command.getGuardExpression().evaluateAsBool(currentState)) {
@@ -538,7 +538,7 @@ namespace storm {
                                     
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                        if (!transitionReward.empty() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
                                             stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }
@@ -551,7 +551,7 @@ namespace storm {
                                 
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                        if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
                                             stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }
@@ -589,7 +589,7 @@ namespace storm {
                                     
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                        if (!transitionReward.isLabeled() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
                                             stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }
@@ -616,7 +616,7 @@ namespace storm {
                                     
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                        if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
                                             stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }

src/parser/PrismParser.cpp

@@ -139,7 +139,7 @@ namespace storm {
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";
             updateListDefinition.name("update list");
             
-            commandDefinition = qi::lit("[") > +(qi::char_ - qi::lit(";")) > qi::lit(";")[qi::_val = phoenix::construct<storm::prism::Command>()];
+            commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > +(qi::char_ - qi::lit(";")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_r1)];
             commandDefinition.name("command definition");
             
             moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
@@ -355,7 +355,21 @@ namespace storm {
         
         storm::prism::Command PrismParser::createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const {
             ++globalProgramInformation.currentCommandIndex;
-            return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, actionName, guardExpression, updates, this->getFilename());
+            return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename());
+        }
+        
+        storm::prism::Command PrismParser::createCommand(std::string const& actionName, GlobalProgramInformation& globalProgramInformation) const {
+            STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run.");
+            
+            if (!actionName.empty()) {
+                // Register the action name if it has not appeared earlier.
+                auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
+                if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
+                    globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size();
+                }
+            }
+            
+            return storm::prism::Command();
         }
         
         storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
@@ -474,7 +488,12 @@ namespace storm {
                         newActionName = renamingPair->second;
                     }
                     
-                    commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
+                    auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
+                    if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
+                        globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size();
+                    }
+                    
+                    commands.emplace_back(globalProgramInformation.currentCommandIndex, globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
                     ++globalProgramInformation.currentCommandIndex;
                 }
                 

src/parser/PrismParser.h

@@ -21,7 +21,7 @@ namespace storm {
         class GlobalProgramInformation {
         public:
             // Default construct the header information.
-            GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) {
+            GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), actionIndices(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) {
                 // Intentionally left empty.
             }
             
@@ -32,6 +32,7 @@ namespace storm {
             std::vector<storm::prism::BooleanVariable> globalBooleanVariables;
             std::vector<storm::prism::IntegerVariable> globalIntegerVariables;
             std::map<std::string, uint_fast64_t> moduleToIndexMap;
+            std::map<std::string, uint_fast64_t> actionIndices;
             std::vector<storm::prism::Module> modules;
             std::vector<storm::prism::RewardModel> rewardModels;
             std::vector<storm::prism::Label> labels;
@@ -235,6 +236,7 @@ namespace storm {
             storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const;
             storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const;
+            storm::prism::Command createCommand(std::string const& actionName, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::BooleanVariable createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const;
             storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const;
             storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;

src/storage/expressions/Valuation.h

@@ -3,6 +3,7 @@
 
 #include <cstdint>
 #include <vector>
+#include <memory>
 
 namespace storm {
     namespace expressions {

src/storage/prism/Command.cpp

@@ -2,10 +2,14 @@
 
 namespace storm {
     namespace prism {
-        Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) {
+        Command::Command(uint_fast64_t globalIndex, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex), labeled(actionName != "") {
             // Nothing to do here.
         }
 
+        uint_fast64_t Command::getActionIndex() const {
+            return this->actionIndex;
+        }
+        
         std::string const& Command::getActionName() const {
             return this->actionName;
         }
@@ -37,7 +41,11 @@ namespace storm {
                 newUpdates.emplace_back(update.substitute(substitution));
             }
             
-            return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber());
+            return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber());
+        }
+        
+        bool Command::isLabeled() const {
+            return labeled;
         }
         
         std::ostream& operator<<(std::ostream& stream, Command const& command) {

src/storage/prism/Command.h

@@ -17,18 +17,19 @@ namespace storm {
              * Creates a command with the given action name, guard and updates.
              *
              * @param globalIndex The global index of the command.
+             * @param actionIndex The index of the action of the command.
              * @param actionName The action name of the command.
              * @param guardExpression the expression that defines the guard of the command.
              * @param updates A list of updates that is associated with this command.
              * @param filename The filename in which the command is defined.
              * @param lineNumber The line number in which the command is defined.
              */
-            Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Command(uint_fast64_t globalIndex, uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             // Create default implementations of constructors/assignment.
             Command() = default;
             Command(Command const& other) = default;
-            Command& operator=(Command const& other)= default;
+            Command& operator=(Command const& other) = default;
 #ifndef WINDOWS
             Command(Command&& other) = default;
             Command& operator=(Command&& other) = default;
@@ -41,6 +42,13 @@ namespace storm {
              */
             std::string const& getActionName() const;
             
+            /*!
+             * Retrieves the action index of this command.
+             *
+             * @return The action index of the command.
+             */
+            uint_fast64_t getActionIndex() const;
+            
             /*!
              * Retrieves a reference to the guard of the command.
              *
@@ -84,9 +92,19 @@ namespace storm {
              */
             Command substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             
+            /*!
+             * Retrieves whether the command possesses a synchronization label.
+             *
+             * @return True iff the command is labeled.
+             */
+            bool isLabeled() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Command const& command);
             
         private:
+            //  The index of the action associated with this command.
+            uint_fast64_t actionIndex;
+
             // The name of the command.
             std::string actionName;
             
@@ -98,6 +116,9 @@ namespace storm {
             
             // The global index of the command.
             uint_fast64_t globalIndex;
+            
+            // A flag indicating whether the command is labeled.
+            bool labeled;
         };
         
     } // namespace prism

src/storage/prism/Module.cpp

@@ -10,7 +10,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
+        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionIndices(), actionsToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
             // Initialize the internal mappings for fast information retrieval.
             this->createMappings();
         }
@@ -76,6 +76,10 @@ namespace storm {
             return actionEntry != this->actions.end();
         }
         
+        bool Module::hasActionIndex(uint_fast64_t const& actionIndex) const {
+            return this->actionIndices.find(actionIndex) != this->actionIndices.end();
+        }
+        
         bool Module::isRenamedFromModule() const {
             return this->renamedFromModule != "";
         }
@@ -99,9 +103,19 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module.");
         }
         
+        std::set<uint_fast64_t> const& Module::getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const {
+            auto actionIndicesCommandSetPair = this->actionIndicesToCommandIndexMap.find(actionIndex);
+            if (actionIndicesCommandSetPair != this->actionIndicesToCommandIndexMap.end()) {
+                return actionIndicesCommandSetPair->second;
+            }
+            
+            STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action index '" << actionIndex << "' does not exist in module.");
+        }
+        
         void Module::createMappings() {
             // Clear the current mappings.
             this->actionsToCommandIndexMap.clear();
+            this->actionIndicesToCommandIndexMap.clear();
             this->booleanVariableToIndexMap.clear();
             this->integerVariableToIndexMap.clear();
             
@@ -116,12 +130,19 @@ namespace storm {
             // Add the mapping for all commands.
             for (uint_fast64_t i = 0; i < this->commands.size(); i++) {
                 std::string const& action = this->commands[i].getActionName();
+                uint_fast64_t actionIndex = this->commands[i].getActionIndex();
                 if (action != "") {
                     if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) {
                         this->actionsToCommandIndexMap.emplace(action, std::set<uint_fast64_t>());
                     }
+                    if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
+                        this->actionIndicesToCommandIndexMap.emplace(actionIndex, std::set<uint_fast64_t>());
+                    }
                     this->actionsToCommandIndexMap[action].insert(i);
+                    this->actionIndicesToCommandIndexMap[actionIndex].insert(i);
+                    
                     this->actions.insert(action);
+                    this->actionIndices.insert(this->commands[i].getActionIndex());
                 }
             }
             
@@ -132,6 +153,11 @@ namespace storm {
                     this->actionsToCommandIndexMap[action] = std::set<uint_fast64_t>();
                 }
             }
+            for (auto const& actionIndex : this->actionIndices) {
+                if (this->actionIndicesToCommandIndexMap.find(actionIndex) == this->actionIndicesToCommandIndexMap.end()) {
+                    this->actionIndicesToCommandIndexMap[actionIndex] = std::set<uint_fast64_t>();
+                }
+            }
         }
         
         Module Module::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const {

src/storage/prism/Module.h

@@ -148,6 +148,14 @@ namespace storm {
              * @return True iff the module has at least one command labeled with the given action.
              */
             bool hasAction(std::string const& action) const;
+
+            /*!
+             * Retrieves whether or not this module contains a command labeled with the given action index.
+             *
+             * @param action The action name to look for in this module.
+             * @return True iff the module has at least one command labeled with the given action index.
+             */
+            bool hasActionIndex(uint_fast64_t const& actionIndex) const;
             
             /*!
              * Retrieves whether this module was created from another module via renaming.
@@ -180,6 +188,14 @@ namespace storm {
              */
             std::set<uint_fast64_t> const& getCommandIndicesByAction(std::string const& action) const;
             
+            /*!
+             * Retrieves the indices of all commands within this module that are labelled by the given action.
+             *
+             * @param actionIndex The index of the action with which the commands have to be labelled.
+             * @return A set of indices of commands that are labelled with the given action index.
+             */
+            std::set<uint_fast64_t> const& getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const;
+            
             /*!
              * Creates a new module that drops all commands whose indices are not in the given set.
              *
@@ -225,8 +241,14 @@ namespace storm {
             // The set of actions present in this module.
             std::set<std::string> actions;
             
+            // The set of action indices present in this module.
+            std::set<uint_fast64_t> actionIndices;
+            
             // A map of actions to the set of commands labeled with this action.
             std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
+
+            // A map of actions to the set of commands labeled with this action.
+            std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToCommandIndexMap;
             
             // This string indicates whether and from what module this module was created via renaming.
             std::string renamedFromModule;