From 1db826c0e233ef7ef5de937148df3ac56984e479 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Sun, 18 Sep 2016 22:01:45 +0200
Subject: [PATCH] recursive parallel composition support in im and export

Former-commit-id: 890653ddba2e04e42b2f1d92473e73b08dd1358f [formerly be393c71896480c8ac95064218ba3ba949caea82]
Former-commit-id: 2311af77390947cc809a92a4ced8ad928747b9d7
---
 src/parser/JaniParser.cpp         | 22 ++++++++++++++++++++--
 src/parser/JaniParser.h           |  1 +
 src/storage/jani/JSONExporter.cpp | 31 ++++++++++++++++++++++++++-----
 3 files changed, 47 insertions(+), 7 deletions(-)

diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index 17ef63125..343f8e2ce 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -715,13 +715,31 @@ namespace storm {
             
             std::vector<std::shared_ptr<storm::jani::Composition>>  compositions;
             for (auto const& elemDecl : compositionStructure.at("elements")) {
-                STORM_LOG_THROW(elemDecl.count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in the element");
+                if(!allowRecursion) {
+                    STORM_LOG_THROW(elemDecl.count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in the element");
+                }
                 compositions.push_back(parseComposition(elemDecl));
             }
             
             STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once");
-            // TODO parse syncs.
+            std::vector<storm::jani::SynchronizationVector> syncVectors;
+            if (compositionStructure.count("syncs") > 0) {
+                // TODO add error checks
+                for (auto const& syncEntry : compositionStructure.at("syncs")) {
+                    std::vector<std::string> inputs;
+                    for (auto const& syncInput : syncEntry.at("synchronise")) {
+                        if(syncInput.is_null()) {
+                            // TODO handle null;
+                        } else {
+                            inputs.push_back(syncInput);
+                        }
+                    }
+                    std::string syncResult = syncEntry.at("result");
+                    syncVectors.emplace_back(inputs, syncResult);
+                }
+            }
             
+            return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition(compositions, syncVectors));
             
         }
     }
diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h
index a033b7479..8fa4e8277 100644
--- a/src/parser/JaniParser.h
+++ b/src/parser/JaniParser.h
@@ -67,6 +67,7 @@ namespace storm {
              */
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
 
+            bool allowRecursion = true;
 
             //////////
             //   Default values -- assumptions from JANI.
diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp
index aa6593274..5d71540c4 100644
--- a/src/storage/jani/JSONExporter.cpp
+++ b/src/storage/jani/JSONExporter.cpp
@@ -31,8 +31,12 @@ namespace storm {
         
         class CompositionJsonExporter : public CompositionVisitor {
         public:
-            static modernjson::json translate(storm::jani::Composition const& comp) {
-                CompositionJsonExporter visitor;
+            CompositionJsonExporter(bool allowRecursion) : allowRecursion(allowRecursion){
+                
+            }
+            
+            static modernjson::json translate(storm::jani::Composition const& comp, bool allowRecursion = true) {
+                CompositionJsonExporter visitor(allowRecursion);
                 return boost::any_cast<modernjson::json>(comp.accept(visitor, boost::none));
             }
             
@@ -55,18 +59,35 @@ namespace storm {
                 std::vector<modernjson::json> elems;
                 for (auto const& subcomp : composition.getSubcompositions()) {
                     modernjson::json elemDecl;
-                    STORM_LOG_THROW(subcomp->isAutomaton(), storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI.");
-                    elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
+                    if (subcomp->isAutomaton()) {
+                        modernjson::json autDecl;
+                        autDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
+                        std::vector<modernjson::json> elements;
+                        elements.push_back(autDecl);
+                        elemDecl["elements"] = elements;
+                    } else {
+                        STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI.");
+                        elemDecl = boost::any_cast<modernjson::json>(subcomp->accept(*this, boost::none));
+                    }
+                    elems.push_back(elemDecl);
                 }
                 compDecl["elements"] = elems;
                 std::vector<modernjson::json> synElems;
                 for (auto const& syncs : composition.getSynchronizationVectors()) {
                     modernjson::json syncDecl;
-                    syncDecl["input"] = syncs.getInput();
+                    syncDecl["synchronise"] = syncs.getInput();
                     syncDecl["result"] = syncs.getOutput();
                     synElems.push_back(syncDecl);
                 }
+                if (!synElems.empty()) {
+                    compDecl["syncs"] = synElems;
+                }
+                
+                return compDecl;
             }
+            
+        private:
+            bool allowRecursion;
         };