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: