moved building the choice origin strings into the ChoiceOrigins class

src/storm/generator/PrismNextStateGenerator.cpp

@@ -634,53 +634,11 @@ namespace storm {
             }
             
             std::vector<CommandSet> identifierToCommandSetMapping(currentIdentifier);
-            std::vector<std::string> identifierToInfoMapping(currentIdentifier);
             for (auto const& setIdPair : commandSetToIdentifierMap) {
                 identifierToCommandSetMapping[setIdPair.second] = setIdPair.first;
-                
-                // 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));
+            return std::make_shared<storm::storage::sparse::PrismChoiceOrigins>(std::make_shared<storm::prism::Program>(program), std::move(identifiers), std::move(identifierToCommandSetMapping));
         }
 
                 

src/storm/models/sparse/ItemLabeling.cpp

@@ -41,6 +41,17 @@ namespace storm {
                 addLabel(label, storage::BitVector(itemCount));
             }
 
+            void ItemLabeling::join(ItemLabeling const& other) {
+                STORM_LOG_THROW(this->itemCount == other.itemCount, storm::exceptions::InvalidArgumentException, "The item count of the two labelings does not match: " << this->itemCount << " vs. " << other.itemCount << ".");
+                for (auto const& label : other.getLabels()) {
+                    if (this->containsLabel(label)) {
+                        this->setItems(label, this->getItems(label) | other.getItems(label));
+                    } else {
+                        this->addLabel(label, other.getItems(label));
+                    }
+                }
+            }
+            
             std::set<std::string> ItemLabeling::getLabels() const {
                 std::set<std::string> result;
                 for (auto const& labelIndexPair : this->nameToLabelingIndexMap) {

src/storm/models/sparse/ItemLabeling.h

@@ -54,8 +54,6 @@ namespace storm {
                  */
                 std::set<std::string> getLabels() const;
 
-
-
                 /*!
                  * Creates a new label and attaches it to the given items. Note that the dimension of given labeling must
                  * match the number of items for which this item labeling is valid.
@@ -74,6 +72,13 @@ namespace storm {
                  */
                 void addLabel(std::string const& label, storage::BitVector&& labeling);
 
+                /*!
+                 * Adds all labels from the other labeling to this labeling.
+                 * It is assumed that both labelings have the same itemcount.
+                 * If a label is present in both labellings, we take the union of the corresponding item sets.
+                 */
+                 void join(ItemLabeling const& other);
+                
                 /*!
                  * Checks whether a label is registered within this labeling.
                  *

src/storm/storage/sparse/ChoiceOrigins.cpp

@@ -4,16 +4,17 @@
 #include "storm/storage/sparse/JaniChoiceOrigins.h"
 #include "storm/utility/vector.h"
 
+#include "storm/utility/macros.h"
 
 namespace storm {
     namespace storage {
         namespace sparse {
             
-            ChoiceOrigins::ChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping) : indexToIdentifier(indexToIdentifierMapping), identifierToInfo(identifierToInfoMapping) {
+            ChoiceOrigins::ChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping) : indexToIdentifier(indexToIdentifierMapping) {
                 // Intentionally left empty
             }
             
-            ChoiceOrigins::ChoiceOrigins(std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping) : indexToIdentifier(std::move(indexToIdentifierMapping)), identifierToInfo(std::move(identifierToInfoMapping)) {
+            ChoiceOrigins::ChoiceOrigins(std::vector<uint_fast64_t>&& indexToIdentifierMapping) : indexToIdentifier(std::move(indexToIdentifierMapping)) {
                 // Intentionally left empty
             }
             
@@ -42,6 +43,7 @@ namespace storm {
             }
             			    
             uint_fast64_t ChoiceOrigins::getIdentifier(uint_fast64_t choiceIndex) const {
+                STORM_LOG_ASSERT(choiceIndex < indexToIdentifier.size(), "Invalid choice index: " << choiceIndex);
             	return  indexToIdentifier[choiceIndex];
             }
             
@@ -50,6 +52,10 @@ namespace storm {
 			}
                 
 			std::string const& ChoiceOrigins::getIdentifierInfo(uint_fast64_t identifier) const {
+                STORM_LOG_ASSERT(identifier <= this->getLargestIdentifier(), "Invalid choice origin identifier: " << identifier);
+                if (identifierToInfo.empty()) {
+                    computeIdentifierInfos();
+                }
 				return identifierToInfo[identifier];
 			}
                 
@@ -75,6 +81,17 @@ namespace storm {
                 }
                 return cloneWithNewIndexToIdentifierMapping(std::move(indexToIdentifierMapping));
             }
+                         
+            storm::models::sparse::ChoiceLabeling ChoiceOrigins::toChoiceLabeling() const {
+                storm::models::sparse::ChoiceLabeling result(indexToIdentifier.size());
+                for (uint_fast64_t identifier = 0; identifier <= this->getLargestIdentifier(); ++identifier) {
+                    storm::storage::BitVector choicesWithIdentifier = storm::utility::vector::filter<uint_fast64_t>(indexToIdentifier, [&identifier](uint_fast64_t i) -> bool { return i == identifier;});
+                    if (!choicesWithIdentifier.empty()) {
+                        result.addLabel(getIdentifierInfo(identifier), std::move(choicesWithIdentifier));
+                    }
+                }
+                return result;
+            }
         }
     }
 }

src/storm/storage/sparse/ChoiceOrigins.h

@@ -3,6 +3,8 @@
 #include <vector>
 #include <string>
 #include "storm/storage/BitVector.h"
+#include "storm/models/sparse/ChoiceLabeling.h"
+
 
 namespace storm {
     namespace storage {
@@ -34,6 +36,11 @@ namespace storm {
                  */
                 uint_fast64_t getIdentifier(uint_fast64_t choiceIndex) const;
                 
+                /*
+                 * Returns the largest identifier that is used by this object.
+                 * This can be used to, e.g., loop over all identifiers.
+                 */
+                virtual uint_fast64_t getLargestIdentifier() const = 0;
                 /*
                  * Returns the identifier that is used for choices without an origin in the input specification
                  * E.g., Selfloops introduced on deadlock states
@@ -50,21 +57,36 @@ namespace storm {
                  */
                 std::string const& getChoiceInfo(uint_fast64_t choiceIndex) const;
                 
-                
+                /*
+                 * Derive new choice origins from this by selecting the given choices.
+                 */
                 std::shared_ptr<ChoiceOrigins> selectChoices(storm::storage::BitVector const& selectedChoices) const;
+                
+                /*
+                 * Derive new choice origins from this by selecting the given choices.
+                 * If an invalid choice index is selected, the corresponding choice will get the identifier for choices with no origin.
+                 */
                 std::shared_ptr<ChoiceOrigins> selectChoices(std::vector<uint_fast64_t> const& selectedChoiceIndices) const;
+                
+                storm::models::sparse::ChoiceLabeling toChoiceLabeling() const;
 
             protected:
-                ChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping);
-                ChoiceOrigins(std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping);
+                ChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping);
+                ChoiceOrigins(std::vector<uint_fast64_t>&& indexToIdentifierMapping);
                 
                 /*
                  * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one.
                  */
                 virtual std::shared_ptr<ChoiceOrigins> cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const = 0;
                 
-                std::vector<uint_fast64_t> indexToIdentifier;
-                std::vector<std::string> identifierToInfo;
+                /*
+                 * Computes the identifier infos (i.e., human readable strings representing the choice origins).
+                 */
+                virtual void computeIdentifierInfos() const = 0;
+                
+                std::vector<uint_fast64_t> const indexToIdentifier;
+                mutable std::vector<std::string> identifierToInfo;
+
             };
         }
     }

src/storm/storage/sparse/JaniChoiceOrigins.cpp

@@ -1,21 +1,30 @@
 #include "storm/storage/sparse/JaniChoiceOrigins.h"
 
+#include "storm/utility/macros.h"
 
 namespace storm {
     namespace storage {
         namespace sparse {
             
-            JaniChoiceOrigins::JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping) : ChoiceOrigins(indexToIdentifierMapping, identifierToInfoMapping) {
+            JaniChoiceOrigins::JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping) : ChoiceOrigins(indexToIdentifierMapping) {
 				// Intentionally left empty
+                STORM_LOG_ASSERT(false, "Jani choice origins not properly implemented");
 			}
 
             bool JaniChoiceOrigins::isJaniChoiceOrigins() const  {
             	return true;
             }
+            
+            uint_fast64_t JaniChoiceOrigins::getLargestIdentifier() const {
+                return 0;
+            }
              
             std::shared_ptr<ChoiceOrigins> JaniChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const {
-                std::vector<std::string> identifierToInfoMapping = this->identifierToInfo;
-                return std::make_shared<JaniChoiceOrigins>(std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping));
+                return std::make_shared<JaniChoiceOrigins>(std::move(indexToIdentifierMapping));
+            }
+            
+            void JaniChoiceOrigins::computeIdentifierInfos() const {
+                
             }
             
         }

src/storm/storage/sparse/JaniChoiceOrigins.h

@@ -13,25 +13,36 @@ namespace storm {
             
             /*!
              * This class represents for each choice the origin in the jani specification
+             * // TODO complete this
              */
             class JaniChoiceOrigins : public ChoiceOrigins {
             public:
                 
                 /*!
                  * Creates a new representation of the choice indices to their origin in the Jani specification
-                 * // TODO complete this
                  */
-                JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping);
+                JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping);
                 
                 virtual ~JaniChoiceOrigins() = default;
                 
                 virtual bool isJaniChoiceOrigins() const override ;
                 
+                /*
+                 * Returns the largest identifier that is used by this object.
+                 * This can be used to, e.g., loop over all identifiers.
+                 */
+                virtual uint_fast64_t getLargestIdentifier() const override;
+                
                 /*
                  * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one.
                  */
                 virtual std::shared_ptr<ChoiceOrigins> cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const override;
                 
+                /*
+                 * Computes the identifier infos (i.e., human readable strings representing the choice origins).
+                 */
+                virtual void computeIdentifierInfos() const override;
+                
             private:
                 
             };

src/storm/storage/sparse/PrismChoiceOrigins.cpp

@@ -1,17 +1,20 @@
 #include "storm/storage/sparse/PrismChoiceOrigins.h"
 
 #include "storm/utility/macros.h"
+#include "storm/utility/vector.h"
+
+#include "storm/exceptions/UnexpectedException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace storage {
         namespace sparse {
             
-            PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping, std::vector<CommandSet> const& identifierToCommandSetMapping) : ChoiceOrigins(indexToIdentifierMapping, identifierToInfoMapping), program(prismProgram), identifierToCommandSet(identifierToCommandSetMapping) {
+            PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<CommandSet> const& identifierToCommandSetMapping) : ChoiceOrigins(indexToIdentifierMapping), program(prismProgram), identifierToCommandSet(identifierToCommandSetMapping) {
                 STORM_LOG_THROW(identifierToCommandSet[this->getIdentifierForChoicesWithNoOrigin()].empty(), storm::exceptions::InvalidArgumentException, "The given command set for the choices without origin is non-empty");
 			}
 
-            PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping, std::vector<CommandSet>&& identifierToCommandSetMapping) : ChoiceOrigins(std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping)), program(prismProgram), identifierToCommandSet(std::move(identifierToCommandSetMapping)) {
+            PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<CommandSet>&& identifierToCommandSetMapping) : ChoiceOrigins(std::move(indexToIdentifierMapping)), program(prismProgram), identifierToCommandSet(std::move(identifierToCommandSetMapping)) {
                 STORM_LOG_THROW(identifierToCommandSet[this->getIdentifierForChoicesWithNoOrigin()].empty(), storm::exceptions::InvalidArgumentException, "The given command set for the choices without origin is non-empty");
             }
                 
@@ -19,6 +22,10 @@ namespace storm {
             	return true;
             }
              
+            uint_fast64_t PrismChoiceOrigins::getLargestIdentifier() const {
+                return identifierToCommandSet.size();
+            }
+            
             storm::prism::Program const& PrismChoiceOrigins::getProgram() const {
             	return *program;
             }
@@ -29,11 +36,78 @@ namespace storm {
             
             std::shared_ptr<ChoiceOrigins> PrismChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const {
                 std::vector<CommandSet> identifierToCommandSetMapping = this->identifierToCommandSet;
-                std::vector<std::string> identifierToInfoMapping = this->identifierToInfo;
-                return std::make_shared<PrismChoiceOrigins>(this->program, std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping), std::move(identifierToCommandSetMapping));
+                auto result = std::make_shared<PrismChoiceOrigins>(this->program, std::move(indexToIdentifierMapping), std::move(identifierToCommandSetMapping));
+                result->identifierToInfo = this->identifierToInfo;
+                return result;
             }
 
-            
+            void PrismChoiceOrigins::computeIdentifierInfos() const {
+                this->identifierToInfo.clear();
+                this->identifierToInfo.reserve(this->getLargestIdentifier() + 1);
+                for (CommandSet const& set : identifierToCommandSet) {
+                    // Get a string representation of this command set.
+                    std::stringstream setName;
+                    if (set.empty()) {
+                        setName << "No origin";
+                    } else {
+                        //process the first command in the set
+                        auto commandIndexIt = set.begin();
+                        auto moduleCommandPair = program->getModuleCommandIndexByGlobalCommandIndex(*commandIndexIt);
+                        storm::prism::Module const& firstModule = program->getModule(moduleCommandPair.first);
+                        storm::prism::Command const& firstCommand = firstModule.getCommand(moduleCommandPair.second);
+                        
+                        std::string actionName = firstCommand.getActionName();
+                        setName << actionName;
+                        
+                        // If the commands are labeled, it is clear which modules induced the current choice.
+                        // In this case, we only need to print more information if there are multiple commands in a module with the same label.
+                        bool setNameNeedsAllModuleNames = !firstCommand.isLabeled();
+                        bool actionNameIsUniqueInModule = firstModule.getCommandIndicesByActionIndex(firstCommand.getActionIndex()).size() != 1;
+                        
+                        bool setNameHasModuleDetails = false;
+                        if (!actionNameIsUniqueInModule || setNameNeedsAllModuleNames) {
+                            setNameHasModuleDetails = true;
+                            if (!actionName.empty()) {
+                                setName << " ";
+                            }
+                            setName << "(" << firstModule.getName();
+                            if (!actionNameIsUniqueInModule) {
+                                setName << ": " << firstCommand;
+                            }
+                        }
+                    
+                        // now process the remaining commands
+                        for (; commandIndexIt != set.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");
+
+                            actionNameIsUniqueInModule = module.getCommandIndicesByActionIndex(command.getActionIndex()).size() != 1;
+                            if (!actionNameIsUniqueInModule || setNameNeedsAllModuleNames) {
+                                if (setNameHasModuleDetails) {
+                                    setName << "  ||  ";
+                                } else {
+                                    setNameHasModuleDetails = true;
+                                    if (!actionName.empty()) {
+                                        setName << " ";
+                                    }
+                                    setName << "(";
+                                }
+                                setName << module.getName();
+                                if (!actionNameIsUniqueInModule) {
+                                    setName << ": " << command;
+                                }
+                            }
+                        }
+                        if (setNameHasModuleDetails) {
+                           setName << ")";
+                        }
+                    }
+                    this->identifierToInfo.push_back(setName.str());
+                }
+                STORM_LOG_ASSERT(storm::utility::vector::isUnique(this->identifierToInfo), "The generated names for the prism choice origins are not unique.");
+            }
         }
     }
 }

src/storm/storage/sparse/PrismChoiceOrigins.h

@@ -25,16 +25,21 @@ namespace storm {
                  * Creates a new representation of the choice indices to their origin in the prism program
                  * @param prismProgram The associated prism program
                  * @param indexToIdentifierMapping maps a choice index to the internally used identifier of the choice origin
-                 * @param identifierToInfoMapping maps an origin identifier to a string representation of the origin
                  * @param identifierToCommandSetMapping maps an origin identifier to the set of global indices of the corresponding prism commands
                  */
-                PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping, std::vector<CommandSet> const& identifierToCommandSetMapping);
-                PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping, std::vector<CommandSet>&& identifierToCommandSetMapping);
+                PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<CommandSet> const& identifierToCommandSetMapping);
+                PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<CommandSet>&& identifierToCommandSetMapping);
                 
                 virtual ~PrismChoiceOrigins() = default;
                 
                 virtual bool isPrismChoiceOrigins() const override ;
                 
+                /*
+                 * Returns the largest identifier that is used by this object.
+                 * This can be used to, e.g., loop over all identifiers.
+                 */
+                virtual uint_fast64_t getLargestIdentifier() const override;
+                
                 /*
                  * Returns the prism program associated with this
                  */
@@ -45,17 +50,20 @@ namespace storm {
                  * The command set is represented by a set of global command indices
                  */
                 CommandSet const& getCommandSet(uint_fast64_t choiceIndex) const;
-                
+
+            protected:
                 /*
                  * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one.
                  */
                 virtual std::shared_ptr<ChoiceOrigins> cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const override;
                 
-            private:
+                /*
+                 * Computes the identifier infos (i.e., human readable strings representing the choice origins).
+                 */
+                virtual void computeIdentifierInfos() const override;
                 
                 std::shared_ptr<storm::prism::Program const> program;
                 std::vector<CommandSet> identifierToCommandSet;
-                
             };
         }
     }

src/storm/utility/vector.h

@@ -122,6 +122,27 @@ namespace storm {
                 return res;
             }
             
+            /*!
+             * Returns true iff every element in the given vector is unique, i.e., there are no i,j with i!=j and v[i]==v[j].
+             */
+            template<typename T>
+            bool isUnique(std::vector<T> const& v) {
+                if (v.size() < 2) {
+                    return true;
+                }
+                auto sortedIndices = getSortedIndices(v);
+                auto indexIt = sortedIndices.begin();
+                T const* previous = &v[*indexIt];
+                for (++indexIt; indexIt != sortedIndices.end(); ++indexIt) {
+                    T const& current = v[*indexIt];
+                    if (current==*previous) {
+                        return false;
+                    }
+                    previous = &current;
+                }
+                return true;
+            }
+            
             /*!
              * Selects the elements from a vector at the specified positions and writes them consecutively into another vector.
              * @param vector The vector into which the selected elements are to be written.