From deaaa91c37a54ab99c57ec626918538ea66ac3f8 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 14 Sep 2016 13:06:04 +0200 Subject: [PATCH] Expressions & Destinations Assignments Former-commit-id: dacc1f71468f814f9ef3ea673575668695d70b5f [formerly 1580bce6a4a2867c25b7959266e81be4ab0e2d9b] Former-commit-id: a089bbd11a38889c7057d349d744ce86d89b03d2 --- src/storage/jani/JSONExporter.cpp | 136 +++++++++++++++++++++++++++++- src/storage/jani/JSONExporter.h | 22 ++++- 2 files changed, 154 insertions(+), 4 deletions(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index d127ceec3..a45519ed9 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -7,10 +7,141 @@ #include "src/utility/macros.h" #include "src/exceptions/FileIoException.h" +#include "src/exceptions/InvalidJaniException.h" +#include "src/storage/expressions/RationalLiteralExpression.h" +#include "src/storage/expressions/IntegerLiteralExpression.h" +#include "src/storage/expressions/BooleanLiteralExpression.h" +#include "src/storage/expressions/UnaryBooleanFunctionExpression.h" +#include "src/storage/expressions/UnaryNumericalFunctionExpression.h" +#include "src/storage/expressions/BinaryBooleanFunctionExpression.h" +#include "src/storage/expressions/BinaryNumericalFunctionExpression.h" +#include "src/storage/expressions/IfThenElseExpression.h" +#include "src/storage/expressions/BinaryRelationExpression.h" +#include "src/storage/expressions/VariableExpression.h" namespace storm { namespace jani { + + std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) { + + using OpType = storm::expressions::OperatorType; + switch(optype) { + case OpType::And: + return "∧"; + case OpType::Or: + return "∨"; + case OpType::Xor: + return "≠"; + case OpType::Implies: + return "⇒"; + case OpType::Iff: + return "="; + case OpType::Plus: + return "+"; + case OpType::Minus: + return "-"; + case OpType::Times: + return "*"; + case OpType::Divide: + return "/"; + case OpType::Min: + return "min"; + case OpType::Max: + return "max"; + case OpType::Power: + return "pow"; + case OpType::Equal: + return "="; + case OpType::NotEqual: + return "≠"; + case OpType::Less: + return "<"; + case OpType::LessOrEqual: + return "≤"; + case OpType::Greater: + return ">"; + case OpType::GreaterOrEqual: + return "≥"; + case OpType::Not: + return "¬"; + case OpType::Floor: + return "floor"; + case OpType::Ceil: + return "ceil"; + case OpType::Ite: + return "ite"; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Operator not supported by Jani"); + } + } + + modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr) { + ExpressionToJson visitor; + return boost::any_cast(expr.accept(visitor, boost::none)); + } + + + boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { + modernjson::json opDecl; + opDecl["op"] = "ite"; + opDecl["if"] = boost::any_cast(expression.getCondition()->accept(*this, boost::none)); + opDecl["then"] = boost::any_cast(expression.getThenExpression()->accept(*this, boost::none)); + opDecl["else"] = boost::any_cast(expression.getElseExpression()->accept(*this, boost::none)); + return opDecl; + } + boost::any ExpressionToJson::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + modernjson::json opDecl; + opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); + opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, boost::none)); + return opDecl; + } + boost::any ExpressionToJson::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + modernjson::json opDecl; + opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); + opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, boost::none)); + return opDecl; + } + boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) { + modernjson::json opDecl; + opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); + opDecl["left"] = boost::any_cast(expression.getOperand(0)->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(expression.getOperand(1)->accept(*this, boost::none)); + return opDecl; + } + boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) { + return modernjson::json(expression.getVariableName()); + } + boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + modernjson::json opDecl; + opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); + opDecl["exp"] = boost::any_cast(expression.getOperand()->accept(*this, boost::none)); + return opDecl; + } + boost::any ExpressionToJson::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + modernjson::json opDecl; + opDecl["op"] = operatorTypeToJaniString(expression.getOperator()); + opDecl["exp"] = boost::any_cast(expression.getOperand()->accept(*this, boost::none)); + return opDecl; + } + boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) { + return modernjson::json(expression.getValue()); + } + boost::any ExpressionToJson::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) { + return modernjson::json(expression.getValue()); + } + boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) { + return modernjson::json(expression.getValueAsDouble()); + } + + + + + + + void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath) { std::ofstream ofs; ofs.open (filepath, std::ofstream::out ); @@ -41,7 +172,7 @@ namespace storm { modernjson::json buildExpression(storm::expressions::Expression const& exp) { - return modernjson::json(); + return ExpressionToJson::translate(exp); } @@ -140,8 +271,7 @@ namespace storm { modernjson::json destEntry; destEntry["location"] = locationNames.at(destination.getLocationIndex()); destEntry["probability"] = buildExpression(destination.getProbability()); - // TODO - //destEntry["assignments"] = buildAssignmentArray(destination.getAssignments()); + destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments()); destDeclarations.push_back(destEntry); } return modernjson::json(destDeclarations); diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 84d3fb44a..35fb567fa 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -1,13 +1,33 @@ #pragma once -#include "Model.h" +#include "src/storage/expressions/ExpressionVisitor.h" +#include "Model.h" // JSON parser #include "json.hpp" namespace modernjson = nlohmann; namespace storm { namespace jani { + + class ExpressionToJson : public storm::expressions::ExpressionVisitor { + + public: + static modernjson::json translate(storm::expressions::Expression const& expr); + + 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::BinaryNumericalFunctionExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data); + + }; + class JsonExporter { JsonExporter() = default;