parallel composition (full, restricted, interleaving) for PRISM appears to work, added some more sanity checks for parallel composition

Former-commit-id: 4ed40c8aba

src/builder/DdPrismModelBuilder.cpp

@@ -235,28 +235,47 @@ namespace storm {
                 
                 // Then, determine the action indices on which we need to synchronize.
                 std::set<uint_fast64_t> leftSynchronizationActionIndices = left.getSynchronizingActionIndices();
-                for (auto const& entry : leftSynchronizationActionIndices) {
-                    std::cout << "entry 1: " << entry << std::endl;
-                }
                 std::set<uint_fast64_t> rightSynchronizationActionIndices = right.getSynchronizingActionIndices();
-                for (auto const& entry : rightSynchronizationActionIndices) {
-                    std::cout << "entry 2: " << entry << std::endl;
-                }
                 std::set<uint_fast64_t> 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<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
+                typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this));
+
+                // Finally, we compose the subcompositions to create the result.
+                composeInParallel(left, right, std::set<uint_fast64_t>());
+                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<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
+                typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this));
+                
+                // Construct the synchronizing action indices from the synchronizing action names.
+                std::set<uint_fast64_t> synchronizingActionIndices;
+                for (auto const& action : composition.getSynchronizingActions()) {
+                    synchronizingActionIndices.insert(generationInfo.program.getActionIndex(action));
+                }
+                
+                std::set<uint_fast64_t> 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<uint_fast64_t> 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:

src/storage/prism/Program.cpp

@@ -61,7 +61,15 @@ namespace storm {
             }
             
             virtual boost::any visit(RestrictedParallelComposition const& composition) override {
-                return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
+                bool isValid = boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(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<uint_fast64_t> 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.");

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.

src/storage/prism/RestrictedParallelComposition.cpp

@@ -12,6 +12,10 @@ namespace storm {
         boost::any RestrictedParallelComposition::accept(CompositionVisitor& visitor) const {
             return visitor.visit(*this);
         }
+
+        std::set<std::string> const& RestrictedParallelComposition::getSynchronizingActions() const {
+            return synchronizingActions;
+        }
         
         void RestrictedParallelComposition::writeToStream(std::ostream& stream) const {
             stream << "(" << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(synchronizingActions, ", ") << "]| " << this->getRightSubcomposition() << ")";

src/storage/prism/RestrictedParallelComposition.h

@@ -14,6 +14,8 @@ namespace storm {
             
             virtual boost::any accept(CompositionVisitor& visitor) const override;
 
+            std::set<std::string> const& getSynchronizingActions() const;
+            
         protected:
             virtual void writeToStream(std::ostream& stream) const override;