diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 6f56bf41c..98ff3128a 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -235,28 +235,47 @@ namespace storm { // Then, determine the action indices on which we need to synchronize. std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); - for (auto const& entry : leftSynchronizationActionIndices) { - std::cout << "entry 1: " << entry << std::endl; - } std::set rightSynchronizationActionIndices = right.getSynchronizingActionIndices(); - for (auto const& entry : rightSynchronizationActionIndices) { - std::cout << "entry 2: " << entry << std::endl; - } std::set synchronizationActionIndices; std::set_intersection(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), std::inserter(synchronizationActionIndices, synchronizationActionIndices.begin())); - // Finally, we compose the subcompositions to create the result. For this, we modify the left - // subcomposition in place and later return it. + // Finally, we compose the subcompositions to create the result. composeInParallel(left, right, synchronizationActionIndices); return left; } virtual boost::any visit(storm::prism::InterleavingParallelComposition const& composition) override { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Interleaving is currently not supported in symbolic model building."); + // First, we translate the subcompositions. + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this)); + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this)); + + // Finally, we compose the subcompositions to create the result. + composeInParallel(left, right, std::set()); + return left; } virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition) override { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Restricted parallel composition is currently not supported in symbolic model building."); + // First, we translate the subcompositions. + typename DdPrismModelBuilder::ModuleDecisionDiagram left = boost::any_cast::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this)); + typename DdPrismModelBuilder::ModuleDecisionDiagram right = boost::any_cast::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this)); + + // Construct the synchronizing action indices from the synchronizing action names. + std::set synchronizingActionIndices; + for (auto const& action : composition.getSynchronizingActions()) { + synchronizingActionIndices.insert(generationInfo.program.getActionIndex(action)); + } + + std::set leftSynchronizationActionIndices = left.getSynchronizingActionIndices(); + bool isContainedInLeft = std::includes(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end()); + STORM_LOG_WARN_COND(isContainedInLeft, "Left subcomposition of composition '" << composition << "' does not include all actions over which to synchronize."); + + std::set rightSynchronizationActionIndices = right.getSynchronizingActionIndices(); + bool isContainedInRight = std::includes(rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end()); + STORM_LOG_WARN_COND(isContainedInRight, "Right subcomposition of composition '" << composition << "' does not include all actions over which to synchronize."); + + // Finally, we compose the subcompositions to create the result. + composeInParallel(left, right, synchronizingActionIndices); + return left; } private: diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 57fd2a471..a76be8dc6 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -61,7 +61,15 @@ namespace storm { } virtual boost::any visit(RestrictedParallelComposition const& composition) override { - return boost::any_cast(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast(composition.getRightSubcomposition().accept(*this)); + bool isValid = boost::any_cast(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast(composition.getRightSubcomposition().accept(*this)); + + for (auto const& action : composition.getSynchronizingActions()) { + if (!program.hasAction(action)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'."); + } + } + + return isValid; } private: @@ -389,6 +397,20 @@ namespace storm { return indexNamePair->second; } + uint_fast64_t Program::getActionIndex(std::string const& actionName) const { + auto const& nameIndexPair = this->actionToIndexMap.find(actionName); + STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action name '" << actionName << "'."); + return nameIndexPair->second; + } + + bool Program::hasAction(std::string const& actionName) const { + return this->actionToIndexMap.find(actionName) != this->actionToIndexMap.end(); + } + + bool Program::hasAction(uint_fast64_t const& actionIndex) const { + return this->indexToActionMap.find(actionIndex) != this->indexToActionMap.end(); + } + std::set const& Program::getModuleIndicesByAction(std::string const& action) const { auto const& nameIndexPair = this->actionToIndexMap.find(action); STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist."); diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 6fc0fc2f4..c76bd7ed0 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -325,6 +325,28 @@ namespace storm { */ std::string const& getActionName(uint_fast64_t actionIndex) const; + /*! + * Retrieves the index of the action with the given name. + * + * @param actionName The name of the action. + * @return The index of the action. + */ + uint_fast64_t getActionIndex(std::string const& actionName) const; + + /*! + * Retrieves whether the program has an action with the given name. + * + * @return True iff the program has an action with the given name. + */ + bool hasAction(std::string const& actionName) const; + + /*! + * Retrieves whether the program has an action with the given index. + * + * @return True iff the program has an action with the given index. + */ + bool hasAction(uint_fast64_t const& actionIndex) const; + /*! * Retrieves the indices of all modules within this program that contain commands that are labelled with the * given action. diff --git a/src/storage/prism/RestrictedParallelComposition.cpp b/src/storage/prism/RestrictedParallelComposition.cpp index 5c9e54770..681fcc4b0 100644 --- a/src/storage/prism/RestrictedParallelComposition.cpp +++ b/src/storage/prism/RestrictedParallelComposition.cpp @@ -12,6 +12,10 @@ namespace storm { boost::any RestrictedParallelComposition::accept(CompositionVisitor& visitor) const { return visitor.visit(*this); } + + std::set const& RestrictedParallelComposition::getSynchronizingActions() const { + return synchronizingActions; + } void RestrictedParallelComposition::writeToStream(std::ostream& stream) const { stream << "(" << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(synchronizingActions, ", ") << "]| " << this->getRightSubcomposition() << ")"; diff --git a/src/storage/prism/RestrictedParallelComposition.h b/src/storage/prism/RestrictedParallelComposition.h index bddcb663e..9f0f14591 100644 --- a/src/storage/prism/RestrictedParallelComposition.h +++ b/src/storage/prism/RestrictedParallelComposition.h @@ -14,6 +14,8 @@ namespace storm { virtual boost::any accept(CompositionVisitor& visitor) const override; + std::set const& getSynchronizingActions() const; + protected: virtual void writeToStream(std::ostream& stream) const override;