From dd137d647966228c177fe0830456b044e5857b42 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 16 Feb 2017 12:21:55 +0100
Subject: [PATCH] added test for using actions multiple times in different
 synch vectors in JANI model (DD builder)

---
 src/storm/builder/DdJaniModelBuilder.cpp    |  2 +-
 src/test/builder/DdJaniModelBuilderTest.cpp | 54 +++++++++++++++++++++
 2 files changed, 55 insertions(+), 1 deletion(-)

diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index d9cb430ec..94fda1882 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -1908,7 +1908,7 @@ namespace storm {
             // Cut transitions to reachable states.
             storm::dd::Add<Type, ValueType> reachableStatesAdd = modelComponents.reachableStates.template toAdd<ValueType>();
             modelComponents.transitionMatrix = system.transitions * reachableStatesAdd;
-            
+
             // Fix deadlocks if existing.
             modelComponents.deadlockStates = fixDeadlocks(preparedModel.getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
             
diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/builder/DdJaniModelBuilderTest.cpp
index 911d49551..0bc5940e0 100644
--- a/src/test/builder/DdJaniModelBuilderTest.cpp
+++ b/src/test/builder/DdJaniModelBuilderTest.cpp
@@ -421,6 +421,33 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
     EXPECT_EQ(3ul, model->getNumberOfStates());
     EXPECT_EQ(3ul, model->getNumberOfTransitions());
     
+    synchronizationVectors.clear();
+    inputVector.clear();
+    inputVector.push_back("a");
+    inputVector.push_back("b");
+    inputVector.push_back("c");
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("c");
+    inputVector.push_back("c");
+    inputVector.push_back("a");
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector, "b");
+    newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+    janiModel.setSystemComposition(newComposition);
+    model = builder.build(janiModel);
+    EXPECT_EQ(4ul, model->getNumberOfStates());
+    EXPECT_EQ(5ul, model->getNumberOfTransitions());
+    
     inputVector.clear();
     inputVector.push_back("b");
     inputVector.push_back("c");
@@ -539,6 +566,33 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
     model = builder.build(janiModel);
     EXPECT_EQ(3ul, model->getNumberOfStates());
     EXPECT_EQ(3ul, model->getNumberOfTransitions());
+
+    synchronizationVectors.clear();
+    inputVector.clear();
+    inputVector.push_back("a");
+    inputVector.push_back("b");
+    inputVector.push_back("c");
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("c");
+    inputVector.push_back("c");
+    inputVector.push_back("a");
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector, "b");
+    newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+    janiModel.setSystemComposition(newComposition);
+    model = builder.build(janiModel);
+    EXPECT_EQ(4ul, model->getNumberOfStates());
+    EXPECT_EQ(5ul, model->getNumberOfTransitions());
     
     inputVector.clear();
     inputVector.push_back("b");