From 082d624174a1153f22b2ef0aba6440c0284cda89 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 15 Oct 2018 13:53:19 +0200 Subject: [PATCH] Jani: import/export of steady-state properties --- src/storm-parsers/parser/JaniParser.cpp | 20 ++++++++++++++- src/storm/storage/jani/JSONExporter.cpp | 34 +++++++++++++++---------- 2 files changed, 40 insertions(+), 14 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 9d90f1e31..6c5937cdc 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -383,7 +383,24 @@ namespace storm { } } } else if (opString == "Smin" || opString == "Smax") { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); + storm::logic::OperatorInformation opInfo; + opInfo.optimalityType = opString == "Smin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + opInfo.bound = bound; + + STORM_LOG_THROW(propertyStructure.count("exp") > 0, storm::exceptions::InvalidJaniException, "Expected an expression at steady state property at " << scope.description); + auto rewExpr = parseExpression(propertyStructure["exp"], scope.refine("steady-state operator"), true); + if (!expr.isInitialized() || expr.hasBooleanType()) { + std::shared_ptr subformula = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0]; + return std::make_shared(subformula, opInfo); + } + STORM_LOG_THROW(rewExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewExpr << "' does not have numerical type in " << scope.description); + std::string rewardName = rewExpr.toString(); + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } + auto subformula = std::make_shared(); + return std::make_shared(subformula, rewardName, opInfo); + } else if (opString == "U" || opString == "F") { assert(bound == boost::none); std::vector> args; @@ -540,6 +557,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons for properties are supported."); } else if (expr.isInitialized()) { assert(bound == boost::none); + STORM_LOG_THROW(expr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Expected a boolean expression at " << scope.description); return std::make_shared(expr); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index bf1f55eea..37aacc269 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -370,7 +370,7 @@ namespace storm { } else { // TODO add checks - opDecl["op"] = "Pmin"; + opDecl["op"] = "Smin"; opDecl["exp"] = anyToJson(f.getSubformula().accept(*this, data)); } } @@ -478,14 +478,24 @@ namespace storm { } STORM_LOG_THROW(!rewardModelName.empty(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); + std::string opString = ""; + if (f.getSubformula().isLongRunAverageRewardFormula()) { + opString = "S"; + } else { + opString = "E"; + } + if (f.hasOptimalityType()) { + opString += storm::solver::minimize(f.getOptimalityType()) ? "min" : "max"; + } else if (f.hasBound()) { + opString += storm::logic::isLowerBound(f.getBound().comparisonType) ? "min" : "max"; + } else { + opString += "min"; + } + if(f.hasBound()) { auto bound = f.getBound(); opDecl["op"] = comparisonTypeToJani(bound.comparisonType); - if(f.hasOptimalityType()) { - opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - } else { - opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; - } + opDecl["left"]["op"] = opString; if (f.getSubformula().isEventuallyFormula()) { opDecl["left"]["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { @@ -504,17 +514,13 @@ namespace storm { } } else if (f.getSubformula().isInstantaneousRewardFormula()) { opDecl["left"][instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); + } else if (f.getSubformula().isLongRunAverageRewardFormula()) { + // Nothing to do in this case } - STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); opDecl["left"]["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables()); } else { - if (f.hasOptimalityType()) { - opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - } else { - // TODO add checks - opDecl["op"] = "Emin"; - } + opDecl["op"] = opString; if (f.getSubformula().isEventuallyFormula()) { opDecl["reach"] = anyToJson(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); @@ -534,6 +540,8 @@ namespace storm { } } else if (f.getSubformula().isInstantaneousRewardFormula()) { opDecl[instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); + } else if (f.getSubformula().isLongRunAverageRewardFormula()) { + // Nothing to do in this case } opDecl["exp"] = buildExpression(model.getRewardModelExpression(rewardModelName), model.getConstants(), model.getGlobalVariables()); }