From 9c581bd6350679cf0739b16a59a6e4e9c266fe07 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 14 Feb 2017 10:21:18 +0100
Subject: [PATCH] fixed two issues: missing include in ToRationalNumberVisitor
 and missing check for whether actions are reused in a JANI parallel
 composition

---
 .../storage/expressions/ToRationalNumberVisitor.h      |  2 ++
 src/storm/storage/jani/Model.cpp                       |  2 +-
 src/storm/storage/jani/ParallelComposition.cpp         |  6 ++++--
 src/test/builder/DdJaniModelBuilderTest.cpp            | 10 ++++++++--
 4 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h
index 55576e5ad..1f2b88f48 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.h
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h
@@ -2,6 +2,8 @@
 
 #include <unordered_map>
 
+#include <boost/optional.hpp>
+
 #include "storm/adapters/CarlAdapter.h"
 
 #include "storm/storage/expressions/Expression.h"
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 083b8f7fb..8f6791441 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -1134,7 +1134,7 @@ namespace storm {
         }
 
         bool Model::reusesActionsInComposition() const {
-            if(composition->isParallelComposition()) {
+            if (composition->isParallelComposition()) {
                 return composition->asParallelComposition().areActionsReused();
             }
             return false;
diff --git a/src/storm/storage/jani/ParallelComposition.cpp b/src/storm/storage/jani/ParallelComposition.cpp
index 1eaa0ff08..d81db1d91 100644
--- a/src/storm/storage/jani/ParallelComposition.cpp
+++ b/src/storm/storage/jani/ParallelComposition.cpp
@@ -195,13 +195,15 @@ namespace storm {
                 for (auto const& vector : synchronizationVectors) {
                     std::string const& action = vector.getInput(inputIndex);
                     if (action != SynchronizationVector::NO_ACTION_INPUT) {
-                        return true;
+                        if (actions.find(action) != actions.end()) {
+                            return true;
+                        }
                         actions.insert(action);
                     }
                 }
                 // And check recursively, in case we have nested parallel composition
                 if (subcompositions.at(inputIndex)->isParallelComposition()) {
-                    if(subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) {
+                    if (subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) {
                         return true;
                     }
                 }
diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/builder/DdJaniModelBuilderTest.cpp
index 14f5e8081..2622662dc 100644
--- a/src/test/builder/DdJaniModelBuilderTest.cpp
+++ b/src/test/builder/DdJaniModelBuilderTest.cpp
@@ -17,6 +17,8 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/IOSettings.h"
 
+#include "storm/exceptions/InvalidSettingsException.h"
+
 TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
     storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
@@ -363,7 +365,9 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
     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);
+    newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+    janiModel.setSystemComposition(newComposition);
+    EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
 }
 
 TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
@@ -419,7 +423,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
     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);
+    newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+    janiModel.setSystemComposition(newComposition);
+    EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
 }
 
 TEST(DdJaniModelBuilderTest_Sylvan, Composition) {