added test for legality check of synch vectors

Former-commit-id: 6bef2f5a98 [formerly df607c9c1a]
Former-commit-id: 78cc502eb2

src/storage/jani/ParallelComposition.cpp

@@ -45,10 +45,7 @@ namespace storm {
         
         ParallelComposition::ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> const& synchronizationVectors) : subcompositions(subcompositions), synchronizationVectors(synchronizationVectors) {
             STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition.");
-
-            for (auto const& vector : this->synchronizationVectors) {
-                STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size.");
-            }
+            this->checkSynchronizationVectors();
         }
         
         ParallelComposition::ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() {
@@ -98,17 +95,12 @@ namespace storm {
             for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) {
                 std::set<std::string> actions;
                 for (auto const& vector : synchronizationVectors) {
+                    STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size.");
                     std::string const& action = vector.getInput(inputIndex);
                     STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vectors.");
                     actions.insert(action);
                 }
             }
-            
-            std::set<std::string> actions;
-            for (auto const& vector : synchronizationVectors) {
-                STORM_LOG_THROW(actions.find(vector.getOutput()) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same output action multiple times in synchronization vectors.");
-                actions.insert(vector.getOutput());
-            }
         }
         
         boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const {

test/functional/builder/DdJaniModelBuilderTest.cpp

@@ -357,4 +357,11 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
     model = builder.build(janiModel);
     EXPECT_EQ(3ul, model->getNumberOfStates());
     EXPECT_EQ(3ul, model->getNumberOfTransitions());
+    
+    inputVector.clear();
+    inputVector.push_back("b");
+    inputVector.push_back("c");
+    inputVector.push_back("b");
+    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
+    EXPECT_THROW(newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException);
 }