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 9bca2d689..13512f554 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)); @@ -75,7 +71,14 @@ namespace storm { std::vector synElems; for (auto const& syncs : composition.getSynchronizationVectors()) { modernjson::json syncDecl; - syncDecl["synchronise"] = syncs.getInput(); + syncDecl["synchronise"] = std::vector(); + for (auto const& syncIn : syncs.getInput()) { + if (syncIn == SynchronizationVector::NO_ACTION_INPUT) { + syncDecl["synchronise"].push_back(nullptr); + } else { + syncDecl["synchronise"].push_back(syncIn); + } + } syncDecl["result"] = syncs.getOutput(); synElems.push_back(syncDecl); } @@ -691,10 +694,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: