diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 8b634013..f6a87d11 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -1155,7 +1155,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : //Accumulation ExpressionAccumulation accexp; - ExpressionAccumulationConstraintBasic constr; + ExpressionAccumulationConstraint constr; TemporalOperatorBound bound; Expression reg; ArrayList fireOn; @@ -1189,7 +1189,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : // Weight constraint ( - constr = ExpressionAccumulationConstraintBasic() + constr = ExpressionAccumulationConstraintImplies() { accexp.setConstraint(constr); } ) @@ -1241,7 +1241,7 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) : ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathprop) : { ExpressionAccumulation ret; - ExpressionAccumulationConstraintBasic constr; + ExpressionAccumulationConstraint constr; TemporalOperatorBound bound; Expression reg; ArrayList fireOn; @@ -1265,7 +1265,7 @@ ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathpro // Weight constraint ( - constr = ExpressionAccumulationConstraintBasic() + constr = ExpressionAccumulationConstraintImplies() { ret.setConstraint(constr); } ) @@ -1297,36 +1297,100 @@ ArrayList ExpressionAccumulationFire() : { return ret; } } + + +ExpressionAccumulationConstraint ExpressionAccumulationConstraintImplies() : +{ + ExpressionAccumulationConstraint ret, expr; + Token begin = null; +} +{ + { begin = getToken(1); } ret = ExpressionAccumulationConstraintOr() + ( expr = ExpressionAccumulationConstraintOr() + { ret = new ExpressionAccumulationConstraint(ExpressionAccumulationConstraint.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0)); } + )* + { return ret; } +} + +ExpressionAccumulationConstraint ExpressionAccumulationConstraintOr() : +{ + ExpressionAccumulationConstraint ret, expr; + Token begin = null; +} +{ + { begin = getToken(1); } ret = ExpressionAccumulationConstraintAnd() + ( expr = ExpressionAccumulationConstraintAnd() + { ret = new ExpressionAccumulationConstraint(ExpressionAccumulationConstraint.OR, ret, expr); ret.setPosition(begin, getToken(0)); } + )* + { return ret; } +} + +ExpressionAccumulationConstraint ExpressionAccumulationConstraintAnd() : +{ + ExpressionAccumulationConstraint ret, expr; + Token begin = null; +} +{ + { begin = getToken(1); } ret = ExpressionAccumulationConstraintNot() + ( expr = ExpressionAccumulationConstraintNot() + { ret = new ExpressionAccumulationConstraint(ExpressionAccumulationConstraint.AND, ret, expr); ret.setPosition(begin, getToken(0)); } + )* + { return ret; } +} + +ExpressionAccumulationConstraint ExpressionAccumulationConstraintNot() : +{ + ExpressionAccumulationConstraint ret, expr; + Token begin = null; +} +{ + ( + begin = expr = ExpressionAccumulationConstraintNot() + { ret = new ExpressionAccumulationConstraint(ExpressionAccumulationConstraint.NOT, expr, null); ret.setPosition(begin, getToken(0)); } + | + begin = ret = ExpressionAccumulationConstraintImplies() + | + ret = ExpressionAccumulationConstraintBasic() + ) + { return ret; } +} + ExpressionAccumulationConstraintBasic ExpressionAccumulationConstraintBasic() : { ExpressionAccumulationConstraintBasic ret; - ArrayList factors; - TemporalOperatorBound bound; + ArrayList terms; + TemporalOperatorBound bound; + Token begin; } { - // (LiCo = Constant) - factors = ExpressionAccumulationLinearCombination() - bound = BoundExpression() - { return new ExpressionAccumulationConstraintBasic(factors, bound); } + ( + // (LiCo = Constant) + begin = ret = ExpressionAccumulationConstraintBasic() + | + terms = ExpressionAccumulationLinearCombination() + bound = BoundExpression() + { ret = new ExpressionAccumulationConstraintBasic(terms, bound); } + ) + { return ret; } } -ArrayList ExpressionAccumulationLinearCombination() : +ArrayList ExpressionAccumulationLinearCombination() : { - AccumulationFactor factor; - ArrayList factors = new ArrayList(); + AccumulationTerm term; + ArrayList terms = new ArrayList(); } { - factor = ExpressionAccumulationLinearFactor() { factors.add(factor); } + term = ExpressionAccumulationLinearFactor() { terms.add(term); } ( - factor = ExpressionAccumulationLinearFactor() { factors.add(factor); } + term = ExpressionAccumulationLinearFactor() { terms.add(term); } )* - { return factors; } + { return terms; } } -AccumulationFactor ExpressionAccumulationLinearFactor() : +AccumulationTerm ExpressionAccumulationLinearFactor() : { - Expression factor = null; + Expression coefficient = null; AccumulationFunction func; } { @@ -1336,10 +1400,10 @@ AccumulationFactor ExpressionAccumulationLinearFactor() : ( getToken(1).image.equals("time") || getToken(1).image.equals("steps") || getToken(1).image.equals("reward") )}) func = ExpressionAccumulationFunction() ) | - ( factor = ExpressionBasic(false,false) - func = ExpressionAccumulationFunction() ) + ( coefficient = ExpressionBasic(false,false) + func = ExpressionAccumulationFunction() ) ) - { return new AccumulationFactor(func,factor); } + { return new AccumulationTerm(func,coefficient); } } // This is taken from TemporalOpBound