Browse Source

JaniParser: Actually fixed parsing of long run average reward formulas

tempestpy_adaptions
TimQu 6 years ago
parent
commit
bbe9253777
  1. 2
      src/storm-parsers/parser/JaniParser.cpp

2
src/storm-parsers/parser/JaniParser.cpp

@ -389,7 +389,7 @@ namespace storm {
STORM_LOG_THROW(propertyStructure.count("exp") > 0, storm::exceptions::InvalidJaniException, "Expected an expression at steady state property at " << scope.description); 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); auto rewExpr = parseExpression(propertyStructure["exp"], scope.refine("steady-state operator"), true);
if (!expr.isInitialized() || expr.hasBooleanType()) {
if (!rewExpr.isInitialized() || rewExpr.hasBooleanType()) {
std::shared_ptr<storm::logic::Formula const> subformula = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Steady-state operator"))[0]; 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); return std::make_shared<storm::logic::LongRunAverageOperatorFormula>(subformula, opInfo);
} }

Loading…
Cancel
Save