diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index b625fcaf..663ef1ae 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -45,6 +45,7 @@ import prism.ModelInfo; import parser.visitor.*; import prism.ModelType; import prism.PrismLangException; +import explicit.MinMax; @SuppressWarnings({"unused", "static-access", "serial"}) public class PrismParser @@ -1571,6 +1572,7 @@ Expression ExpressionProb(boolean prop, boolean pathprop) : ExpressionIdent modifier = null; int r; String relOp = null; + MinMax minMax = null; Expression prob = null; Expression expr; Filter filter = null; @@ -1582,14 +1584,18 @@ Expression ExpressionProb(boolean prop, boolean pathprop) : // This production is only allowed in expressions if the "prop" parameter is true { if (!prop) throw generateParseException(); } // Various options for "P" keyword and attached symbols - (( begin =

( modifier = IdentifierExpression() )? ( - ( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) - |( { relOp = "="; isBool = false; } ) - |( { relOp = "min="; isBool = false; } ) - |( { relOp = "max="; isBool = false; } ))) - // These two are dupes of above but allow space to be omitted - |( begin = { relOp = "min="; isBool = false; } ) - |( begin = { relOp = "max="; isBool = false; } )) + ( + ( begin =

( modifier = IdentifierExpression() )? + (( { minMax = MinMax.min(); }) | ( {minMax = MinMax.max();} ))? + ) + // variants without whitespace between P and MIN/MAX: + | (begin = { minMax = MinMax.min();}) + | (begin = { minMax = MinMax.max();}) + ) + ( + ( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) + |( { relOp = "="; isBool = false; } ) + ) // Path formula, optional filter expr = PathSpecification(prop) @@ -1598,6 +1604,7 @@ Expression ExpressionProb(boolean prop, boolean pathprop) : { ret.setModifier(modifier == null ? null : modifier.getName()); ret.setRelOp(relOp); + ret.setMinMax(minMax); ret.setProb(prob); ret.setExpression(expr); ret.setFilter(filter); @@ -1740,6 +1747,7 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : ExpressionIdent modifier = null; int r; String relOp = null; + MinMax minMax = null; Expression rew = null; Expression expr; Filter filter = null; @@ -1751,20 +1759,25 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : // This production is only allowed in expressions if the "prop" parameter is true { if (!prop) throw generateParseException(); } // Various options for "R" keyword and attached symbols - (( begin = + ( + ( begin = ( modifier = IdentifierExpression() )? (RewardSpecification(ret))? - (( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) + (( {minMax = MinMax.min();}) | ( {minMax = MinMax.max();}))? + ) + // These two are dupes of above but allow space to be omitted + |( begin = { minMax = MinMax.min();}) + |( begin = { minMax = MinMax.max();}) + ) + ( + ( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) |( { relOp = "="; isBool = false; } ) - |( { relOp = "min="; isBool = false; } ) - |( { relOp = "max="; isBool = false; } ))) - // These two are dupes of above but allow space to be omitted - |( begin = { relOp = "min="; isBool = false; } ) - |( begin = { relOp = "max="; isBool = false; } )) + ) // Path formula, optional filter expr = ExpressionRewardContents(prop, pathprop) (filter = Filter())? { ret.setModifier(modifier == null ? null : modifier.getName()); + ret.setMinMax(minMax); ret.setRelOp(relOp); ret.setReward(rew); ret.setExpression(expr);