Browse Source

Jani Export: Power expressions of integer type need to be type casted.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
d863fe4156
  1. 12
      src/storm/storage/jani/JSONExporter.cpp

12
src/storm/storage/jani/JSONExporter.cpp

@ -632,8 +632,17 @@ namespace storm {
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data));
return opDecl;
if (expression.getOperator() == storm::expressions::OperatorType::Power && expression.getType().isIntegerType()) {
// power expressions that have integer type need to be "type casted"
ExportJsonType trc;
trc["op"] = "trc";
trc["exp"] = std::move(opDecl);
return trc;
} else {
return opDecl;
}
}
boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
@ -670,6 +679,7 @@ namespace storm {
opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data));
return opDecl;
}
boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) {
return ExportJsonType(expression.getValue());
}

Loading…
Cancel
Save