From d945cb279df4fa1cb04ea50a3a38c65d3a6c72e9 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Nov 2016 22:28:41 +0100 Subject: [PATCH] add derived operators to features, fixed composition export Former-commit-id: 4d57e83fdf4a6496c18723c128c4b569f0f004be [formerly f392ca29257e9f68a9c46ab2f412ed0676362c72] Former-commit-id: 555084f8b0e19850246c4f5c23dde2f8c8f19f67 --- src/storage/jani/JSONExporter.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 9bca2d689..7025b21b2 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -60,11 +60,7 @@ namespace storm { for (auto const& subcomp : composition.getSubcompositions()) { modernjson::json elemDecl; if (subcomp->isAutomaton()) { - modernjson::json autDecl; - autDecl["automaton"] = std::static_pointer_cast(subcomp)->getAutomatonName(); - std::vector elements; - elements.push_back(autDecl); - elemDecl["elements"] = elements; + elemDecl["automaton"] = std::static_pointer_cast(subcomp)->getAutomatonName(); } else { STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI."); elemDecl = boost::any_cast(subcomp->accept(*this, boost::none)); @@ -691,10 +687,14 @@ namespace storm { jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction()); jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap()); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); + std::vector standardFeatureVector = {"derived-operators"}; + jsonStruct["features"] = standardFeatureVector; } + + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { case storm::modelchecker::FilterType::MIN: