From 12a5258a45839113b6f15cc8de9e2bba33442283 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Tue, 11 Oct 2016 22:32:49 +0200
Subject: [PATCH] second time is a charm

Former-commit-id: 9af436c8430d7f7665f885a8270dbf1c6974f279 [formerly 0594ee49f8b828485722b544ed48f386d2ed42f8]
Former-commit-id: db0f6c4dc3e0753b169441dd5e1b487cfdc6d773
---
 src/parser/JaniParser.cpp | 58 +++++++++++++++++++++------------------
 1 file changed, 32 insertions(+), 26 deletions(-)

diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index a7def4b2a..a49ab5548 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -697,24 +697,42 @@ namespace storm {
 
             return automaton;
         }
+        
+        std::vector<storm::jani::SynchronizationVector> parseSyncVectors(json const& syncVectorStructure) {
+            std::vector<storm::jani::SynchronizationVector> syncVectors;
+            // TODO add error checks
+            for (auto const& syncEntry : syncVectorStructure) {
+                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 syncVectors;
+        }
 
         std::shared_ptr<storm::jani::Composition> JaniParser::parseComposition(json const &compositionStructure) {
+            if(compositionStructure.count("automaton")) {
+                return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").get<std::string>()));
+            }
             
-            STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given");
+            STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given, got " << compositionStructure.dump());
             
-            if (compositionStructure.at("elements").size() == 1) {
-                if (compositionStructure.count("syncs") == 0) {
-                    // We might have an automaton.
-                    STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition");
-                    if (compositionStructure.at("elements").back().at("automaton").is_string()) {
-                        std::string name = compositionStructure.at("elements").back().at("automaton");
-                        // TODO check whether name exist?
-                        return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name));
-                    }
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Nesting parallel composition is not supported");
-                } else {
-                    // Might be rename or input-enable.
+            if (compositionStructure.at("elements").size() == 1 && compositionStructure.count("syncs") == 0) {
+                // We might have an automaton.
+                STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition");
+                if (compositionStructure.at("elements").back().at("automaton").is_string()) {
+                    std::string name = compositionStructure.at("elements").back().at("automaton");
+                    // TODO check whether name exist?
+                    return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name));
                 }
+                STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Trivial nesting parallel composition is not yet supported");
+                
             }
             
             std::vector<std::shared_ptr<storm::jani::Composition>>  compositions;
@@ -728,19 +746,7 @@ namespace storm {
             STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once");
             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);
-                }
+                syncVectors = parseSyncVectors(compositionStructure.at("syncs"));
             }
             
             return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition(compositions, syncVectors));