From 6af6bc5472a8c024d49dbd5c8adfccf85fffbbab Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 13 Mar 2020 16:32:09 +0100
Subject: [PATCH] Replaced remaining uses of modernjson::json with the new
storm::json<..>
---
src/storm-dft/parser/DFTJsonParser.cpp | 18 +-
src/storm-dft/parser/DFTJsonParser.h | 12 +-
src/storm-dft/storage/dft/DftJsonExporter.cpp | 14 +-
src/storm-dft/storage/dft/DftJsonExporter.h | 14 +-
.../storage/gspn/GspnJsonExporter.cpp | 52 ++--
.../storage/gspn/GspnJsonExporter.h | 17 +-
src/storm/storage/Qvbs.cpp | 9 +-
src/storm/storage/Qvbs.h | 9 +-
src/storm/storage/jani/JSONExporter.cpp | 222 +++++++++---------
src/storm/storage/jani/JSONExporter.h | 27 +--
10 files changed, 189 insertions(+), 205 deletions(-)
diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp
index b099aeca9..0cda7ff08 100644
--- a/src/storm-dft/parser/DFTJsonParser.cpp
+++ b/src/storm-dft/parser/DFTJsonParser.cpp
@@ -21,7 +21,7 @@ namespace storm {
STORM_LOG_DEBUG("Parsing from JSON file");
std::ifstream file;
storm::utility::openFile(filename, file);
- json jsonInput;
+ Json jsonInput;
jsonInput << file;
storm::utility::closeFile(file);
return parseJson(jsonInput);
@@ -30,19 +30,19 @@ namespace storm {
template<typename ValueType>
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJsonFromString(std::string const& jsonString) {
STORM_LOG_DEBUG("Parsing from JSON string");
- json jsonInput = json::parse(jsonString);
+ Json jsonInput = Json::parse(jsonString);
return parseJson(jsonInput);
}
template<typename ValueType>
- storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJson(json const& jsonInput) {
+ storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJson(Json const& jsonInput) {
// Init DFT builder and value parser
storm::builder::DFTBuilder<ValueType> builder;
ValueParser<ValueType> valueParser;
// Try to parse parameters
if (jsonInput.find("parameters") != jsonInput.end()) {
- json parameters = jsonInput.at("parameters");
+ Json parameters = jsonInput.at("parameters");
STORM_LOG_THROW(parameters.empty() || (std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException,
"Parameters only allowed when using rational functions.");
for (auto it = parameters.begin(); it != parameters.end(); ++it) {
@@ -52,12 +52,12 @@ namespace storm {
}
}
- json nodes = jsonInput.at("nodes");
+ Json nodes = jsonInput.at("nodes");
// Start by building mapping from ids to their unique names
std::map<std::string, std::string> nameMapping;
std::set<std::string> names;
for (auto& element : nodes) {
- json data = element.at("data");
+ Json data = element.at("data");
std::string id = data.at("id");
std::string uniqueName = generateUniqueName(data.at("name"));
STORM_LOG_THROW(names.find(uniqueName) == names.end(), storm::exceptions::WrongFormatException, "Element '" << uniqueName << "' was already declared.");
@@ -69,7 +69,7 @@ namespace storm {
for (auto& element : nodes) {
STORM_LOG_TRACE("Parsing: " << element);
bool success = true;
- json data = element.at("data");
+ Json data = element.at("data");
std::string name = generateUniqueName(data.at("name"));
std::vector<std::string> childNames;
if (data.count("children") > 0) {
@@ -137,7 +137,7 @@ namespace storm {
// TODO: do splitting later in rewriting step
if (type != "fdep" && type != "pdep") {
// Set layout positions
- json position = element.at("position");
+ Json position = element.at("position");
double x = position.at("x");
double y = position.at("y");
builder.addLayoutInfo(name, x / 7, y / 7);
@@ -171,7 +171,7 @@ namespace storm {
}
template<typename ValueType>
- std::string DFTJsonParser<ValueType>::parseJsonNumber(json number) {
+ std::string DFTJsonParser<ValueType>::parseJsonNumber(Json number) {
if (number.is_string()) {
return number.get<std::string>();
} else {
diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h
index c092d47eb..8bcd4605a 100644
--- a/src/storm-dft/parser/DFTJsonParser.h
+++ b/src/storm-dft/parser/DFTJsonParser.h
@@ -4,18 +4,14 @@
#include "storm-dft/storage/dft/DFT.h"
#include "storm-dft/builder/DFTBuilder.h"
-
-// JSON parser
-#include "json.hpp"
-
-using json = nlohmann::json;
-
+#include "storm/adapters/JsonAdapter.h"
namespace storm {
namespace parser {
template<typename ValueType>
class DFTJsonParser {
+ typedef typename storm::json<double> Json;
public:
static storm::storage::DFT<ValueType> parseJsonFromString(std::string const& jsonString);
@@ -23,11 +19,11 @@ namespace storm {
static storm::storage::DFT<ValueType> parseJsonFromFile(std::string const& filename);
private:
- static storm::storage::DFT<ValueType> parseJson(json const& jsonInput);
+ static storm::storage::DFT<ValueType> parseJson(Json const& jsonInput);
static std::string generateUniqueName(std::string const& name);
- static std::string parseJsonNumber(json number);
+ static std::string parseJsonNumber(Json number);
};
}
}
diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp
index 9ff66615e..506536ee5 100644
--- a/src/storm-dft/storage/dft/DftJsonExporter.cpp
+++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp
@@ -24,23 +24,23 @@ namespace storm {
}
template<typename ValueType>
- modernjson::json DftJsonExporter<ValueType>::translate(storm::storage::DFT<ValueType> const& dft) {
+ typename DftJsonExporter<ValueType>::Json DftJsonExporter<ValueType>::translate(storm::storage::DFT<ValueType> const& dft) {
// Nodes
- modernjson::json jsonNodes;
+ Json jsonNodes;
for (size_t i = 0; i < dft.nrElements(); ++i) {
- modernjson::json jsonNode = translateNode(dft.getElement(i));
+ Json jsonNode = translateNode(dft.getElement(i));
jsonNodes.push_back(jsonNode);
}
- modernjson::json jsonDft;
+ Json jsonDft;
jsonDft["toplevel"] = std::to_string(dft.getTopLevelIndex());
jsonDft["nodes"] = jsonNodes;
return jsonDft;
}
template<typename ValueType>
- modernjson::json DftJsonExporter<ValueType>::translateNode(DFTElementCPointer const& element) {
- modernjson::json nodeData;
+ typename DftJsonExporter<ValueType>::Json DftJsonExporter<ValueType>::translateNode(DFTElementCPointer const& element) {
+ Json nodeData;
nodeData["id"] = std::to_string(element->id());
nodeData["name"] = element->name();
std::string type = storm::storage::toString(element->type());
@@ -117,7 +117,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Element of type '" << element->type() << "' is not supported.");
}
- modernjson::json jsonNode;
+ Json jsonNode;
jsonNode["data"] = nodeData;
jsonNode["group"] = "nodes";
jsonNode["classes"] = type;
diff --git a/src/storm-dft/storage/dft/DftJsonExporter.h b/src/storm-dft/storage/dft/DftJsonExporter.h
index 646821bb6..542857879 100644
--- a/src/storm-dft/storage/dft/DftJsonExporter.h
+++ b/src/storm-dft/storage/dft/DftJsonExporter.h
@@ -3,12 +3,7 @@
#include "storm/utility/macros.h"
#include "storm-dft/storage/dft/DFT.h"
-
-// JSON parser
-#include "json.hpp"
-namespace modernjson {
- using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>;
-}
+#include "storm/adapters/JsonAdapter.h"
namespace storm {
namespace storage {
@@ -18,7 +13,8 @@ namespace storm {
*/
template<typename ValueType>
class DftJsonExporter {
-
+ typedef typename storm::json<double> Json;
+
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementCPointer = std::shared_ptr<DFTElement<ValueType> const>;
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
@@ -31,9 +27,9 @@ namespace storm {
private:
- static modernjson::json translate(storm::storage::DFT<ValueType> const& dft);
+ static Json translate(storm::storage::DFT<ValueType> const& dft);
- static modernjson::json translateNode(DFTElementCPointer const& element);
+ static Json translateNode(DFTElementCPointer const& element);
};
}
diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
index f4e910b81..0c2df7532 100644
--- a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
+++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
@@ -17,8 +17,8 @@ namespace storm {
os << translate(gspn).dump(4) << std::endl;
}
- modernjson::json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) {
- modernjson::json jsonGspn;
+ typename GspnJsonExporter::Json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) {
+ Json jsonGspn;
// Layouts
std::map<uint64_t, LayoutInfo> placeLayout = gspn.getPlaceLayoutInfos();
@@ -35,7 +35,7 @@ namespace storm {
y = placeLayout.at(place.getID()).y;
}
tmpX += 3;
- modernjson::json jsonPlace = translatePlace(place, x, y);
+ Json jsonPlace = translatePlace(place, x, y);
jsonGspn.push_back(jsonPlace);
}
@@ -48,7 +48,7 @@ namespace storm {
y = transitionLayout.at(transition.getID()).y;
}
tmpX += 3;
- modernjson::json jsonImmediateTransition = translateImmediateTransition(transition, x, y);
+ Json jsonImmediateTransition = translateImmediateTransition(transition, x, y);
jsonGspn.push_back(jsonImmediateTransition);
}
@@ -61,7 +61,7 @@ namespace storm {
y = transitionLayout.at(transition.getID()).y;
}
tmpX += 3;
- modernjson::json jsonTimedTransition = translateTimedTransition(transition, x, y);
+ Json jsonTimedTransition = translateTimedTransition(transition, x, y);
jsonGspn.push_back(jsonTimedTransition);
}
@@ -72,21 +72,21 @@ namespace storm {
// Export input arcs
for (auto const& entry : transition.getInputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
- modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INPUT);
+ Json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INPUT);
jsonGspn.push_back(jsonInputArc);
}
// Export inhibitor arcs
for (auto const& entry : transition.getInhibitionPlaces()) {
storm::gspn::Place place = places.at(entry.first);
- modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INHIBITOR);
+ Json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::INHIBITOR);
jsonGspn.push_back(jsonInputArc);
}
// Export output arcs
for (auto const& entry : transition.getOutputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
- modernjson::json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::OUTPUT);
+ Json jsonInputArc = translateArc(transition, place, entry.second, true, ArcType::OUTPUT);
jsonGspn.push_back(jsonInputArc);
}
}
@@ -95,21 +95,21 @@ namespace storm {
// Export input arcs
for (auto const& entry : transition.getInputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
- modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INPUT);
+ Json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INPUT);
jsonGspn.push_back(jsonInputArc);
}
// Export inhibitor arcs
for (auto const& entry : transition.getInhibitionPlaces()) {
storm::gspn::Place place = places.at(entry.first);
- modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INHIBITOR);
+ Json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::INHIBITOR);
jsonGspn.push_back(jsonInputArc);
}
// Export output arcs
for (auto const& entry : transition.getOutputPlaces()) {
storm::gspn::Place place = places.at(entry.first);
- modernjson::json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::OUTPUT);
+ Json jsonInputArc = translateArc(transition, place, entry.second, false, ArcType::OUTPUT);
jsonGspn.push_back(jsonInputArc);
}
}
@@ -117,17 +117,17 @@ namespace storm {
}
- modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place, double x, double y) {
- modernjson::json data;
+ typename GspnJsonExporter::Json GspnJsonExporter::translatePlace(storm::gspn::Place const& place, double x, double y) {
+ Json data;
data["id"] = toJsonString(place);
data["name"] = place.getName();
data["marking"] = place.getNumberOfInitialTokens();
- modernjson::json position;
+ Json position;
position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor;
- modernjson::json jsonPlace;
+ Json jsonPlace;
jsonPlace["data"] = data;
jsonPlace["position"] = position;
jsonPlace["group"] = "nodes";
@@ -135,18 +135,18 @@ namespace storm {
return jsonPlace;
}
- modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y) {
- modernjson::json data;
+ typename GspnJsonExporter::Json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y) {
+ Json data;
data["id"] = toJsonString(transition, true);
data["name"] = transition.getName();
data["priority"] = transition.getPriority();
data["weight"] = transition.getWeight();
- modernjson::json position;
+ Json position;
position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor;
- modernjson::json jsonTrans;
+ Json jsonTrans;
jsonTrans["data"] = data;
jsonTrans["position"] = position;
jsonTrans["group"] = "nodes";
@@ -154,8 +154,8 @@ namespace storm {
return jsonTrans;
}
- modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y) {
- modernjson::json data;
+ typename GspnJsonExporter::Json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y) {
+ Json data;
data["id"] = toJsonString(transition, false);
data["name"] = transition.getName();
data["rate"] = transition.getRate();
@@ -170,11 +170,11 @@ namespace storm {
}
}
- modernjson::json position;
+ Json position;
position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor;
- modernjson::json jsonTrans;
+ Json jsonTrans;
jsonTrans["data"] = data;
jsonTrans["position"] = position;
jsonTrans["group"] = "nodes";
@@ -182,14 +182,14 @@ namespace storm {
return jsonTrans;
}
- modernjson::json GspnJsonExporter::translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype) {
- modernjson::json data;
+ typename GspnJsonExporter::Json GspnJsonExporter::translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype) {
+ Json data;
data["id"] = toJsonString(transition, place, arctype);
data["source"] = toJsonString(place);
data["target"] = toJsonString(transition, immediate);
data["mult"] = multiplicity;
- modernjson::json jsonArc;
+ Json jsonArc;
jsonArc["data"] = data;
//jsonTrans["group"] = "nodes";
switch (arctype) {
diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.h b/src/storm-gspn/storage/gspn/GspnJsonExporter.h
index 9c225434d..e8a55df51 100644
--- a/src/storm-gspn/storage/gspn/GspnJsonExporter.h
+++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.h
@@ -4,11 +4,7 @@
#include "storm-gspn/storage/gspn/GSPN.h"
-// JSON parser
-#include "json.hpp"
-namespace modernjson {
- using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>;
-}
+#include "storm/adapters/JsonAdapter.h"
namespace storm {
namespace gspn {
@@ -19,20 +15,21 @@ namespace storm {
class GspnJsonExporter {
public:
+ typedef typename storm::json<double> Json;
static void toStream(storm::gspn::GSPN const& gspn, std::ostream& os);
- static modernjson::json translate(storm::gspn::GSPN const& gspn);
+ static Json translate(storm::gspn::GSPN const& gspn);
private:
enum ArcType { INPUT, OUTPUT, INHIBITOR };
- static modernjson::json translatePlace(storm::gspn::Place const& place, double x, double y);
+ static Json translatePlace(storm::gspn::Place const& place, double x, double y);
- static modernjson::json translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y);
+ static Json translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y);
- static modernjson::json translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y);
+ static Json translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y);
- static modernjson::json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype);
+ static Json translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype);
std::string static inline toJsonString(storm::gspn::Place const& place) {
std::stringstream stream;
diff --git a/src/storm/storage/Qvbs.cpp b/src/storm/storage/Qvbs.cpp
index cb810c948..71c012568 100644
--- a/src/storm/storage/Qvbs.cpp
+++ b/src/storm/storage/Qvbs.cpp
@@ -9,13 +9,14 @@
#include "storm/settings/modules/IOSettings.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/utility/constants.h"
namespace storm {
namespace storage {
- modernjson::json readQvbsJsonFile(std::string const& filePath) {
+ storm::json<storm::RationalNumber> readQvbsJsonFile(std::string const& filePath) {
STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(filePath), storm::exceptions::WrongFormatException, "QVBS json file " << filePath << " was not found.");
- modernjson::json result;
+ storm::json<storm::RationalNumber> result;
std::ifstream file;
storm::utility::openFile(filePath, file);
result << file;
@@ -23,11 +24,11 @@ namespace storm {
return result;
}
- std::string getString(modernjson::json const& structure, std::string const& errorInfo = "") {
+ std::string getString(storm::json<storm::RationalNumber> const& structure, std::string const& errorInfo = "") {
if (structure.is_number_integer()) {
return std::to_string(structure.get<int64_t>());
} else if (structure.is_number_float()) {
- return std::to_string(structure.get<double>());
+ return storm::utility::to_string(structure.get<storm::RationalNumber>());
} else if (structure.is_string()) {
return structure.get<std::string>();
} else if (structure.is_boolean()) {
diff --git a/src/storm/storage/Qvbs.h b/src/storm/storage/Qvbs.h
index d88c28bd9..8a101d78d 100644
--- a/src/storm/storage/Qvbs.h
+++ b/src/storm/storage/Qvbs.h
@@ -4,11 +4,8 @@
#include <vector>
#include <boost/optional.hpp>
-// JSON parser
-#include "json.hpp"
-namespace modernjson {
- using json = nlohmann::json;
-}
+#include "storm/adapters/JsonAdapter.h"
+#include "storm/adapters/RationalNumberAdapter.h"
namespace storm {
@@ -36,7 +33,7 @@ namespace storm {
std::vector<std::string> instanceInfos;
std::string modelPath;
- modernjson::json modelData;
+ storm::json<storm::RationalNumber> modelData;
};
}
}
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 2975f9ff3..bf082b3e0 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -39,13 +39,13 @@
namespace storm {
namespace jani {
- modernjson::json anyToJson(boost::any&& input) {
+ ExportJsonType anyToJson(boost::any&& input) {
boost::any tmp(std::move(input));
- modernjson::json res = std::move(*boost::any_cast<modernjson::json>(&tmp));
+ ExportJsonType res = std::move(*boost::any_cast<ExportJsonType>(&tmp));
return res;
}
- modernjson::json buildExpression(storm::expressions::Expression const& exp, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet(), std::unordered_set<std::string> const& auxiliaryVariables = {}) {
+ ExportJsonType buildExpression(storm::expressions::Expression const& exp, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet(), std::unordered_set<std::string> const& auxiliaryVariables = {}) {
STORM_LOG_TRACE("Exporting " << exp);
return ExpressionToJson::translate(exp, constants, globalVariables, localVariables, auxiliaryVariables);
}
@@ -56,27 +56,27 @@ namespace storm {
}
- static modernjson::json translate(storm::jani::Composition const& comp, bool allowRecursion = true) {
+ static ExportJsonType translate(storm::jani::Composition const& comp, bool allowRecursion = true) {
CompositionJsonExporter visitor(allowRecursion);
return anyToJson(comp.accept(visitor, boost::none));
}
virtual boost::any visit(AutomatonComposition const& composition, boost::any const&) {
- modernjson::json compDecl;
- modernjson::json autDecl;
+ ExportJsonType compDecl;
+ ExportJsonType autDecl;
autDecl["automaton"] = composition.getAutomatonName();
- std::vector<modernjson::json> elements;
+ std::vector<ExportJsonType> elements;
elements.push_back(autDecl);
compDecl["elements"] = elements;
return compDecl;
}
virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) {
- modernjson::json compDecl;
+ ExportJsonType compDecl;
- std::vector<modernjson::json> elems;
+ std::vector<ExportJsonType> elems;
for (auto const& subcomp : composition.getSubcompositions()) {
- modernjson::json elemDecl;
+ ExportJsonType elemDecl;
if (subcomp->isAutomatonComposition()) {
elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
} else {
@@ -86,9 +86,9 @@ namespace storm {
elems.push_back(elemDecl);
}
compDecl["elements"] = elems;
- std::vector<modernjson::json> synElems;
+ std::vector<ExportJsonType> synElems;
for (auto const& syncs : composition.getSynchronizationVectors()) {
- modernjson::json syncDecl;
+ ExportJsonType syncDecl;
syncDecl["synchronise"] = std::vector<std::string>();
for (auto const& syncIn : syncs.getInput()) {
if (syncIn == SynchronizationVector::NO_ACTION_INPUT) {
@@ -125,11 +125,11 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
}
- modernjson::json numberToJson(storm::RationalNumber rn) {
- modernjson::json numDecl;
+ ExportJsonType numberToJson(storm::RationalNumber rn) {
+ ExportJsonType numDecl;
numDecl = storm::utility::convertNumber<double>(rn);
// if(carl::isOne(carl::getDenom(rn))) {
-// numDecl = modernjson::json(carl::toString(carl::getNum(rn)));
+// numDecl = ExportJsonType(carl::toString(carl::getNum(rn)));
// } else {
// numDecl["op"] = "/";
// // TODO set json lib to work with arbitrary precision ints.
@@ -142,12 +142,12 @@ namespace storm {
}
- modernjson::json FormulaToJaniJson::constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const {
+ ExportJsonType FormulaToJaniJson::constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const {
STORM_LOG_THROW((lower.is_initialized() || upper.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval needs either a lower or an upper bound, but none was given.");
STORM_LOG_THROW((lower.is_initialized() || !lowerExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the lower bound is exclusive but no lower bound is given.");
STORM_LOG_THROW((upper.is_initialized() || !upperExclusive.is_initialized()), storm::exceptions::InvalidJaniException, "PropertyInterval defines wether the upper bound is exclusive but no upper bound is given.");
- modernjson::json iDecl;
+ ExportJsonType iDecl;
if (lower) {
iDecl["lower"] = buildExpression(*lower, model.getConstants(), model.getGlobalVariables());
if (lowerExclusive) {
@@ -163,7 +163,7 @@ namespace storm {
return iDecl;
}
- modernjson::json FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const {
+ ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const {
storm::jani::RewardModelInformation info(model, rewardModelName);
bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards());
@@ -173,7 +173,7 @@ namespace storm {
return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit));
}
- modernjson::json FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const {
+ ExportJsonType FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const {
std::vector<std::string> res;
if (rewardAccumulation.isStepsSet()) {
res.push_back("steps");
@@ -188,7 +188,7 @@ namespace storm {
return res;
}
- modernjson::json FormulaToJaniJson::constructStandardRewardAccumulation(std::string const& rewardModelName) const {
+ ExportJsonType FormulaToJaniJson::constructStandardRewardAccumulation(std::string const& rewardModelName) const {
if (model.isDiscreteTimeModel()) {
return constructRewardAccumulation(storm::logic::RewardAccumulation(true, false, true), rewardModelName);
} else {
@@ -196,7 +196,7 @@ namespace storm {
}
}
- modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
+ ExportJsonType FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
FormulaToJaniJson translator(model);
auto result = anyToJson(formula.accept(translator));
if (translator.containsStateExitRewards()) {
@@ -214,11 +214,11 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const {
- modernjson::json opDecl(f.getLabel());
+ ExportJsonType opDecl(f.getLabel());
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{
- modernjson::json opDecl;
+ ExportJsonType opDecl;
storm::logic::BinaryBooleanStateFormula::OperatorType op = f.getOperator();
opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "∧" : "∨";
opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data));
@@ -226,18 +226,18 @@ namespace storm {
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const&) const {
- modernjson::json opDecl(f.isTrueFormula() ? true : false);
+ ExportJsonType opDecl(f.isTrueFormula() ? true : false);
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(!f.hasMultiDimensionalSubformulas(), storm::exceptions::NotSupportedException, "Jani export of multi-dimensional bounded until formulas is not supported.");
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data));
opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data));
bool hasStepBounds(false), hasTimeBounds(false);
- std::vector<modernjson::json> rewardBounds;
+ std::vector<ExportJsonType> rewardBounds;
for (uint64_t i = 0; i < f.getDimension(); ++i) {
boost::optional<storm::expressions::Expression> lower, upper;
@@ -250,7 +250,7 @@ namespace storm {
upper = f.getUpperBound(i);
upperExclusive = f.isUpperBoundStrict(i);
}
- modernjson::json propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive);
+ ExportJsonType propertyInterval = constructPropertyInterval(lower, lowerExclusive, upper, upperExclusive);
auto tbr = f.getTimeBoundReference(i);
if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) {
@@ -258,7 +258,7 @@ namespace storm {
hasStepBounds = true;
opDecl["step-bounds"] = propertyInterval;
} else if(tbr.isRewardBound()) {
- modernjson::json rewbound;
+ ExportJsonType rewbound;
rewbound["exp"] = buildExpression(model.getRewardModelExpression(tbr.getRewardName()), model.getConstants(), model.getGlobalVariables());
if (tbr.hasRewardAccumulation()) {
rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName());
@@ -274,7 +274,7 @@ namespace storm {
}
}
if (!rewardBounds.empty()) {
- opDecl["reward-bounds"] = modernjson::json(rewardBounds);
+ opDecl["reward-bounds"] = ExportJsonType(rewardBounds);
}
return opDecl;
@@ -289,7 +289,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getTrueFormula()->accept(*this, data));
opDecl["right"] = anyToJson(f.getSubformula().accept(*this, data));
@@ -297,7 +297,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
// Create standard reward accumulation for time operator formulas.
storm::logic::RewardAccumulation rewAcc(model.isDiscreteTimeModel(), !model.isDiscreteTimeModel(), false);
@@ -320,7 +320,7 @@ namespace storm {
opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin";
opDecl["left"]["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
}
- opDecl["left"]["exp"] = modernjson::json(1);
+ opDecl["left"]["exp"] = ExportJsonType(1);
opDecl["left"]["accumulate"] = rewAccJson;
opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables());
} else {
@@ -336,14 +336,14 @@ namespace storm {
opDecl["op"] = "Emin";
opDecl["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
}
- opDecl["exp"] = modernjson::json(1);
+ opDecl["exp"] = ExportJsonType(1);
opDecl["accumulate"] = rewAccJson;
}
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "G";
opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data));
return opDecl;
@@ -354,7 +354,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
if(f.hasBound()) {
auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
@@ -381,7 +381,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const&, boost::any const&) const {
-// modernjson::json opDecl;
+// ExportJsonType opDecl;
// if(f.()) {
// auto bound = f.getBound();
// opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
@@ -419,7 +419,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getTrueFormula()->accept(*this, data));
opDecl["right"] = anyToJson(f.getSubformula().accept(*this, data));
@@ -432,7 +432,7 @@ namespace storm {
boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
if(f.hasBound()) {
auto bound = f.getBound();
@@ -460,7 +460,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
std::string instantName;
if (model.isDiscreteTimeModel()) {
@@ -529,7 +529,7 @@ namespace storm {
opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables());
if(f.hasBound()) {
- modernjson::json compDecl;
+ ExportJsonType compDecl;
auto bound = f.getBound();
compDecl["op"] = comparisonTypeToJani(bound.comparisonType);
compDecl["left"] = std::move(opDecl);
@@ -545,7 +545,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator();
assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
opDecl["op"] = "¬";
@@ -554,7 +554,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data));
opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data));
@@ -616,7 +616,7 @@ namespace storm {
}
}
- modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables) {
+ ExportJsonType ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables) {
// Simplify the expression first and reduce the nesting
auto simplifiedExpr = storm::jani::reduceNestingInJaniExpression(expr.simplify());
@@ -626,7 +626,7 @@ namespace storm {
}
boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "ite";
opDecl["if"] = anyToJson(expression.getCondition()->accept(*this, data));
opDecl["then"] = anyToJson(expression.getThenExpression()->accept(*this, data));
@@ -634,21 +634,21 @@ namespace storm {
return opDecl;
}
boost::any ExpressionToJson::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data));
return opDecl;
}
boost::any ExpressionToJson::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data));
return opDecl;
}
boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data));
@@ -656,47 +656,47 @@ namespace storm {
}
boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const&) {
if (auxiliaryVariables.count(expression.getVariableName())) {
- return modernjson::json(expression.getVariableName());
+ return ExportJsonType(expression.getVariableName());
} else if (globalVariables.hasVariable(expression.getVariable())) {
- return modernjson::json(globalVariables.getVariable(expression.getVariable()).getName());
+ return ExportJsonType(globalVariables.getVariable(expression.getVariable()).getName());
} else if (localVariables.hasVariable(expression.getVariable())) {
- return modernjson::json(localVariables.getVariable(expression.getVariable()).getName());
+ return ExportJsonType(localVariables.getVariable(expression.getVariable()).getName());
} else {
for (auto const& constant : constants) {
if (constant.getExpressionVariable() == expression.getVariable()) {
- return modernjson::json(constant.getName());
+ return ExportJsonType(constant.getName());
}
}
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Expression variable '" << expression.getVariableName() << "' not known in Jani data structures.");
- return modernjson::json(); // should not reach this point.
+ return ExportJsonType(); // should not reach this point.
}
boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data));
return opDecl;
}
boost::any ExpressionToJson::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data));
return opDecl;
}
boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) {
- return modernjson::json(expression.getValue());
+ return ExportJsonType(expression.getValue());
}
boost::any ExpressionToJson::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) {
- return modernjson::json(expression.getValue());
+ return ExportJsonType(expression.getValue());
}
boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) {
- return modernjson::json(expression.getValueAsDouble());
+ return ExportJsonType(expression.getValueAsDouble());
}
boost::any ExpressionToJson::visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "av";
- std::vector<modernjson::json> elements;
+ std::vector<ExportJsonType> elements;
uint64_t size = expression.size()->evaluateAsInt();
for (uint64_t i = 0; i < size; ++i) {
elements.push_back(anyToJson(expression.at(i)->accept(*this, data)));
@@ -706,7 +706,7 @@ namespace storm {
}
boost::any ExpressionToJson::visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "ac";
opDecl["var"] = expression.getIndexVar().getName();
opDecl["length"] = anyToJson(expression.size()->accept(*this, data));
@@ -719,7 +719,7 @@ namespace storm {
}
boost::any ExpressionToJson::visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "aa";
opDecl["exp"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["index"] = anyToJson(expression.getOperand(1)->accept(*this, data));
@@ -727,10 +727,10 @@ namespace storm {
}
boost::any ExpressionToJson::visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) {
- modernjson::json opDecl;
+ ExportJsonType opDecl;
opDecl["op"] = "call";
opDecl["function"] = expression.getFunctionIdentifier();
- std::vector<modernjson::json> arguments;
+ std::vector<ExportJsonType> arguments;
for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) {
arguments.push_back(anyToJson(expression.getArgument(i)->accept(*this, data)));
}
@@ -766,8 +766,8 @@ namespace storm {
STORM_LOG_INFO("Conversion completed " << janiModel.getName() << ".");
}
- modernjson::json buildActionArray(std::vector<storm::jani::Action> const& actions) {
- std::vector<modernjson::json> actionReprs;
+ ExportJsonType buildActionArray(std::vector<storm::jani::Action> const& actions) {
+ std::vector<ExportJsonType> actionReprs;
uint64_t actIndex = 0;
for(auto const& act : actions) {
if(actIndex == storm::jani::Model::SILENT_ACTION_INDEX) {
@@ -775,17 +775,17 @@ namespace storm {
continue;
}
actIndex++;
- modernjson::json actEntry;
+ ExportJsonType actEntry;
actEntry["name"] = act.getName();
actionReprs.push_back(actEntry);
}
- return modernjson::json(actionReprs);
+ return ExportJsonType(actionReprs);
}
- modernjson::json buildTypeDescription(storm::expressions::Type const& type) {
- modernjson::json typeDescr;
+ ExportJsonType buildTypeDescription(storm::expressions::Type const& type) {
+ ExportJsonType typeDescr;
if (type.isIntegerType()) {
typeDescr = "int";
} else if (type.isRationalType()) {
@@ -801,7 +801,7 @@ namespace storm {
return typeDescr;
}
- void getBoundsFromConstraints(modernjson::json& typeDesc, storm::expressions::Variable const& var, storm::expressions::Expression const& constraint, std::vector<storm::jani::Constant> const& constants) {
+ void getBoundsFromConstraints(ExportJsonType& typeDesc, storm::expressions::Variable const& var, storm::expressions::Expression const& constraint, std::vector<storm::jani::Constant> const& constants) {
if (constraint.getBaseExpression().isBinaryBooleanFunctionExpression() && constraint.getBaseExpression().getOperator() == storm::expressions::OperatorType::And) {
getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(0), constants);
getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(1), constants);
@@ -825,12 +825,12 @@ namespace storm {
}
}
- modernjson::json buildConstantsArray(std::vector<storm::jani::Constant> const& constants) {
- std::vector<modernjson::json> constantDeclarations;
+ ExportJsonType buildConstantsArray(std::vector<storm::jani::Constant> const& constants) {
+ std::vector<ExportJsonType> constantDeclarations;
for(auto const& constant : constants) {
- modernjson::json constantEntry;
+ ExportJsonType constantEntry;
constantEntry["name"] = constant.getName();
- modernjson::json typeDesc;
+ ExportJsonType typeDesc;
if (constant.hasConstraint()) {
typeDesc["kind"] = "bounded";
typeDesc["base"] = buildTypeDescription(constant.getType());
@@ -844,19 +844,19 @@ namespace storm {
}
constantDeclarations.push_back(constantEntry);
}
- return modernjson::json(constantDeclarations);
+ return ExportJsonType(constantDeclarations);
}
- modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
- modernjson::json variableDeclarations = std::vector<modernjson::json>();
+ ExportJsonType buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
+ ExportJsonType variableDeclarations = std::vector<ExportJsonType>();
for(auto const& variable : varSet) {
- modernjson::json varEntry;
+ ExportJsonType varEntry;
varEntry["name"] = variable.getName();
if (variable.isTransient()) {
varEntry["transient"] = variable.isTransient();
}
- modernjson::json typeDesc;
+ ExportJsonType typeDesc;
if(variable.isBooleanVariable()) {
typeDesc = "bool";
} else if (variable.isRealVariable()) {
@@ -879,7 +879,7 @@ namespace storm {
break;
case storm::jani::ArrayVariable::ElementType::Int:
if (variable.asArrayVariable().hasElementTypeBound()) {
- modernjson::json baseTypeDescr;
+ ExportJsonType baseTypeDescr;
baseTypeDescr["kind"] = "bounded";
baseTypeDescr["base "] = "int";
if (variable.asArrayVariable().hasLowerElementTypeBound()) {
@@ -907,17 +907,17 @@ namespace storm {
return variableDeclarations;
}
- modernjson::json buildFunctionsArray(std::unordered_map<std::string, FunctionDefinition> const& functionDefinitions, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
- modernjson::json functionDeclarations = std::vector<modernjson::json>();
+ ExportJsonType buildFunctionsArray(std::unordered_map<std::string, FunctionDefinition> const& functionDefinitions, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
+ ExportJsonType functionDeclarations = std::vector<ExportJsonType>();
for (auto const& nameFunDef : functionDefinitions) {
storm::jani::FunctionDefinition const& funDef = nameFunDef.second;
- modernjson::json funDefJson;
+ ExportJsonType funDefJson;
funDefJson["name"] = nameFunDef.first;
funDefJson["type"] = buildTypeDescription(funDef.getType());
- std::vector<modernjson::json> parameterDeclarations;
+ std::vector<ExportJsonType> parameterDeclarations;
std::unordered_set<std::string> parameterNames;
for (auto const& p : funDef.getParameters()) {
- modernjson::json parDefJson;
+ ExportJsonType parDefJson;
parDefJson["name"] = p.getName();
parameterNames.insert(p.getName());
parDefJson["type"] = buildTypeDescription(p.getType());
@@ -930,16 +930,16 @@ namespace storm {
return functionDeclarations;
}
- modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
- modernjson::json assignmentDeclarations = std::vector<modernjson::json>();
+ ExportJsonType buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
+ ExportJsonType assignmentDeclarations = std::vector<ExportJsonType>();
bool addIndex = orderedAssignments.hasMultipleLevels();
for(auto const& assignment : orderedAssignments) {
- modernjson::json assignmentEntry;
+ ExportJsonType assignmentEntry;
if (assignment.getLValue().isVariable()) {
assignmentEntry["ref"] = assignment.getVariable().getName();
} else {
STORM_LOG_ASSERT(assignment.getLValue().isArrayAccess(), "Unhandled LValue " << assignment.getLValue());
- modernjson::json arrayAccess;
+ ExportJsonType arrayAccess;
arrayAccess["op"] = "aa";
arrayAccess["exp"] = assignment.getLValue().getArray().getName();
arrayAccess["index"] = buildExpression(assignment.getLValue().getArrayIndex(), constants, globalVariables, localVariables);
@@ -957,13 +957,13 @@ namespace storm {
return assignmentDeclarations;
}
- modernjson::json buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
- modernjson::json locationDeclarations = std::vector<modernjson::json>();
+ ExportJsonType buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
+ ExportJsonType locationDeclarations = std::vector<ExportJsonType>();
for(auto const& location : locations) {
- modernjson::json locEntry;
+ ExportJsonType locEntry;
locEntry["name"] = location.getName();
if (location.hasTimeProgressInvariant()) {
- modernjson::json timeProg;
+ ExportJsonType timeProg;
timeProg["exp"] = buildExpression(location.getTimeProgressInvariant(), constants, globalVariables, localVariables);
if (commentExpressions) {
timeProg["comment"] = location.getTimeProgressInvariant().toString();
@@ -978,19 +978,19 @@ namespace storm {
return locationDeclarations;
}
- modernjson::json buildInitialLocations(storm::jani::Automaton const& automaton) {
+ ExportJsonType buildInitialLocations(storm::jani::Automaton const& automaton) {
std::vector<std::string> names;
for(auto const& initLocIndex : automaton.getInitialLocationIndices()) {
names.push_back(automaton.getLocation(initLocIndex).getName());
}
- return modernjson::json(names);
+ return ExportJsonType(names);
}
- modernjson::json buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
+ ExportJsonType buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
assert(destinations.size() > 0);
- modernjson::json destDeclarations = std::vector<modernjson::json>();
+ ExportJsonType destDeclarations = std::vector<ExportJsonType>();
for(auto const& destination : destinations) {
- modernjson::json destEntry;
+ ExportJsonType destEntry;
destEntry["location"] = locationNames.at(destination.getLocationIndex());
bool prob1 = false;
if(destination.getProbability().isLiteral()) {
@@ -1012,14 +1012,14 @@ namespace storm {
return destDeclarations;
}
- modernjson::json buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
- modernjson::json edgeDeclarations = std::vector<modernjson::json>();
+ ExportJsonType buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
+ ExportJsonType edgeDeclarations = std::vector<ExportJsonType>();
for(auto const& edge : edges) {
if (edge.getGuard().isFalse()) {
continue;
}
STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed.");
- modernjson::json edgeEntry;
+ ExportJsonType edgeEntry;
edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex());
if(!edge.hasSilentAction()) {
edgeEntry["action"] = actionNames.at(edge.getActionIndex());
@@ -1046,10 +1046,10 @@ namespace storm {
return edgeDeclarations;
}
- modernjson::json buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, bool commentExpressions) {
- modernjson::json automataDeclarations = std::vector<modernjson::json>();
+ ExportJsonType buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, bool commentExpressions) {
+ ExportJsonType automataDeclarations = std::vector<ExportJsonType>();
for(auto const& automaton : automata) {
- modernjson::json autoEntry;
+ ExportJsonType autoEntry;
autoEntry["name"] = automaton.getName();
autoEntry["variables"] = buildVariablesArray(automaton.getVariables(), constants, globalVariables, automaton.getVariables());
if (!automaton.getFunctionDefinitions().empty()) {
@@ -1108,8 +1108,8 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType");
}
- modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
- modernjson::json propDecl;
+ ExportJsonType convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
+ ExportJsonType propDecl;
propDecl["states"]["op"] = "initial";
propDecl["op"] = "filter";
propDecl["fun"] = janiFilterTypeString(fe.getFilterType());
@@ -1119,18 +1119,18 @@ namespace storm {
void JsonExporter::convertProperties( std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model) {
- modernjson::json properties;
+ ExportJsonType properties;
// Unset model-features that only relate to properties. These are only set if such properties actually exist.
modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards);
if (formulas.empty()) {
- jsonStruct["properties"] = modernjson::json(modernjson::json::value_t::array);
+ jsonStruct["properties"] = ExportJsonType(ExportJsonType::value_t::array);
return;
}
uint64_t index = 0;
for(auto const& f : formulas) {
- modernjson::json propDecl;
+ ExportJsonType propDecl;
propDecl["name"] = f.getName();
propDecl["expression"] = convertFilterExpression(f.getFilter(), model, modelFeatures);
++index;
@@ -1139,8 +1139,8 @@ namespace storm {
jsonStruct["properties"] = std::move(properties);
}
- modernjson::json JsonExporter::finalize() {
- jsonStruct["features"] = modernjson::json::parse(modelFeatures.toString());
+ ExportJsonType JsonExporter::finalize() {
+ jsonStruct["features"] = ExportJsonType::parse(modelFeatures.toString());
return jsonStruct;
}
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index 9a99a443a..ba2489b03 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -7,19 +7,17 @@
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/Property.h"
#include "storm/adapters/RationalNumberAdapter.h"
-// JSON parser
-#include "json.hpp"
-namespace modernjson {
- using json = nlohmann::json;
-}
+#include "storm/adapters/JsonAdapter.h"
namespace storm {
namespace jani {
+
+ typedef storm::json<double> ExportJsonType;
class ExpressionToJson : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor {
public:
- static modernjson::json translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables);
+ static ExportJsonType translate(storm::expressions::Expression const& expr, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set<std::string> const& auxiliaryVariables);
virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data);
virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data);
@@ -48,7 +46,7 @@ namespace storm {
class FormulaToJaniJson : public storm::logic::FormulaVisitor {
public:
- static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures);
+ static ExportJsonType translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures);
bool containsStateExitRewards() const; // Returns true iff the previously translated formula contained state exit rewards
virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
@@ -75,20 +73,19 @@ namespace storm {
private:
FormulaToJaniJson(storm::jani::Model const& model) : model(model), stateExitRewards(false) { }
- modernjson::json constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const;
+ ExportJsonType constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const;
- modernjson::json constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const;
- modernjson::json constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const;
- modernjson::json constructStandardRewardAccumulation(std::string const& rewardModelName) const;
+ ExportJsonType constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const;
+ ExportJsonType constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const;
+ ExportJsonType constructStandardRewardAccumulation(std::string const& rewardModelName) const;
storm::jani::Model const& model;
mutable bool stateExitRewards;
};
class JsonExporter {
- JsonExporter() = default;
-
public:
+ JsonExporter() = default;
static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false);
static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false, bool compact = false);
@@ -98,9 +95,9 @@ namespace storm {
void convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);
void appendVariableDeclaration(storm::jani::Variable const& variable);
- modernjson::json finalize();
+ ExportJsonType finalize();
- modernjson::json jsonStruct;
+ ExportJsonType jsonStruct;
storm::jani::ModelFeatures modelFeatures;
};