diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 58f6e6c51..6b80e8c52 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -634,53 +634,11 @@ namespace storm { } std::vector identifierToCommandSetMapping(currentIdentifier); - std::vector 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(std::make_shared(program), std::move(identifiers), std::move(identifierToInfoMapping), std::move(identifierToCommandSetMapping)); + return std::make_shared(std::make_shared(program), std::move(identifiers), std::move(identifierToCommandSetMapping)); } diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp index 455791d66..be049bf84 100644 --- a/src/storm/models/sparse/ItemLabeling.cpp +++ b/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 ItemLabeling::getLabels() const { std::set result; for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h index 57b52ff76..fb39f4433 100644 --- a/src/storm/models/sparse/ItemLabeling.h +++ b/src/storm/models/sparse/ItemLabeling.h @@ -54,8 +54,6 @@ namespace storm { */ std::set 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. * diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp index 465500ea4..db6dcdd18 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.cpp +++ b/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 const& indexToIdentifierMapping, std::vector const& identifierToInfoMapping) : indexToIdentifier(indexToIdentifierMapping), identifierToInfo(identifierToInfoMapping) { + ChoiceOrigins::ChoiceOrigins(std::vector const& indexToIdentifierMapping) : indexToIdentifier(indexToIdentifierMapping) { // Intentionally left empty } - ChoiceOrigins::ChoiceOrigins(std::vector&& indexToIdentifierMapping, std::vector&& identifierToInfoMapping) : indexToIdentifier(std::move(indexToIdentifierMapping)), identifierToInfo(std::move(identifierToInfoMapping)) { + ChoiceOrigins::ChoiceOrigins(std::vector&& 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(indexToIdentifier, [&identifier](uint_fast64_t i) -> bool { return i == identifier;}); + if (!choicesWithIdentifier.empty()) { + result.addLabel(getIdentifierInfo(identifier), std::move(choicesWithIdentifier)); + } + } + return result; + } } } } \ No newline at end of file diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index 3b1a1faad..15f29c1aa 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/src/storm/storage/sparse/ChoiceOrigins.h @@ -3,6 +3,8 @@ #include #include #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 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 selectChoices(std::vector const& selectedChoiceIndices) const; + + storm::models::sparse::ChoiceLabeling toChoiceLabeling() const; protected: - ChoiceOrigins(std::vector const& indexToIdentifierMapping, std::vector const& identifierToInfoMapping); - ChoiceOrigins(std::vector&& indexToIdentifierMapping, std::vector&& identifierToInfoMapping); + ChoiceOrigins(std::vector const& indexToIdentifierMapping); + ChoiceOrigins(std::vector&& 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 cloneWithNewIndexToIdentifierMapping(std::vector&& indexToIdentifierMapping) const = 0; - std::vector indexToIdentifier; - std::vector identifierToInfo; + /* + * Computes the identifier infos (i.e., human readable strings representing the choice origins). + */ + virtual void computeIdentifierInfos() const = 0; + + std::vector const indexToIdentifier; + mutable std::vector identifierToInfo; + }; } } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.cpp b/src/storm/storage/sparse/JaniChoiceOrigins.cpp index 3548469f8..35f8f92cc 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.cpp +++ b/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 const& indexToIdentifierMapping, std::vector const& identifierToInfoMapping) : ChoiceOrigins(indexToIdentifierMapping, identifierToInfoMapping) { + JaniChoiceOrigins::JaniChoiceOrigins(std::vector 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 JaniChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector&& indexToIdentifierMapping) const { - std::vector identifierToInfoMapping = this->identifierToInfo; - return std::make_shared(std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping)); + return std::make_shared(std::move(indexToIdentifierMapping)); + } + + void JaniChoiceOrigins::computeIdentifierInfos() const { + } } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.h b/src/storm/storage/sparse/JaniChoiceOrigins.h index 58518c561..6d253fa68 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.h +++ b/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 const& indexToIdentifierMapping, std::vector const& identifierToInfoMapping); + JaniChoiceOrigins(std::vector 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 cloneWithNewIndexToIdentifierMapping(std::vector&& indexToIdentifierMapping) const override; + /* + * Computes the identifier infos (i.e., human readable strings representing the choice origins). + */ + virtual void computeIdentifierInfos() const override; + private: }; diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp index d087b5a54..2b4e5b3f8 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.cpp +++ b/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 const& prismProgram, std::vector const& indexToIdentifierMapping, std::vector const& identifierToInfoMapping, std::vector const& identifierToCommandSetMapping) : ChoiceOrigins(indexToIdentifierMapping, identifierToInfoMapping), program(prismProgram), identifierToCommandSet(identifierToCommandSetMapping) { + PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr const& prismProgram, std::vector const& indexToIdentifierMapping, std::vector 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 const& prismProgram, std::vector&& indexToIdentifierMapping, std::vector&& identifierToInfoMapping, std::vector&& identifierToCommandSetMapping) : ChoiceOrigins(std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping)), program(prismProgram), identifierToCommandSet(std::move(identifierToCommandSetMapping)) { + PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr const& prismProgram, std::vector&& indexToIdentifierMapping, std::vector&& 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 PrismChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector&& indexToIdentifierMapping) const { std::vector identifierToCommandSetMapping = this->identifierToCommandSet; - std::vector identifierToInfoMapping = this->identifierToInfo; - return std::make_shared(this->program, std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping), std::move(identifierToCommandSetMapping)); + auto result = std::make_shared(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."); + } } } } \ No newline at end of file diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h index 0d65728a2..0a820d178 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.h +++ b/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 const& prismProgram, std::vector const& indexToIdentifierMapping, std::vector const& identifierToInfoMapping, std::vector const& identifierToCommandSetMapping); - PrismChoiceOrigins(std::shared_ptr const& prismProgram, std::vector&& indexToIdentifierMapping, std::vector&& identifierToInfoMapping, std::vector&& identifierToCommandSetMapping); + PrismChoiceOrigins(std::shared_ptr const& prismProgram, std::vector const& indexToIdentifierMapping, std::vector const& identifierToCommandSetMapping); + PrismChoiceOrigins(std::shared_ptr const& prismProgram, std::vector&& indexToIdentifierMapping, std::vector&& 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 cloneWithNewIndexToIdentifierMapping(std::vector&& 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 program; std::vector identifierToCommandSet; - }; } } diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 76fc58a5c..3ac618b3e 100644 --- a/src/storm/utility/vector.h +++ b/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 + bool isUnique(std::vector 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 = ¤t; + } + 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.