From 50aa6d14240344b9695c483e01663d849d9d728a Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 29 Jun 2018 19:33:10 +0200 Subject: [PATCH] assuming the only global real transient variable is the reward when exporting JANI and no reward model is mentioned in the property (issues a warning) --- src/storm/storage/jani/JSONExporter.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 0c0c212a0..d41cf86af 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -398,8 +398,22 @@ namespace storm { opDecl["op"] = "Emin"; opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } - STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); - opDecl["exp"] = f.getRewardModelName(); + std::string rewardModelName; + if (f.hasRewardModelName()) { + rewardModelName = f.getRewardModelName(); + } else { + if (model.getGlobalVariables().getNumberOfRealTransientVariables() == 1) { + for (auto const& variable : model.getGlobalVariables().getRealVariables()) { + if (variable.isTransient()) { + rewardModelName = variable.getName(); + STORM_LOG_WARN("Reward model name was not given, assuming the only global real transient variable '" << rewardModelName << "' to measure the reward."); + break; + } + } + } + } + STORM_LOG_THROW(!rewardModelName.empty(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); + opDecl["exp"] = rewardModelName; opDecl["accumulate"] = modernjson::json(accvec); } return opDecl; @@ -408,7 +422,6 @@ namespace storm { boost::any FormulaToJaniJson::visit(storm::logic::TotalRewardFormula const&, boost::any const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support a total reward formula"); } - boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { modernjson::json opDecl;