Jani: import/export of steady-state properties

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<storm::logic::Formula const> subformula = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0];
+                        return std::make_shared<storm::logic::LongRunAverageOperatorFormula>(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<storm::logic::LongRunAverageRewardFormula>();
+                    return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo);
+                    
                 } else if (opString == "U" || opString == "F") {
                     assert(bound == boost::none);
                     std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::logic::AtomicExpressionFormula>(expr);
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString);

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");
 
-            if(f.hasBound()) {
-                auto bound = f.getBound();
-                opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
+            std::string opString = "";
+            if (f.getSubformula().isLongRunAverageRewardFormula()) {
+                opString = "S";
+            } else {
+                opString = "E";
+            }
             if (f.hasOptimalityType()) {
-                    opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
+                opString += storm::solver::minimize(f.getOptimalityType()) ? "min" : "max";
+            } else if (f.hasBound()) {
+                opString += storm::logic::isLowerBound(f.getBound().comparisonType) ? "min" : "max";
             } else {
-                    opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin";
+                opString += "min";
             }
+            
+            if(f.hasBound()) {
+                auto bound = f.getBound();
+                opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
+                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());
             }