From dfe0a445a1d43e6c0789261ad1a681490575a3f7 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Sun, 12 Feb 2017 14:13:24 +0100
Subject: [PATCH] JANI: Compacter export; Do not export optional values if they
 contain the default

---
 src/storm/storage/jani/JSONExporter.cpp | 29 ++++++++++++++++++++-----
 1 file changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 834ce8623..5231a1506 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -588,7 +588,9 @@ namespace storm {
             for(auto const& variable : varSet) {
                 modernjson::json varEntry;
                 varEntry["name"] = variable.getName();
-                varEntry["transient"] = variable.isTransient();
+                if (variable.isTransient()) {
+                    varEntry["transient"] = variable.isTransient();
+                }
                 modernjson::json typeDesc;
                 if(variable.isBooleanVariable()) {
                     typeDesc = "bool";
@@ -635,7 +637,9 @@ namespace storm {
                 modernjson::json locEntry;
                 locEntry["name"] = location.getName();
                 // TODO support invariants?
-                locEntry["transient-values"] = buildAssignmentArray(location.getAssignments());
+                if (!location.getAssignments().empty()) {
+                    locEntry["transient-values"] = buildAssignmentArray(location.getAssignments());
+                }
                 locationDeclarations.push_back(locEntry);
             }
             return modernjson::json(locationDeclarations);
@@ -655,8 +659,18 @@ namespace storm {
             for(auto const& destination : destinations) {
                 modernjson::json destEntry;
                 destEntry["location"] = locationNames.at(destination.getLocationIndex());
-                destEntry["probability"]["exp"] = buildExpression(destination.getProbability());
-                destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments());
+                bool prob1 = false;
+                if(destination.getProbability().isLiteral()) {
+                    if(destination.getProbability().evaluateAsDouble() == 1) {
+                        prob1 = true;
+                    }
+                }
+                if (!prob1) {
+                    destEntry["probability"]["exp"] = buildExpression(destination.getProbability());
+                }
+                if (!destination.getOrderedAssignments().empty()) {
+                    destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments());
+                }
                 destDeclarations.push_back(destEntry);
             }
             return modernjson::json(destDeclarations);
@@ -677,8 +691,13 @@ namespace storm {
                 if(edge.hasRate()) {
                     edgeEntry["rate"]["exp"] = buildExpression(edge.getRate());
                 }
-                edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard());
+                if (!edge.getGuard().isTrue()) {
+                    edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard());
+                }
                 edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames);
+                if (!edge.getAssignments().empty()) {
+                    edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments());
+                }
                 
                 edgeDeclarations.push_back(edgeEntry);
             }