diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 3e0093f5b..97f811e9f 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -31,6 +31,7 @@ #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/Property.h" #include "storm/storage/jani/traverser/AssignmentsFinder.h" +#include "storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h" namespace storm { namespace jani { @@ -619,8 +620,7 @@ namespace storm { modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set const& auxiliaryVariables) { // Simplify the expression first and reduce the nesting - auto simplifiedExpr = expr.simplify().reduceNesting(); - + auto simplifiedExpr = storm::jani::reduceNestingInJaniExpression(expr.simplify()); ExpressionToJson visitor(constants, globalVariables, localVariables, auxiliaryVariables); return boost::any_cast(simplifiedExpr.accept(visitor, boost::none)); diff --git a/src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.cpp b/src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.cpp new file mode 100644 index 000000000..cdee6e967 --- /dev/null +++ b/src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.cpp @@ -0,0 +1,62 @@ +#include "storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h" + +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + + namespace jani { + storm::expressions::Expression reduceNestingInJaniExpression(storm::expressions::Expression const& expression) { + return storm::expressions::JaniReduceNestingExpressionVisitor().reduceNesting(expression); + } + } + + namespace expressions { + + JaniReduceNestingExpressionVisitor::JaniReduceNestingExpressionVisitor() : ReduceNestingVisitor() { + // Intentionally left empty. + } + + boost::any JaniReduceNestingExpressionVisitor::visit(ValueArrayExpression const& expression, boost::any const& data) { + uint64_t size = expression.size()->evaluateAsInt(); + std::vector> newElements; + newElements.reserve(size); + for (uint64_t i = 0; i < size; ++i) { + newElements.push_back(boost::any_cast>(expression.at(i)->accept(*this, data))); + } + return std::const_pointer_cast(std::shared_ptr(new ValueArrayExpression(expression.getManager(), expression.getType(), newElements))); + } + + boost::any JaniReduceNestingExpressionVisitor::visit(ConstructorArrayExpression const& expression, boost::any const& data) { + std::shared_ptr newSize = boost::any_cast>(expression.size()->accept(*this, data)); + std::shared_ptr elementExpression = boost::any_cast>(expression.getElementExpression()->accept(*this, data)); + + // If the arguments did not change, we simply push the expression itself. + if (newSize.get() == expression.size().get() && elementExpression.get() == expression.getElementExpression().get()) { + return expression.getSharedPointer(); + } else { + return std::const_pointer_cast(std::shared_ptr(new ConstructorArrayExpression(expression.getManager(), expression.getType(), newSize, expression.getIndexVar(), elementExpression))); + } + } + + boost::any JaniReduceNestingExpressionVisitor::visit(ArrayAccessExpression const& expression, boost::any const& data) { + std::shared_ptr firstExpression = boost::any_cast>(expression.getFirstOperand()->accept(*this, data)); + std::shared_ptr secondExpression = boost::any_cast>(expression.getSecondOperand()->accept(*this, data)); + + // If the arguments did not change, we simply push the expression itself. + if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) { + return expression.getSharedPointer(); + } else { + return std::const_pointer_cast(std::shared_ptr(new ArrayAccessExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression))); + } + } + + boost::any JaniReduceNestingExpressionVisitor::visit(FunctionCallExpression const& expression, boost::any const& data) { + std::vector> newArguments; + newArguments.reserve(expression.getNumberOfArguments()); + for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) { + newArguments.push_back(boost::any_cast>(expression.getArgument(i)->accept(*this, data))); + } + return std::const_pointer_cast(std::shared_ptr(new FunctionCallExpression(expression.getManager(), expression.getType(), expression.getFunctionIdentifier(), newArguments))); + } + } +} diff --git a/src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h b/src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h new file mode 100644 index 000000000..c45c1ac6e --- /dev/null +++ b/src/storm/storage/jani/expressions/JaniReduceNestingExpressionVisitor.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm/storage/expressions/ReduceNestingVisitor.h" +#include "storm/storage/jani/expressions/JaniExpressions.h" +#include "storm/storage/jani/expressions/JaniExpressionVisitor.h" + +namespace storm { + namespace jani { + storm::expressions::Expression reduceNestingInJaniExpression(storm::expressions::Expression const& expression); + } + + namespace expressions { + + + class JaniReduceNestingExpressionVisitor : public ReduceNestingVisitor, public JaniExpressionVisitor { + public: + JaniReduceNestingExpressionVisitor(); + + virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) override; + virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) override; + virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override; + virtual boost::any visit(FunctionCallExpression const& expression, boost::any const& data) override; + }; + } +} \ No newline at end of file