From ce9d7db67a1151357f85338e88e6a767679dff38 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 27 Oct 2016 13:56:08 +0200 Subject: [PATCH 1/3] fixed knuths die in pdtmc Former-commit-id: f52f34571d095619a2cd12a611507b912a9595b8 [formerly 20c9ef124ae3b2bbceea0e61dcba2f46894fb03e] Former-commit-id: f6d23f46eb12a2cce806d8fe4f5d250f65714025 --- examples/pdtmc/die.pm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); From d945cb279df4fa1cb04ea50a3a38c65d3a6c72e9 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Nov 2016 22:28:41 +0100 Subject: [PATCH 2/3] 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: From e0fd50cb9dc162ffece040092ce7a963c6f6898e Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 3 Nov 2016 11:42:32 +0100 Subject: [PATCH 3/3] Fixed export of sync input for no-action Former-commit-id: 7124276a8642c1f95c596afd69057ac0d668ba91 [formerly 1e63ff5245ec13fba0a78f4755eda9d053c3434f] Former-commit-id: 05f1f33c492935c4852d3882f5852887aaa2a8e7 --- src/storage/jani/JSONExporter.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 7025b21b2..13512f554 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -71,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); }