sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Replaced remaining uses of modernjson::json with the new storm::json<..>

main
Tim Quatmann 5 years ago
parent
328b9c6986
commit
6af6bc5472
10 changed files with 189 additions and 205 deletions
Unified View
  1. 18
      src/storm-dft/parser/DFTJsonParser.cpp
  2. 12
      src/storm-dft/parser/DFTJsonParser.h
  3. 14
      src/storm-dft/storage/dft/DftJsonExporter.cpp
  4. 14
      src/storm-dft/storage/dft/DftJsonExporter.h
  5. 52
      src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
  6. 17
      src/storm-gspn/storage/gspn/GspnJsonExporter.h
  7. 9
      src/storm/storage/Qvbs.cpp
  8. 9
      src/storm/storage/Qvbs.h
  9. 222
      src/storm/storage/jani/JSONExporter.cpp
  10. 27
      src/storm/storage/jani/JSONExporter.h

18
src/storm-dft/parser/DFTJsonParser.cpp
View File

@ -21,7 +21,7 @@ namespace storm {
STORM_LOG_DEBUG("Parsing from JSON file"); STORM_LOG_DEBUG("Parsing from JSON file");
std::ifstream file; std::ifstream file;
storm::utility::openFile(filename, file); storm::utility::openFile(filename, file);
json jsonInput; Json jsonInput;
jsonInput << file; jsonInput << file;
storm::utility::closeFile(file); storm::utility::closeFile(file);
return parseJson(jsonInput); return parseJson(jsonInput);
@ -30,19 +30,19 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJsonFromString(std::string const& jsonString) { storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJsonFromString(std::string const& jsonString) {
STORM_LOG_DEBUG("Parsing from JSON string"); STORM_LOG_DEBUG("Parsing from JSON string");
json jsonInput = json::parse(jsonString); Json jsonInput = Json::parse(jsonString);
return parseJson(jsonInput); return parseJson(jsonInput);
} }
template<typename ValueType> 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 // Init DFT builder and value parser
storm::builder::DFTBuilder<ValueType> builder; storm::builder::DFTBuilder<ValueType> builder;
ValueParser<ValueType> valueParser; ValueParser<ValueType> valueParser;
// Try to parse parameters // Try to parse parameters
if (jsonInput.find("parameters") != jsonInput.end()) { 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, STORM_LOG_THROW(parameters.empty() || (std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException,
"Parameters only allowed when using rational functions."); "Parameters only allowed when using rational functions.");
for (auto it = parameters.begin(); it != parameters.end(); ++it) { 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 // Start by building mapping from ids to their unique names
std::map<std::string, std::string> nameMapping; std::map<std::string, std::string> nameMapping;
std::set<std::string> names; std::set<std::string> names;
for (auto& element : nodes) { for (auto& element : nodes) {
json data = element.at("data"); Json data = element.at("data");
std::string id = data.at("id"); std::string id = data.at("id");
std::string uniqueName = generateUniqueName(data.at("name")); std::string uniqueName = generateUniqueName(data.at("name"));
STORM_LOG_THROW(names.find(uniqueName) == names.end(), storm::exceptions::WrongFormatException, "Element '" << uniqueName << "' was already declared."); 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) { for (auto& element : nodes) {
STORM_LOG_TRACE("Parsing: " << element); STORM_LOG_TRACE("Parsing: " << element);
bool success = true; bool success = true;
json data = element.at("data"); Json data = element.at("data");
std::string name = generateUniqueName(data.at("name")); std::string name = generateUniqueName(data.at("name"));
std::vector<std::string> childNames; std::vector<std::string> childNames;
if (data.count("children") > 0) { if (data.count("children") > 0) {
@ -137,7 +137,7 @@ namespace storm {
// TODO: do splitting later in rewriting step // TODO: do splitting later in rewriting step
if (type != "fdep" && type != "pdep") { if (type != "fdep" && type != "pdep") {
// Set layout positions // Set layout positions
json position = element.at("position"); Json position = element.at("position");
double x = position.at("x"); double x = position.at("x");
double y = position.at("y"); double y = position.at("y");
builder.addLayoutInfo(name, x / 7, y / 7); builder.addLayoutInfo(name, x / 7, y / 7);
@ -171,7 +171,7 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
std::string DFTJsonParser<ValueType>::parseJsonNumber(json number) { std::string DFTJsonParser<ValueType>::parseJsonNumber(Json number) {
if (number.is_string()) { if (number.is_string()) {
return number.get<std::string>(); return number.get<std::string>();
} else { } else {

12
src/storm-dft/parser/DFTJsonParser.h
View File

@ -4,18 +4,14 @@
#include "storm-dft/storage/dft/DFT.h" #include "storm-dft/storage/dft/DFT.h"
#include "storm-dft/builder/DFTBuilder.h" #include "storm-dft/builder/DFTBuilder.h"
#include "storm/adapters/JsonAdapter.h"
// JSON parser
#include "json.hpp"
using json = nlohmann::json;
namespace storm { namespace storm {
namespace parser { namespace parser {
template<typename ValueType> template<typename ValueType>
class DFTJsonParser { class DFTJsonParser {
typedef typename storm::json<double> Json;
public: public:
static storm::storage::DFT<ValueType> parseJsonFromString(std::string const& jsonString); 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); static storm::storage::DFT<ValueType> parseJsonFromFile(std::string const& filename);
private: 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 generateUniqueName(std::string const& name);
static std::string parseJsonNumber(json number); static std::string parseJsonNumber(Json number);
}; };
} }
} }

14
src/storm-dft/storage/dft/DftJsonExporter.cpp
View File

@ -24,23 +24,23 @@ namespace storm {
} }
template<typename ValueType> 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 // Nodes
modernjson::json jsonNodes; Json jsonNodes;
for (size_t i = 0; i < dft.nrElements(); ++i) { 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); jsonNodes.push_back(jsonNode);
} }
modernjson::json jsonDft; Json jsonDft;
jsonDft["toplevel"] = std::to_string(dft.getTopLevelIndex()); jsonDft["toplevel"] = std::to_string(dft.getTopLevelIndex());
jsonDft["nodes"] = jsonNodes; jsonDft["nodes"] = jsonNodes;
return jsonDft; return jsonDft;
} }
template<typename ValueType> template<typename ValueType>
modernjson::json DftJsonExporter<ValueType>::translateNode(DFTElementCPointer const& element) { typename DftJsonExporter<ValueType>::Json DftJsonExporter<ValueType>::translateNode(DFTElementCPointer const& element) {
modernjson::json nodeData; Json nodeData;
nodeData["id"] = std::to_string(element->id()); nodeData["id"] = std::to_string(element->id());
nodeData["name"] = element->name(); nodeData["name"] = element->name();
std::string type = storm::storage::toString(element->type()); 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."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Element of type '" << element->type() << "' is not supported.");
} }
modernjson::json jsonNode; Json jsonNode;
jsonNode["data"] = nodeData; jsonNode["data"] = nodeData;
jsonNode["group"] = "nodes"; jsonNode["group"] = "nodes";
jsonNode["classes"] = type; jsonNode["classes"] = type;

14
src/storm-dft/storage/dft/DftJsonExporter.h
View File

@ -3,12 +3,7 @@
#include "storm/utility/macros.h" #include "storm/utility/macros.h"
#include "storm-dft/storage/dft/DFT.h" #include "storm-dft/storage/dft/DFT.h"
#include "storm/adapters/JsonAdapter.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>;
}
namespace storm { namespace storm {
namespace storage { namespace storage {
@ -18,7 +13,8 @@ namespace storm {
*/ */
template<typename ValueType> template<typename ValueType>
class DftJsonExporter { class DftJsonExporter {
typedef typename storm::json<double> Json;
using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>; using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
using DFTElementCPointer = std::shared_ptr<DFTElement<ValueType> const>; using DFTElementCPointer = std::shared_ptr<DFTElement<ValueType> const>;
using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>; using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
@ -31,9 +27,9 @@ namespace storm {
private: 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);
}; };
} }

52
src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
View File

@ -17,8 +17,8 @@ namespace storm {
os << translate(gspn).dump(4) << std::endl; os << translate(gspn).dump(4) << std::endl;
} }
modernjson::json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) { typename GspnJsonExporter::Json GspnJsonExporter::translate(storm::gspn::GSPN const& gspn) {
modernjson::json jsonGspn; Json jsonGspn;
// Layouts // Layouts
std::map<uint64_t, LayoutInfo> placeLayout = gspn.getPlaceLayoutInfos(); std::map<uint64_t, LayoutInfo> placeLayout = gspn.getPlaceLayoutInfos();
@ -35,7 +35,7 @@ namespace storm {
y = placeLayout.at(place.getID()).y; y = placeLayout.at(place.getID()).y;
} }
tmpX += 3; tmpX += 3;
modernjson::json jsonPlace = translatePlace(place, x, y); Json jsonPlace = translatePlace(place, x, y);
jsonGspn.push_back(jsonPlace); jsonGspn.push_back(jsonPlace);
} }
@ -48,7 +48,7 @@ namespace storm {
y = transitionLayout.at(transition.getID()).y; y = transitionLayout.at(transition.getID()).y;
} }
tmpX += 3; tmpX += 3;
modernjson::json jsonImmediateTransition = translateImmediateTransition(transition, x, y); Json jsonImmediateTransition = translateImmediateTransition(transition, x, y);
jsonGspn.push_back(jsonImmediateTransition); jsonGspn.push_back(jsonImmediateTransition);
} }
@ -61,7 +61,7 @@ namespace storm {
y = transitionLayout.at(transition.getID()).y; y = transitionLayout.at(transition.getID()).y;
} }
tmpX += 3; tmpX += 3;
modernjson::json jsonTimedTransition = translateTimedTransition(transition, x, y); Json jsonTimedTransition = translateTimedTransition(transition, x, y);
jsonGspn.push_back(jsonTimedTransition); jsonGspn.push_back(jsonTimedTransition);
} }
@ -72,21 +72,21 @@ namespace storm {
// Export input arcs // Export input arcs
for (auto const& entry : transition.getInputPlaces()) { for (auto const& entry : transition.getInputPlaces()) {
storm::gspn::Place place = places.at(entry.first); 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); jsonGspn.push_back(jsonInputArc);
} }
// Export inhibitor arcs // Export inhibitor arcs
for (auto const& entry : transition.getInhibitionPlaces()) { for (auto const& entry : transition.getInhibitionPlaces()) {
storm::gspn::Place place = places.at(entry.first); 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); jsonGspn.push_back(jsonInputArc);
} }
// Export output arcs // Export output arcs
for (auto const& entry : transition.getOutputPlaces()) { for (auto const& entry : transition.getOutputPlaces()) {
storm::gspn::Place place = places.at(entry.first); 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); jsonGspn.push_back(jsonInputArc);
} }
} }
@ -95,21 +95,21 @@ namespace storm {
// Export input arcs // Export input arcs
for (auto const& entry : transition.getInputPlaces()) { for (auto const& entry : transition.getInputPlaces()) {
storm::gspn::Place place = places.at(entry.first); 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); jsonGspn.push_back(jsonInputArc);
} }
// Export inhibitor arcs // Export inhibitor arcs
for (auto const& entry : transition.getInhibitionPlaces()) { for (auto const& entry : transition.getInhibitionPlaces()) {
storm::gspn::Place place = places.at(entry.first); 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); jsonGspn.push_back(jsonInputArc);
} }
// Export output arcs // Export output arcs
for (auto const& entry : transition.getOutputPlaces()) { for (auto const& entry : transition.getOutputPlaces()) {
storm::gspn::Place place = places.at(entry.first); 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); jsonGspn.push_back(jsonInputArc);
} }
} }
@ -117,17 +117,17 @@ namespace storm {
} }
modernjson::json GspnJsonExporter::translatePlace(storm::gspn::Place const& place, double x, double y) { typename GspnJsonExporter::Json GspnJsonExporter::translatePlace(storm::gspn::Place const& place, double x, double y) {
modernjson::json data; Json data;
data["id"] = toJsonString(place); data["id"] = toJsonString(place);
data["name"] = place.getName(); data["name"] = place.getName();
data["marking"] = place.getNumberOfInitialTokens(); data["marking"] = place.getNumberOfInitialTokens();
modernjson::json position; Json position;
position["x"] = x * scaleFactor; position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor; position["y"] = y * scaleFactor;
modernjson::json jsonPlace; Json jsonPlace;
jsonPlace["data"] = data; jsonPlace["data"] = data;
jsonPlace["position"] = position; jsonPlace["position"] = position;
jsonPlace["group"] = "nodes"; jsonPlace["group"] = "nodes";
@ -135,18 +135,18 @@ namespace storm {
return jsonPlace; return jsonPlace;
} }
modernjson::json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y) { typename GspnJsonExporter::Json GspnJsonExporter::translateImmediateTransition(storm::gspn::ImmediateTransition<double> const& transition, double x, double y) {
modernjson::json data; Json data;
data["id"] = toJsonString(transition, true); data["id"] = toJsonString(transition, true);
data["name"] = transition.getName(); data["name"] = transition.getName();
data["priority"] = transition.getPriority(); data["priority"] = transition.getPriority();
data["weight"] = transition.getWeight(); data["weight"] = transition.getWeight();
modernjson::json position; Json position;
position["x"] = x * scaleFactor; position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor; position["y"] = y * scaleFactor;
modernjson::json jsonTrans; Json jsonTrans;
jsonTrans["data"] = data; jsonTrans["data"] = data;
jsonTrans["position"] = position; jsonTrans["position"] = position;
jsonTrans["group"] = "nodes"; jsonTrans["group"] = "nodes";
@ -154,8 +154,8 @@ namespace storm {
return jsonTrans; return jsonTrans;
} }
modernjson::json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y) { typename GspnJsonExporter::Json GspnJsonExporter::translateTimedTransition(storm::gspn::TimedTransition<double> const& transition, double x, double y) {
modernjson::json data; Json data;
data["id"] = toJsonString(transition, false); data["id"] = toJsonString(transition, false);
data["name"] = transition.getName(); data["name"] = transition.getName();
data["rate"] = transition.getRate(); data["rate"] = transition.getRate();
@ -170,11 +170,11 @@ namespace storm {
} }
} }
modernjson::json position; Json position;
position["x"] = x * scaleFactor; position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor; position["y"] = y * scaleFactor;
modernjson::json jsonTrans; Json jsonTrans;
jsonTrans["data"] = data; jsonTrans["data"] = data;
jsonTrans["position"] = position; jsonTrans["position"] = position;
jsonTrans["group"] = "nodes"; jsonTrans["group"] = "nodes";
@ -182,14 +182,14 @@ namespace storm {
return jsonTrans; return jsonTrans;
} }
modernjson::json GspnJsonExporter::translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype) { typename GspnJsonExporter::Json GspnJsonExporter::translateArc(storm::gspn::Transition const& transition, storm::gspn::Place const& place, uint64_t multiplicity, bool immediate, ArcType arctype) {
modernjson::json data; Json data;
data["id"] = toJsonString(transition, place, arctype); data["id"] = toJsonString(transition, place, arctype);
data["source"] = toJsonString(place); data["source"] = toJsonString(place);
data["target"] = toJsonString(transition, immediate); data["target"] = toJsonString(transition, immediate);
data["mult"] = multiplicity; data["mult"] = multiplicity;
modernjson::json jsonArc; Json jsonArc;
jsonArc["data"] = data; jsonArc["data"] = data;
//jsonTrans["group"] = "nodes"; //jsonTrans["group"] = "nodes";
switch (arctype) { switch (arctype) {

17
src/storm-gspn/storage/gspn/GspnJsonExporter.h
View File

@ -4,11 +4,7 @@
#include "storm-gspn/storage/gspn/GSPN.h" #include "storm-gspn/storage/gspn/GSPN.h"
// JSON parser #include "storm/adapters/JsonAdapter.h"
#include "json.hpp"
namespace modernjson {
using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>;
}
namespace storm { namespace storm {
namespace gspn { namespace gspn {
@ -19,20 +15,21 @@ namespace storm {
class GspnJsonExporter { class GspnJsonExporter {
public: public:
typedef typename storm::json<double> Json;
static void toStream(storm::gspn::GSPN const& gspn, std::ostream& os); 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: private:
enum ArcType { INPUT, OUTPUT, INHIBITOR }; 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::string static inline toJsonString(storm::gspn::Place const& place) {
std::stringstream stream; std::stringstream stream;

9
src/storm/storage/Qvbs.cpp
View File

@ -9,13 +9,14 @@
#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/IOSettings.h"
#include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/WrongFormatException.h"
#include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidArgumentException.h"
#include "storm/utility/constants.h"
namespace storm { namespace storm {
namespace storage { 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."); 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; std::ifstream file;
storm::utility::openFile(filePath, file); storm::utility::openFile(filePath, file);
result << file; result << file;
@ -23,11 +24,11 @@ namespace storm {
return result; 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()) { if (structure.is_number_integer()) {
return std::to_string(structure.get<int64_t>()); return std::to_string(structure.get<int64_t>());
} else if (structure.is_number_float()) { } 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()) { } else if (structure.is_string()) {
return structure.get<std::string>(); return structure.get<std::string>();
} else if (structure.is_boolean()) { } else if (structure.is_boolean()) {

9
src/storm/storage/Qvbs.h
View File

@ -4,11 +4,8 @@
#include <vector> #include <vector>
#include <boost/optional.hpp> #include <boost/optional.hpp>
// JSON parser #include "storm/adapters/JsonAdapter.h"
#include "json.hpp" #include "storm/adapters/RationalNumberAdapter.h"
namespace modernjson {
using json = nlohmann::json;
}
namespace storm { namespace storm {
@ -36,7 +33,7 @@ namespace storm {
std::vector<std::string> instanceInfos; std::vector<std::string> instanceInfos;
std::string modelPath; std::string modelPath;
modernjson::json modelData; storm::json<storm::RationalNumber> modelData;
}; };
} }
} }

222
src/storm/storage/jani/JSONExporter.cpp
View File

@ -39,13 +39,13 @@
namespace storm { namespace storm {
namespace jani { namespace jani {
modernjson::json anyToJson(boost::any&& input) { ExportJsonType anyToJson(boost::any&& input) {
boost::any tmp(std::move(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; 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); STORM_LOG_TRACE("Exporting " << exp);
return ExpressionToJson::translate(exp, constants, globalVariables, localVariables, auxiliaryVariables); 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); CompositionJsonExporter visitor(allowRecursion);
return anyToJson(comp.accept(visitor, boost::none)); return anyToJson(comp.accept(visitor, boost::none));
} }
virtual boost::any visit(AutomatonComposition const& composition, boost::any const&) { virtual boost::any visit(AutomatonComposition const& composition, boost::any const&) {
modernjson::json compDecl; ExportJsonType compDecl;
modernjson::json autDecl; ExportJsonType autDecl;
autDecl["automaton"] = composition.getAutomatonName(); autDecl["automaton"] = composition.getAutomatonName();
std::vector<modernjson::json> elements; std::vector<ExportJsonType> elements;
elements.push_back(autDecl); elements.push_back(autDecl);
compDecl["elements"] = elements; compDecl["elements"] = elements;
return compDecl; return compDecl;
} }
virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) { 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()) { for (auto const& subcomp : composition.getSubcompositions()) {
modernjson::json elemDecl; ExportJsonType elemDecl;
if (subcomp->isAutomatonComposition()) { if (subcomp->isAutomatonComposition()) {
elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName(); elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
} else { } else {
@ -86,9 +86,9 @@ namespace storm {
elems.push_back(elemDecl); elems.push_back(elemDecl);
} }
compDecl["elements"] = elems; compDecl["elements"] = elems;
std::vector<modernjson::json> synElems; std::vector<ExportJsonType> synElems;
for (auto const& syncs : composition.getSynchronizationVectors()) { for (auto const& syncs : composition.getSynchronizationVectors()) {
modernjson::json syncDecl; ExportJsonType syncDecl;
syncDecl["synchronise"] = std::vector<std::string>(); syncDecl["synchronise"] = std::vector<std::string>();
for (auto const& syncIn : syncs.getInput()) { for (auto const& syncIn : syncs.getInput()) {
if (syncIn == SynchronizationVector::NO_ACTION_INPUT) { if (syncIn == SynchronizationVector::NO_ACTION_INPUT) {
@ -125,11 +125,11 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType"); STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ComparisonType");
} }
modernjson::json numberToJson(storm::RationalNumber rn) { ExportJsonType numberToJson(storm::RationalNumber rn) {
modernjson::json numDecl; ExportJsonType numDecl;
numDecl = storm::utility::convertNumber<double>(rn); numDecl = storm::utility::convertNumber<double>(rn);
// if(carl::isOne(carl::getDenom(rn))) { // if(carl::isOne(carl::getDenom(rn))) {
// numDecl = modernjson::json(carl::toString(carl::getNum(rn))); // numDecl = ExportJsonType(carl::toString(carl::getNum(rn)));
// } else { // } else {
// numDecl["op"] = "/"; // numDecl["op"] = "/";
// // TODO set json lib to work with arbitrary precision ints. // // 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() || 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((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."); 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) { if (lower) {
iDecl["lower"] = buildExpression(*lower, model.getConstants(), model.getGlobalVariables()); iDecl["lower"] = buildExpression(*lower, model.getConstants(), model.getGlobalVariables());
if (lowerExclusive) { if (lowerExclusive) {
@ -163,7 +163,7 @@ namespace storm {
return iDecl; 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); storm::jani::RewardModelInformation info(model, rewardModelName);
bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards()); bool steps = rewardAccumulation.isStepsSet() && (info.hasActionRewards() || info.hasTransitionRewards());
@ -173,7 +173,7 @@ namespace storm {
return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit)); 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; std::vector<std::string> res;
if (rewardAccumulation.isStepsSet()) { if (rewardAccumulation.isStepsSet()) {
res.push_back("steps"); res.push_back("steps");
@ -188,7 +188,7 @@ namespace storm {
return res; return res;
} }
modernjson::json FormulaToJaniJson::constructStandardRewardAccumulation(std::string const& rewardModelName) const { ExportJsonType FormulaToJaniJson::constructStandardRewardAccumulation(std::string const& rewardModelName) const {
if (model.isDiscreteTimeModel()) { if (model.isDiscreteTimeModel()) {
return constructRewardAccumulation(storm::logic::RewardAccumulation(true, false, true), rewardModelName); return constructRewardAccumulation(storm::logic::RewardAccumulation(true, false, true), rewardModelName);
} else { } 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); FormulaToJaniJson translator(model);
auto result = anyToJson(formula.accept(translator)); auto result = anyToJson(formula.accept(translator));
if (translator.containsStateExitRewards()) { if (translator.containsStateExitRewards()) {
@ -214,11 +214,11 @@ namespace storm {
} }
boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const&) const {
modernjson::json opDecl(f.getLabel()); ExportJsonType opDecl(f.getLabel());
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{ 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(); storm::logic::BinaryBooleanStateFormula::OperatorType op = f.getOperator();
opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "∧" : "∨"; opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "∧" : "∨";
opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data)); opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data));
@ -226,18 +226,18 @@ namespace storm {
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const&) const { 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; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { 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."); 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["op"] = "U";
opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data)); opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data));
opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data)); opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data));
bool hasStepBounds(false), hasTimeBounds(false); bool hasStepBounds(false), hasTimeBounds(false);
std::vector<modernjson::json> rewardBounds; std::vector<ExportJsonType> rewardBounds;
for (uint64_t i = 0; i < f.getDimension(); ++i) { for (uint64_t i = 0; i < f.getDimension(); ++i) {
boost::optional<storm::expressions::Expression> lower, upper; boost::optional<storm::expressions::Expression> lower, upper;
@ -250,7 +250,7 @@ namespace storm {
upper = f.getUpperBound(i); upper = f.getUpperBound(i);
upperExclusive = f.isUpperBoundStrict(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); auto tbr = f.getTimeBoundReference(i);
if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) { if (tbr.isStepBound() || (model.isDiscreteTimeModel() && tbr.isTimeBound())) {
@ -258,7 +258,7 @@ namespace storm {
hasStepBounds = true; hasStepBounds = true;
opDecl["step-bounds"] = propertyInterval; opDecl["step-bounds"] = propertyInterval;
} else if(tbr.isRewardBound()) { } else if(tbr.isRewardBound()) {
modernjson::json rewbound; ExportJsonType rewbound;
rewbound["exp"] = buildExpression(model.getRewardModelExpression(tbr.getRewardName()), model.getConstants(), model.getGlobalVariables()); rewbound["exp"] = buildExpression(model.getRewardModelExpression(tbr.getRewardName()), model.getConstants(), model.getGlobalVariables());
if (tbr.hasRewardAccumulation()) { if (tbr.hasRewardAccumulation()) {
rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName()); rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName());
@ -274,7 +274,7 @@ namespace storm {
} }
} }
if (!rewardBounds.empty()) { if (!rewardBounds.empty()) {
opDecl["reward-bounds"] = modernjson::json(rewardBounds); opDecl["reward-bounds"] = ExportJsonType(rewardBounds);
} }
return opDecl; return opDecl;
@ -289,7 +289,7 @@ namespace storm {
} }
boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "U"; opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getTrueFormula()->accept(*this, data)); opDecl["left"] = anyToJson(f.getTrueFormula()->accept(*this, data));
opDecl["right"] = anyToJson(f.getSubformula().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 { 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. // Create standard reward accumulation for time operator formulas.
storm::logic::RewardAccumulation rewAcc(model.isDiscreteTimeModel(), !model.isDiscreteTimeModel(), false); 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"]["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"]["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["left"]["accumulate"] = rewAccJson;
opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables()); opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables());
} else { } else {
@ -336,14 +336,14 @@ namespace storm {
opDecl["op"] = "Emin"; opDecl["op"] = "Emin";
opDecl["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); opDecl["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
} }
opDecl["exp"] = modernjson::json(1); opDecl["exp"] = ExportJsonType(1);
opDecl["accumulate"] = rewAccJson; opDecl["accumulate"] = rewAccJson;
} }
return opDecl; return opDecl;
} }
boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "G"; opDecl["op"] = "G";
opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data));
return opDecl; return opDecl;
@ -354,7 +354,7 @@ namespace storm {
} }
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl; ExportJsonType opDecl;
if(f.hasBound()) { if(f.hasBound()) {
auto bound = f.getBound(); auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType); opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
@ -381,7 +381,7 @@ namespace storm {
} }
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const&, boost::any const&) const { boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const&, boost::any const&) const {
// modernjson::json opDecl; // ExportJsonType opDecl;
// if(f.()) { // if(f.()) {
// auto bound = f.getBound(); // auto bound = f.getBound();
// opDecl["op"] = comparisonTypeToJani(bound.comparisonType); // 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 { boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "U"; opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getTrueFormula()->accept(*this, data)); opDecl["left"] = anyToJson(f.getTrueFormula()->accept(*this, data));
opDecl["right"] = anyToJson(f.getSubformula().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 { boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl; ExportJsonType opDecl;
if(f.hasBound()) { if(f.hasBound()) {
auto bound = f.getBound(); auto bound = f.getBound();
@ -460,7 +460,7 @@ namespace storm {
} }
boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl; ExportJsonType opDecl;
std::string instantName; std::string instantName;
if (model.isDiscreteTimeModel()) { if (model.isDiscreteTimeModel()) {
@ -529,7 +529,7 @@ namespace storm {
opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables());
if(f.hasBound()) { if(f.hasBound()) {
modernjson::json compDecl; ExportJsonType compDecl;
auto bound = f.getBound(); auto bound = f.getBound();
compDecl["op"] = comparisonTypeToJani(bound.comparisonType); compDecl["op"] = comparisonTypeToJani(bound.comparisonType);
compDecl["left"] = std::move(opDecl); 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 { 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(); storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator();
assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not); assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
opDecl["op"] = "¬"; opDecl["op"] = "¬";
@ -554,7 +554,7 @@ namespace storm {
} }
boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "U"; opDecl["op"] = "U";
opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data)); opDecl["left"] = anyToJson(f.getLeftSubformula().accept(*this, data));
opDecl["right"] = anyToJson(f.getRightSubformula().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 // Simplify the expression first and reduce the nesting
auto simplifiedExpr = storm::jani::reduceNestingInJaniExpression(expr.simplify()); 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) { boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "ite"; opDecl["op"] = "ite";
opDecl["if"] = anyToJson(expression.getCondition()->accept(*this, data)); opDecl["if"] = anyToJson(expression.getCondition()->accept(*this, data));
opDecl["then"] = anyToJson(expression.getThenExpression()->accept(*this, data)); opDecl["then"] = anyToJson(expression.getThenExpression()->accept(*this, data));
@ -634,21 +634,21 @@ namespace storm {
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data)); opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data)); opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data));
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data)); opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data)); opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data));
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data)); opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->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&) { boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const&) {
if (auxiliaryVariables.count(expression.getVariableName())) { if (auxiliaryVariables.count(expression.getVariableName())) {
return modernjson::json(expression.getVariableName()); return ExportJsonType(expression.getVariableName());
} else if (globalVariables.hasVariable(expression.getVariable())) { } 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())) { } else if (localVariables.hasVariable(expression.getVariable())) {
return modernjson::json(localVariables.getVariable(expression.getVariable()).getName()); return ExportJsonType(localVariables.getVariable(expression.getVariable()).getName());
} else { } else {
for (auto const& constant : constants) { for (auto const& constant : constants) {
if (constant.getExpressionVariable() == expression.getVariable()) { 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."); 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) { boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data)); opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data));
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) { boost::any ExpressionToJson::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data)); opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data));
return opDecl; return opDecl;
} }
boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) { 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&) { 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&) { 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) { boost::any ExpressionToJson::visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "av"; opDecl["op"] = "av";
std::vector<modernjson::json> elements; std::vector<ExportJsonType> elements;
uint64_t size = expression.size()->evaluateAsInt(); uint64_t size = expression.size()->evaluateAsInt();
for (uint64_t i = 0; i < size; ++i) { for (uint64_t i = 0; i < size; ++i) {
elements.push_back(anyToJson(expression.at(i)->accept(*this, data))); 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) { boost::any ExpressionToJson::visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "ac"; opDecl["op"] = "ac";
opDecl["var"] = expression.getIndexVar().getName(); opDecl["var"] = expression.getIndexVar().getName();
opDecl["length"] = anyToJson(expression.size()->accept(*this, data)); 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) { boost::any ExpressionToJson::visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "aa"; opDecl["op"] = "aa";
opDecl["exp"] = anyToJson(expression.getOperand(0)->accept(*this, data)); opDecl["exp"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["index"] = anyToJson(expression.getOperand(1)->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) { boost::any ExpressionToJson::visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) {
modernjson::json opDecl; ExportJsonType opDecl;
opDecl["op"] = "call"; opDecl["op"] = "call";
opDecl["function"] = expression.getFunctionIdentifier(); opDecl["function"] = expression.getFunctionIdentifier();
std::vector<modernjson::json> arguments; std::vector<ExportJsonType> arguments;
for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) { for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) {
arguments.push_back(anyToJson(expression.getArgument(i)->accept(*this, data))); arguments.push_back(anyToJson(expression.getArgument(i)->accept(*this, data)));
} }
@ -766,8 +766,8 @@ namespace storm {
STORM_LOG_INFO("Conversion completed " << janiModel.getName() << "."); STORM_LOG_INFO("Conversion completed " << janiModel.getName() << ".");
} }
modernjson::json buildActionArray(std::vector<storm::jani::Action> const& actions) { ExportJsonType buildActionArray(std::vector<storm::jani::Action> const& actions) {
std::vector<modernjson::json> actionReprs; std::vector<ExportJsonType> actionReprs;
uint64_t actIndex = 0; uint64_t actIndex = 0;
for(auto const& act : actions) { for(auto const& act : actions) {
if(actIndex == storm::jani::Model::SILENT_ACTION_INDEX) { if(actIndex == storm::jani::Model::SILENT_ACTION_INDEX) {
@ -775,17 +775,17 @@ namespace storm {
continue; continue;
} }
actIndex++; actIndex++;
modernjson::json actEntry; ExportJsonType actEntry;
actEntry["name"] = act.getName(); actEntry["name"] = act.getName();
actionReprs.push_back(actEntry); actionReprs.push_back(actEntry);
} }
return modernjson::json(actionReprs); return ExportJsonType(actionReprs);
} }
modernjson::json buildTypeDescription(storm::expressions::Type const& type) { ExportJsonType buildTypeDescription(storm::expressions::Type const& type) {
modernjson::json typeDescr; ExportJsonType typeDescr;
if (type.isIntegerType()) { if (type.isIntegerType()) {
typeDescr = "int"; typeDescr = "int";
} else if (type.isRationalType()) { } else if (type.isRationalType()) {
@ -801,7 +801,7 @@ namespace storm {
return typeDescr; 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) { 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(0), constants);
getBoundsFromConstraints(typeDesc, var, constraint.getBaseExpression().getOperand(1), 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) { ExportJsonType buildConstantsArray(std::vector<storm::jani::Constant> const& constants) {
std::vector<modernjson::json> constantDeclarations; std::vector<ExportJsonType> constantDeclarations;
for(auto const& constant : constants) { for(auto const& constant : constants) {
modernjson::json constantEntry; ExportJsonType constantEntry;
constantEntry["name"] = constant.getName(); constantEntry["name"] = constant.getName();
modernjson::json typeDesc; ExportJsonType typeDesc;
if (constant.hasConstraint()) { if (constant.hasConstraint()) {
typeDesc["kind"] = "bounded"; typeDesc["kind"] = "bounded";
typeDesc["base"] = buildTypeDescription(constant.getType()); typeDesc["base"] = buildTypeDescription(constant.getType());
@ -844,19 +844,19 @@ namespace storm {
} }
constantDeclarations.push_back(constantEntry); 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()) { ExportJsonType 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 variableDeclarations = std::vector<ExportJsonType>();
for(auto const& variable : varSet) { for(auto const& variable : varSet) {
modernjson::json varEntry; ExportJsonType varEntry;
varEntry["name"] = variable.getName(); varEntry["name"] = variable.getName();
if (variable.isTransient()) { if (variable.isTransient()) {
varEntry["transient"] = variable.isTransient(); varEntry["transient"] = variable.isTransient();
} }
modernjson::json typeDesc; ExportJsonType typeDesc;
if(variable.isBooleanVariable()) { if(variable.isBooleanVariable()) {
typeDesc = "bool"; typeDesc = "bool";
} else if (variable.isRealVariable()) { } else if (variable.isRealVariable()) {
@ -879,7 +879,7 @@ namespace storm {
break; break;
case storm::jani::ArrayVariable::ElementType::Int: case storm::jani::ArrayVariable::ElementType::Int:
if (variable.asArrayVariable().hasElementTypeBound()) { if (variable.asArrayVariable().hasElementTypeBound()) {
modernjson::json baseTypeDescr; ExportJsonType baseTypeDescr;
baseTypeDescr["kind"] = "bounded"; baseTypeDescr["kind"] = "bounded";
baseTypeDescr["base "] = "int"; baseTypeDescr["base "] = "int";
if (variable.asArrayVariable().hasLowerElementTypeBound()) { if (variable.asArrayVariable().hasLowerElementTypeBound()) {
@ -907,17 +907,17 @@ namespace storm {
return variableDeclarations; 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()) { ExportJsonType 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 functionDeclarations = std::vector<ExportJsonType>();
for (auto const& nameFunDef : functionDefinitions) { for (auto const& nameFunDef : functionDefinitions) {
storm::jani::FunctionDefinition const& funDef = nameFunDef.second; storm::jani::FunctionDefinition const& funDef = nameFunDef.second;
modernjson::json funDefJson; ExportJsonType funDefJson;
funDefJson["name"] = nameFunDef.first; funDefJson["name"] = nameFunDef.first;
funDefJson["type"] = buildTypeDescription(funDef.getType()); funDefJson["type"] = buildTypeDescription(funDef.getType());
std::vector<modernjson::json> parameterDeclarations; std::vector<ExportJsonType> parameterDeclarations;
std::unordered_set<std::string> parameterNames; std::unordered_set<std::string> parameterNames;
for (auto const& p : funDef.getParameters()) { for (auto const& p : funDef.getParameters()) {
modernjson::json parDefJson; ExportJsonType parDefJson;
parDefJson["name"] = p.getName(); parDefJson["name"] = p.getName();
parameterNames.insert(p.getName()); parameterNames.insert(p.getName());
parDefJson["type"] = buildTypeDescription(p.getType()); parDefJson["type"] = buildTypeDescription(p.getType());
@ -930,16 +930,16 @@ namespace storm {
return functionDeclarations; 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) { ExportJsonType 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 assignmentDeclarations = std::vector<ExportJsonType>();
bool addIndex = orderedAssignments.hasMultipleLevels(); bool addIndex = orderedAssignments.hasMultipleLevels();
for(auto const& assignment : orderedAssignments) { for(auto const& assignment : orderedAssignments) {
modernjson::json assignmentEntry; ExportJsonType assignmentEntry;
if (assignment.getLValue().isVariable()) { if (assignment.getLValue().isVariable()) {
assignmentEntry["ref"] = assignment.getVariable().getName(); assignmentEntry["ref"] = assignment.getVariable().getName();
} else { } else {
STORM_LOG_ASSERT(assignment.getLValue().isArrayAccess(), "Unhandled LValue " << assignment.getLValue()); STORM_LOG_ASSERT(assignment.getLValue().isArrayAccess(), "Unhandled LValue " << assignment.getLValue());
modernjson::json arrayAccess; ExportJsonType arrayAccess;
arrayAccess["op"] = "aa"; arrayAccess["op"] = "aa";
arrayAccess["exp"] = assignment.getLValue().getArray().getName(); arrayAccess["exp"] = assignment.getLValue().getArray().getName();
arrayAccess["index"] = buildExpression(assignment.getLValue().getArrayIndex(), constants, globalVariables, localVariables); arrayAccess["index"] = buildExpression(assignment.getLValue().getArrayIndex(), constants, globalVariables, localVariables);
@ -957,13 +957,13 @@ namespace storm {
return assignmentDeclarations; 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) { ExportJsonType 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 locationDeclarations = std::vector<ExportJsonType>();
for(auto const& location : locations) { for(auto const& location : locations) {
modernjson::json locEntry; ExportJsonType locEntry;
locEntry["name"] = location.getName(); locEntry["name"] = location.getName();
if (location.hasTimeProgressInvariant()) { if (location.hasTimeProgressInvariant()) {
modernjson::json timeProg; ExportJsonType timeProg;
timeProg["exp"] = buildExpression(location.getTimeProgressInvariant(), constants, globalVariables, localVariables); timeProg["exp"] = buildExpression(location.getTimeProgressInvariant(), constants, globalVariables, localVariables);
if (commentExpressions) { if (commentExpressions) {
timeProg["comment"] = location.getTimeProgressInvariant().toString(); timeProg["comment"] = location.getTimeProgressInvariant().toString();
@ -978,19 +978,19 @@ namespace storm {
return locationDeclarations; return locationDeclarations;
} }
modernjson::json buildInitialLocations(storm::jani::Automaton const& automaton) { ExportJsonType buildInitialLocations(storm::jani::Automaton const& automaton) {
std::vector<std::string> names; std::vector<std::string> names;
for(auto const& initLocIndex : automaton.getInitialLocationIndices()) { for(auto const& initLocIndex : automaton.getInitialLocationIndices()) {
names.push_back(automaton.getLocation(initLocIndex).getName()); 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); assert(destinations.size() > 0);
modernjson::json destDeclarations = std::vector<modernjson::json>(); ExportJsonType destDeclarations = std::vector<ExportJsonType>();
for(auto const& destination : destinations) { for(auto const& destination : destinations) {
modernjson::json destEntry; ExportJsonType destEntry;
destEntry["location"] = locationNames.at(destination.getLocationIndex()); destEntry["location"] = locationNames.at(destination.getLocationIndex());
bool prob1 = false; bool prob1 = false;
if(destination.getProbability().isLiteral()) { if(destination.getProbability().isLiteral()) {
@ -1012,14 +1012,14 @@ namespace storm {
return destDeclarations; 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) { 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) {
modernjson::json edgeDeclarations = std::vector<modernjson::json>(); ExportJsonType edgeDeclarations = std::vector<ExportJsonType>();
for(auto const& edge : edges) { for(auto const& edge : edges) {
if (edge.getGuard().isFalse()) { if (edge.getGuard().isFalse()) {
continue; continue;
} }
STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed."); 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()); edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex());
if(!edge.hasSilentAction()) { if(!edge.hasSilentAction()) {
edgeEntry["action"] = actionNames.at(edge.getActionIndex()); edgeEntry["action"] = actionNames.at(edge.getActionIndex());
@ -1046,10 +1046,10 @@ namespace storm {
return edgeDeclarations; 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) { 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) {
modernjson::json automataDeclarations = std::vector<modernjson::json>(); ExportJsonType automataDeclarations = std::vector<ExportJsonType>();
for(auto const& automaton : automata) { for(auto const& automaton : automata) {
modernjson::json autoEntry; ExportJsonType autoEntry;
autoEntry["name"] = automaton.getName(); autoEntry["name"] = automaton.getName();
autoEntry["variables"] = buildVariablesArray(automaton.getVariables(), constants, globalVariables, automaton.getVariables()); autoEntry["variables"] = buildVariablesArray(automaton.getVariables(), constants, globalVariables, automaton.getVariables());
if (!automaton.getFunctionDefinitions().empty()) { if (!automaton.getFunctionDefinitions().empty()) {
@ -1108,8 +1108,8 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType"); 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) { ExportJsonType convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
modernjson::json propDecl; ExportJsonType propDecl;
propDecl["states"]["op"] = "initial"; propDecl["states"]["op"] = "initial";
propDecl["op"] = "filter"; propDecl["op"] = "filter";
propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); 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) { 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. // Unset model-features that only relate to properties. These are only set if such properties actually exist.
modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards); modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards);
if (formulas.empty()) { if (formulas.empty()) {
jsonStruct["properties"] = modernjson::json(modernjson::json::value_t::array); jsonStruct["properties"] = ExportJsonType(ExportJsonType::value_t::array);
return; return;
} }
uint64_t index = 0; uint64_t index = 0;
for(auto const& f : formulas) { for(auto const& f : formulas) {
modernjson::json propDecl; ExportJsonType propDecl;
propDecl["name"] = f.getName(); propDecl["name"] = f.getName();
propDecl["expression"] = convertFilterExpression(f.getFilter(), model, modelFeatures); propDecl["expression"] = convertFilterExpression(f.getFilter(), model, modelFeatures);
++index; ++index;
@ -1139,8 +1139,8 @@ namespace storm {
jsonStruct["properties"] = std::move(properties); jsonStruct["properties"] = std::move(properties);
} }
modernjson::json JsonExporter::finalize() { ExportJsonType JsonExporter::finalize() {
jsonStruct["features"] = modernjson::json::parse(modelFeatures.toString()); jsonStruct["features"] = ExportJsonType::parse(modelFeatures.toString());
return jsonStruct; return jsonStruct;
} }

27
src/storm/storage/jani/JSONExporter.h
View File

@ -7,19 +7,17 @@
#include "storm/storage/jani/Model.h" #include "storm/storage/jani/Model.h"
#include "storm/storage/jani/Property.h" #include "storm/storage/jani/Property.h"
#include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalNumberAdapter.h"
// JSON parser #include "storm/adapters/JsonAdapter.h"
#include "json.hpp"
namespace modernjson {
using json = nlohmann::json;
}
namespace storm { namespace storm {
namespace jani { namespace jani {
typedef storm::json<double> ExportJsonType;
class ExpressionToJson : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor { class ExpressionToJson : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor {
public: 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::IfThenElseExpression const& expression, boost::any const& data);
virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression 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 { class FormulaToJaniJson : public storm::logic::FormulaVisitor {
public: 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 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::AtomicExpressionFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::AtomicLabelFormula 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: private:
FormulaToJaniJson(storm::jani::Model const& model) : model(model), stateExitRewards(false) { } 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; ExportJsonType constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const;
modernjson::json constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const; ExportJsonType constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const;
modernjson::json constructStandardRewardAccumulation(std::string const& rewardModelName) const; ExportJsonType constructStandardRewardAccumulation(std::string const& rewardModelName) const;
storm::jani::Model const& model; storm::jani::Model const& model;
mutable bool stateExitRewards; mutable bool stateExitRewards;
}; };
class JsonExporter { class JsonExporter {
JsonExporter() = default;
public: 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 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); 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 convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);
void appendVariableDeclaration(storm::jani::Variable const& variable); void appendVariableDeclaration(storm::jani::Variable const& variable);
modernjson::json finalize(); ExportJsonType finalize();
modernjson::json jsonStruct; ExportJsonType jsonStruct;
storm::jani::ModelFeatures modelFeatures; storm::jani::ModelFeatures modelFeatures;
}; };

Write Preview
|||||||
100:0
Loading…
Cancel
Save