diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 7e54d15fb..17ef63125 100644 --- a/src/parser/JaniParser.cpp +++ b/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 #include #include @@ -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 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 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) { @@ -691,7 +695,34 @@ namespace storm { } std::shared_ptr 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(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> 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. + + } } } \ No newline at end of file diff --git a/src/storage/jani/AutomatonComposition.h b/src/storage/jani/AutomatonComposition.h index 497a85e8e..1df440365 100644 --- a/src/storage/jani/AutomatonComposition.h +++ b/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; diff --git a/src/storage/jani/Composition.h b/src/storage/jani/Composition.h index e1f1f85b6..b337f8015 100644 --- a/src/storage/jani/Composition.h +++ b/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; diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index cfadf0c41..aa6593274 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/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(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 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 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(subcomp)->getAutomatonName(); + } + compDecl["elements"] = elems; + std::vector 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()); }