Browse Source

fixing time operator formulas

tempestpy_adaptions
TimQu 6 years ago
parent
commit
b3be56588f
  1. 4
      src/storm/storage/jani/JSONExporter.cpp

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

@ -263,7 +263,7 @@ namespace storm {
} }
} else { } else {
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"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, data));
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
} }
opDecl["left"]["exp"] = modernjson::json(1); opDecl["left"]["exp"] = modernjson::json(1);
opDecl["left"]["accumulate"] = modernjson::json(tvec); opDecl["left"]["accumulate"] = modernjson::json(tvec);
@ -279,7 +279,7 @@ namespace storm {
} else { } else {
// TODO add checks // TODO add checks
opDecl["op"] = "Emin"; opDecl["op"] = "Emin";
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, data));
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
} }
opDecl["exp"] = modernjson::json(1); opDecl["exp"] = modernjson::json(1);
opDecl["accumulate"] = modernjson::json(tvec); opDecl["accumulate"] = modernjson::json(tvec);

Loading…
Cancel
Save