Parser refresh

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<Expression> fireOn;
@@ -1189,7 +1189,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
 		// Weight constraint
 		<LBRACE>
 		(
-			constr = ExpressionAccumulationConstraintBasic()
+			constr = ExpressionAccumulationConstraintImplies()
 			{ accexp.setConstraint(constr); }
 		)
 		<RBRACE>
@@ -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<Expression> fireOn;
@@ -1265,7 +1265,7 @@ ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathpro
 	// Weight constraint
 	<LBRACE>
 	(
-		constr = ExpressionAccumulationConstraintBasic()
+		constr = ExpressionAccumulationConstraintImplies()
 		{ ret.setConstraint(constr); }
 	)
 	<RBRACE>
@@ -1297,36 +1297,100 @@ ArrayList<Expression> ExpressionAccumulationFire() :
 	{ return ret; }
 }
 
+
+
+ExpressionAccumulationConstraint ExpressionAccumulationConstraintImplies() :
+{
+	ExpressionAccumulationConstraint ret, expr;
+	Token begin = null;
+}
+{
+	{ begin = getToken(1); } ret = ExpressionAccumulationConstraintOr()
+	( <IMPLIES> 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()
+	( <OR> 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()
+	( <AND> 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 = <NOT> expr = ExpressionAccumulationConstraintNot()
+		{ ret = new ExpressionAccumulationConstraint(ExpressionAccumulationConstraint.NOT, expr, null); ret.setPosition(begin, getToken(0)); }
+	|
+		begin = <LPARENTH> ret = ExpressionAccumulationConstraintImplies() <RPARENTH>
+	|
+		ret = ExpressionAccumulationConstraintBasic()
+	)
+	{ return ret; }
+}
+
 ExpressionAccumulationConstraintBasic ExpressionAccumulationConstraintBasic() :
 {
 	ExpressionAccumulationConstraintBasic ret;
-	ArrayList<AccumulationFactor> factors;
-	TemporalOperatorBound bound;	
+	ArrayList<AccumulationTerm> terms;
+	TemporalOperatorBound bound;
+	Token begin;	
 }
 {
-	// (LiCo = Constant)
-	factors = ExpressionAccumulationLinearCombination()
-	bound = BoundExpression()
-	{ return new ExpressionAccumulationConstraintBasic(factors, bound); }
+	(
+		// (LiCo = Constant)
+		begin = <LPARENTH> ret = ExpressionAccumulationConstraintBasic() <RPARENTH>
+	|
+		terms = ExpressionAccumulationLinearCombination()
+		bound = BoundExpression()
+		{ ret = new ExpressionAccumulationConstraintBasic(terms, bound); }
+	)
+	{ return ret; }
 }
 
-ArrayList<AccumulationFactor> ExpressionAccumulationLinearCombination() :
+ArrayList<AccumulationTerm> ExpressionAccumulationLinearCombination() :
 {
-	AccumulationFactor factor;
-	ArrayList<AccumulationFactor> factors = new ArrayList<AccumulationFactor>();
+	AccumulationTerm term;
+	ArrayList<AccumulationTerm> terms = new ArrayList<AccumulationTerm>();
 }
 {
-	factor = ExpressionAccumulationLinearFactor() { factors.add(factor); }
+	term = ExpressionAccumulationLinearFactor() { terms.add(term); }
 	(
 		<PLUS>
-		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) <TIMES>
-	      func   = ExpressionAccumulationFunction() )
+	    ( coefficient = ExpressionBasic(false,false) <TIMES>
+	      func        = ExpressionAccumulationFunction() )
 	)
-	{ return new AccumulationFactor(func,factor); }
+	{ return new AccumulationTerm(func,coefficient); }
 }
 
 // This is taken from TemporalOpBound