initial support for compositions - not done yet

Former-commit-id: ef3bc88034 [formerly 058387a17c]
Former-commit-id: 87b5544298

src/parser/JaniParser.cpp

@@ -1,11 +1,14 @@
 #include "JaniParser.h"
 #include "src/storage/jani/Model.h"
 #include "src/storage/jani/Property.h"
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/InvalidJaniException.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/storage/jani/ModelType.h"
 
+
 #include <iostream>
 #include <sstream>
 #include <fstream>
@@ -106,8 +109,9 @@ namespace storm {
             for (auto const& automataEntry : parsedStructure.at("automata")) {
                 model.addAutomaton(parseAutomaton(automataEntry, model));
             }
-            //STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
-            //std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
+            STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
+            std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
+            model.setSystemComposition(composition);
             STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given");
             PropertyVector properties;
             if (parseProperties && parsedStructure.count("properties") == 1) {
@@ -692,6 +696,33 @@ namespace storm {
 
         std::shared_ptr<storm::jani::Composition> JaniParser::parseComposition(json const &compositionStructure) {
             
+            STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given");
+            
+            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.
+                }
+            }
+            
+            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");
+                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.
+            
+            
         }
     }
 }

src/storage/jani/AutomatonComposition.h

@@ -21,6 +21,8 @@ namespace storm {
             
             virtual void write(std::ostream& stream) const override;
             
+            bool isAutomaton() const override  { return true; }
+            
         private:
             // The name of the automaton this composition element refers to.
             std::string name;

src/storage/jani/Composition.h

@@ -9,6 +9,8 @@ namespace storm {
         
         class Composition {
         public:
+            virtual bool isAutomaton() const { return false; }
+            
             virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0;
             
             virtual void write(std::ostream& stream) const = 0;

src/storage/jani/JSONExporter.cpp

@@ -20,9 +20,56 @@
 #include "src/storage/expressions/BinaryRelationExpression.h"
 #include "src/storage/expressions/VariableExpression.h"
 
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/RenameComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
+
+
 namespace storm {
     namespace jani {
         
+        
+        class CompositionJsonExporter : public CompositionVisitor {
+        public:
+            static modernjson::json translate(storm::jani::Composition const& comp) {
+                CompositionJsonExporter visitor;
+                return boost::any_cast<modernjson::json>(comp.accept(visitor, boost::none));
+            }
+            
+            virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) {
+                modernjson::json compDecl;
+                modernjson::json autDecl;
+                autDecl["automaton"] = composition.getAutomatonName();
+                std::vector<modernjson::json> elements;
+                elements.push_back(autDecl);
+                compDecl["elements"] = elements;
+                return compDecl;
+            }
+            
+            virtual boost::any visit(RenameComposition const& composition, boost::any const& data) {
+                
+            }
+            virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) {
+                modernjson::json compDecl;
+                
+                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();
+                }
+                compDecl["elements"] = elems;
+                std::vector<modernjson::json> synElems;
+                for (auto const& syncs : composition.getSynchronizationVectors()) {
+                    modernjson::json syncDecl;
+                    syncDecl["input"] = syncs.getInput();
+                    syncDecl["result"] = syncs.getOutput();
+                    synElems.push_back(syncDecl);
+                }
+            }
+        };
+        
+        
         std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) {
             
             using OpType = storm::expressions::OperatorType;
@@ -332,7 +379,7 @@ namespace storm {
             jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables());
             jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction());
             jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.buildActionToNameMap());
-            //jsonStruct["system"] = buildComposition();
+            jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
             
         }