2 Commits

Author SHA1 Message Date
Sascha Wunderlich ed4f421b6a Parser refresh 6 years ago
Sascha Wunderlich f4794800d1 Prep for complex accumulation constraints, pt3 6 years ago
  1. 2916
      prism/src/parser/PrismParser.java
  2. 106
      prism/src/parser/PrismParser.jj
  3. 7
      prism/src/parser/ast/ExpressionAccumulationConstraint.java
  4. 22
      prism/src/parser/ast/ExpressionAccumulationConstraintBasic.java
  5. 11
      prism/src/parser/visitor/ASTTraverse.java
  6. 9
      prism/src/parser/visitor/ASTTraverseModify.java

2916
prism/src/parser/PrismParser.java
File diff suppressed because it is too large
View File

106
prism/src/parser/PrismParser.jj

@ -1155,7 +1155,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
//Accumulation //Accumulation
ExpressionAccumulation accexp; ExpressionAccumulation accexp;
ExpressionAccumulationConstraintBasic constr;
ExpressionAccumulationConstraint constr;
TemporalOperatorBound bound; TemporalOperatorBound bound;
Expression reg; Expression reg;
ArrayList<Expression> fireOn; ArrayList<Expression> fireOn;
@ -1189,7 +1189,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
// Weight constraint // Weight constraint
<LBRACE> <LBRACE>
( (
constr = ExpressionAccumulationConstraintBasic()
constr = ExpressionAccumulationConstraintImplies()
{ accexp.setConstraint(constr); } { accexp.setConstraint(constr); }
) )
<RBRACE> <RBRACE>
@ -1241,7 +1241,7 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) :
ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathprop) : ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathprop) :
{ {
ExpressionAccumulation ret; ExpressionAccumulation ret;
ExpressionAccumulationConstraintBasic constr;
ExpressionAccumulationConstraint constr;
TemporalOperatorBound bound; TemporalOperatorBound bound;
Expression reg; Expression reg;
ArrayList<Expression> fireOn; ArrayList<Expression> fireOn;
@ -1265,7 +1265,7 @@ ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathpro
// Weight constraint // Weight constraint
<LBRACE> <LBRACE>
( (
constr = ExpressionAccumulationConstraintBasic()
constr = ExpressionAccumulationConstraintImplies()
{ ret.setConstraint(constr); } { ret.setConstraint(constr); }
) )
<RBRACE> <RBRACE>
@ -1297,36 +1297,100 @@ ArrayList<Expression> ExpressionAccumulationFire() :
{ return ret; } { 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 ExpressionAccumulationConstraintBasic() :
{ {
ExpressionAccumulationConstraintBasic ret; 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> <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; AccumulationFunction func;
} }
{ {
@ -1336,10 +1400,10 @@ AccumulationFactor ExpressionAccumulationLinearFactor() :
( getToken(1).image.equals("time") || getToken(1).image.equals("steps") || getToken(1).image.equals("reward") )}) ( getToken(1).image.equals("time") || getToken(1).image.equals("steps") || getToken(1).image.equals("reward") )})
func = ExpressionAccumulationFunction() ) 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 // This is taken from TemporalOpBound

7
prism/src/parser/ast/ExpressionAccumulationConstraint.java

@ -186,7 +186,12 @@ public class ExpressionAccumulationConstraint extends Expression
@Override @Override
public Expression deepCopy() public Expression deepCopy()
{ {
ExpressionAccumulationConstraint expr = new ExpressionAccumulationConstraint(op, (ExpressionAccumulationConstraint)operand1.deepCopy(), (ExpressionAccumulationConstraint)operand2.deepCopy());
ExpressionAccumulationConstraint newop1 = null;
ExpressionAccumulationConstraint newop2 = null;
if(operand1 != null) newop1 = (ExpressionAccumulationConstraint)operand1.deepCopy();
if(operand2 != null) newop2 = (ExpressionAccumulationConstraint)operand2.deepCopy();
ExpressionAccumulationConstraint expr = new ExpressionAccumulationConstraint(op, newop1, newop2);
expr.setType(type); expr.setType(type);
expr.setPosition(this); expr.setPosition(this);
return expr; return expr;

22
prism/src/parser/ast/ExpressionAccumulationConstraintBasic.java

@ -25,12 +25,12 @@ public class ExpressionAccumulationConstraintBasic extends ExpressionAccumulatio
this.op = BASIC; this.op = BASIC;
} }
public ArrayList<AccumulationTerm> getFactors() {
public ArrayList<AccumulationTerm> getTerms() {
return terms; return terms;
} }
public void setFactors(ArrayList<AccumulationTerm> factors) {
this.terms = factors;
public void setTerms(ArrayList<AccumulationTerm> terms) {
this.terms = terms;
} }
public TemporalOperatorBound getBound() { public TemporalOperatorBound getBound() {
@ -44,8 +44,8 @@ public class ExpressionAccumulationConstraintBasic extends ExpressionAccumulatio
@Override @Override
public Vector<AccumulationFunction> getFunctions() { public Vector<AccumulationFunction> getFunctions() {
Vector<AccumulationFunction> ret = new Vector<AccumulationFunction>(); Vector<AccumulationFunction> ret = new Vector<AccumulationFunction>();
for(AccumulationTerm factor : terms) {
ret.add(factor.getFunction());
for(AccumulationTerm term : terms) {
ret.add(term.getFunction());
} }
return ret; return ret;
} }
@ -74,14 +74,14 @@ public class ExpressionAccumulationConstraintBasic extends ExpressionAccumulatio
} }
public ExpressionAccumulationConstraintBasic deepCopy() { public ExpressionAccumulationConstraintBasic deepCopy() {
ArrayList<AccumulationTerm> factorscopy = new ArrayList<AccumulationTerm>();
ArrayList<AccumulationTerm> termscopy = new ArrayList<AccumulationTerm>();
TemporalOperatorBound boundcopy = bound.deepCopy(); TemporalOperatorBound boundcopy = bound.deepCopy();
for (AccumulationTerm factor : terms) {
factorscopy.add(factor.deepCopy());
for (AccumulationTerm term : terms) {
termscopy.add(term.deepCopy());
} }
return new ExpressionAccumulationConstraintBasic(factorscopy,boundcopy);
return new ExpressionAccumulationConstraintBasic(termscopy,boundcopy);
} }
public String toString() public String toString()
@ -89,11 +89,11 @@ public class ExpressionAccumulationConstraintBasic extends ExpressionAccumulatio
boolean first = true; boolean first = true;
String ret = ""; String ret = "";
for (AccumulationTerm factor : terms) {
for (AccumulationTerm term : terms) {
if (!first) ret += " + "; if (!first) ret += " + ";
first = false; first = false;
ret += factor.toString();
ret += term.toString();
} }
ret += bound.toString(); ret += bound.toString();

11
prism/src/parser/visitor/ASTTraverse.java

@ -423,10 +423,10 @@ public class ASTTraverse implements ASTVisitor
public Object visit(ExpressionAccumulationConstraint e) throws PrismLangException public Object visit(ExpressionAccumulationConstraint e) throws PrismLangException
{ {
visitPre(e); visitPre(e);
e.setOperand1((ExpressionAccumulationConstraint)(e.getOperand1().accept(this)));
e.setOperand2((ExpressionAccumulationConstraint)(e.getOperand2().accept(this)));
if(e.getOperand1() != null) e.getOperand1().accept(this);
if(e.getOperand2() != null) e.getOperand2().accept(this);
visitPost(e); visitPost(e);
return e;
return null;
} }
public void visitPost(ExpressionAccumulationConstraint e) throws PrismLangException { defaultVisitPost(e); } public void visitPost(ExpressionAccumulationConstraint e) throws PrismLangException { defaultVisitPost(e); }
// ----------------------------------------------------------------------------------- // -----------------------------------------------------------------------------------
@ -439,12 +439,13 @@ public class ASTTraverse implements ASTVisitor
return null; return null;
} }
public void visitPost(AccumulationTerm e) throws PrismLangException { defaultVisitPost(e); } public void visitPost(AccumulationTerm e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(ExpressionAccumulationConstraintBasic e) throws PrismLangException { defaultVisitPre(e); } public void visitPre(ExpressionAccumulationConstraintBasic e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(ExpressionAccumulationConstraintBasic e) throws PrismLangException public Object visit(ExpressionAccumulationConstraintBasic e) throws PrismLangException
{ {
visitPre(e); visitPre(e);
for (AccumulationTerm factor : e.getFactors()) {
factor.accept(this);
for (AccumulationTerm term : e.getTerms()) {
term.accept(this);
} }
if (e.getBound() != null) e.getBound().accept(this); if (e.getBound() != null) e.getBound().accept(this);
visitPost(e); visitPost(e);

9
prism/src/parser/visitor/ASTTraverseModify.java

@ -434,8 +434,8 @@ public class ASTTraverseModify implements ASTVisitor
public Object visit(ExpressionAccumulationConstraint e) throws PrismLangException public Object visit(ExpressionAccumulationConstraint e) throws PrismLangException
{ {
visitPre(e); visitPre(e);
e.setOperand1((ExpressionAccumulationConstraint)(e.getOperand1().accept(this)));
e.setOperand2((ExpressionAccumulationConstraint)(e.getOperand2().accept(this)));
if(e.getOperand1() != null) e.setOperand1((ExpressionAccumulationConstraint)(e.getOperand1().accept(this)));
if(e.getOperand2() != null) e.setOperand2((ExpressionAccumulationConstraint)(e.getOperand2().accept(this)));
visitPost(e); visitPost(e);
return e; return e;
} }
@ -450,12 +450,13 @@ public class ASTTraverseModify implements ASTVisitor
return e; return e;
} }
public void visitPost(AccumulationTerm e) throws PrismLangException { defaultVisitPost(e); } public void visitPost(AccumulationTerm e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(ExpressionAccumulationConstraintBasic e) throws PrismLangException { defaultVisitPre(e); } public void visitPre(ExpressionAccumulationConstraintBasic e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(ExpressionAccumulationConstraintBasic e) throws PrismLangException public Object visit(ExpressionAccumulationConstraintBasic e) throws PrismLangException
{ {
visitPre(e); visitPre(e);
for (AccumulationTerm factor : e.getFactors()) {
factor.accept(this);
for (AccumulationTerm term : e.getTerms()) {
term.accept(this);
} }
if (e.getBound() != null) e.getBound().accept(this); if (e.getBound() != null) e.getBound().accept(this);
visitPost(e); visitPost(e);

Loading…
Cancel
Save