diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index 7e453eb0f..fac8e2ad7 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -45,10 +45,7 @@ namespace storm { ParallelComposition::ParallelComposition(std::vector> const& subcompositions, std::vector 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> const& subcompositions, std::set const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() { @@ -98,17 +95,12 @@ namespace storm { for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { std::set 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 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 { @@ -136,4 +128,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 2d01bb209..1b0248ce5 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/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(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); }