From ce9d7db67a1151357f85338e88e6a767679dff38 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 27 Oct 2016 13:56:08 +0200
Subject: [PATCH 1/2] 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 <sebastian.junges@rwth-aachen.de>
Date: Wed, 2 Nov 2016 22:28:41 +0100
Subject: [PATCH 2/2] 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<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: