From 36e07006f98c0cd055b6102a018dcbdfe4a5f67d Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 15 Sep 2016 21:26:03 +0200 Subject: [PATCH] added test for legality check of synch vectors Former-commit-id: 6bef2f5a987e5fc32883b2432ac0501bee338b5f [formerly df607c9c1ab9028f8fd9dbaa19b2a031dd85c282] Former-commit-id: 78cc502eb2678fc29a568038e00cf24bc928d23d --- src/storage/jani/ParallelComposition.cpp | 14 +++----------- test/functional/builder/DdJaniModelBuilderTest.cpp | 7 +++++++ 2 files changed, 10 insertions(+), 11 deletions(-) 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); }