diff --git a/examples/pdtmc/die.pm b/examples/pdtmc/die.pm index 31290bd69..a2a8f57b0 100644 --- a/examples/pdtmc/die.pm +++ b/examples/pdtmc/die.pm @@ -16,7 +16,7 @@ module die [] s=2 -> q : (s'=5) + 1-q : (s'=6); [] s=3 -> p : (s'=1) + 1-p : (s'=7) & (d'=1); [] s=4 -> p : (s'=7) & (d'=3) + 1-p : (s'=7) & (d'=2); - [] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=6); + [] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=4); [] s=6 -> p : (s'=7) & (d'=6) + 1-p : (s'=7) & (d'=5); [] s=7 -> 1: (s'=7); diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 46c4ef1be..6152cd9ec 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->isAutomatonComposition()) { - modernjson::json autDecl; - autDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName(); - std::vector<modernjson::json> elements; - elements.push_back(autDecl); - elemDecl["elements"] = elements; + elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName(); } else { STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI."); elemDecl = boost::any_cast<modernjson::json>(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<std::string> standardFeatureVector = {"derived-operators"}; + jsonStruct["features"] = standardFeatureVector; } + + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { case storm::modelchecker::FilterType::MIN: