Browse Source

Prep for complex accumulation constraints

accumulation
Sascha Wunderlich 6 years ago
parent
commit
621b21388b
  1. 14
      prism/src/parser/PrismParser.jj
  2. 12
      prism/src/parser/ast/AccumulationConstraintBasic.java
  3. 6
      prism/src/parser/ast/ExpressionAccumulation.java
  4. 8
      prism/src/parser/visitor/ASTTraverse.java
  5. 8
      prism/src/parser/visitor/ASTTraverseModify.java
  6. 2
      prism/src/parser/visitor/ASTVisitor.java
  7. 4
      prism/src/parser/visitor/ReplaceAccumulationBox.java

14
prism/src/parser/PrismParser.jj

@ -1155,7 +1155,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
//Accumulation
ExpressionAccumulation accexp;
AccumulationConstraint constr;
AccumulationConstraintBasic constr;
TemporalOperatorBound bound;
Expression reg;
ArrayList<Expression> fireOn;
@ -1189,7 +1189,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
// Weight constraint
<LBRACE>
(
constr = ExpressionAccumulationConstraint()
constr = ExpressionAccumulationConstraintBasic()
{ accexp.setConstraint(constr); }
)
<RBRACE>
@ -1241,7 +1241,7 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) :
ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathprop) :
{
ExpressionAccumulation ret;
AccumulationConstraint constr;
AccumulationConstraintBasic constr;
TemporalOperatorBound bound;
Expression reg;
ArrayList<Expression> fireOn;
@ -1265,7 +1265,7 @@ ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathpro
// Weight constraint
<LBRACE>
(
constr = ExpressionAccumulationConstraint()
constr = ExpressionAccumulationConstraintBasic()
{ ret.setConstraint(constr); }
)
<RBRACE>
@ -1297,9 +1297,9 @@ ArrayList<Expression> ExpressionAccumulationFire() :
{ return ret; }
}
AccumulationConstraint ExpressionAccumulationConstraint() :
AccumulationConstraintBasic ExpressionAccumulationConstraintBasic() :
{
AccumulationConstraint ret;
AccumulationConstraintBasic ret;
ArrayList<AccumulationFactor> factors;
TemporalOperatorBound bound;
}
@ -1307,7 +1307,7 @@ AccumulationConstraint ExpressionAccumulationConstraint() :
// (LiCo = Constant)
factors = ExpressionAccumulationLinearCombination()
bound = BoundExpression()
{ return new AccumulationConstraint(factors, bound); }
{ return new AccumulationConstraintBasic(factors, bound); }
}
ArrayList<AccumulationFactor> ExpressionAccumulationLinearCombination() :

12
prism/src/parser/ast/AccumulationConstraint.java → prism/src/parser/ast/AccumulationConstraintBasic.java

@ -5,12 +5,12 @@ import java.util.ArrayList;
import parser.visitor.ASTVisitor;
import prism.PrismLangException;
public class AccumulationConstraint extends ASTElement {
public class AccumulationConstraintBasic extends ASTElement {
private ArrayList<AccumulationFactor> factors;
private TemporalOperatorBound bound;
public AccumulationConstraint(ArrayList<AccumulationFactor> factors,
public AccumulationConstraintBasic(ArrayList<AccumulationFactor> factors,
TemporalOperatorBound bound) {
this.factors = factors;
this.bound = bound;
@ -32,13 +32,13 @@ public class AccumulationConstraint extends ASTElement {
this.bound = bound;
}
public AccumulationConstraint negate() {
AccumulationConstraint result = this.deepCopy();
public AccumulationConstraintBasic negate() {
AccumulationConstraintBasic result = this.deepCopy();
result.setBound(result.getBound().invert());
return result;
}
public AccumulationConstraint deepCopy() {
public AccumulationConstraintBasic deepCopy() {
ArrayList<AccumulationFactor> factorscopy = new ArrayList<AccumulationFactor>();
TemporalOperatorBound boundcopy = bound.deepCopy();
@ -46,7 +46,7 @@ public class AccumulationConstraint extends ASTElement {
factorscopy.add(factor.deepCopy());
}
return new AccumulationConstraint(factorscopy,boundcopy);
return new AccumulationConstraintBasic(factorscopy,boundcopy);
}
public String toString()

6
prism/src/parser/ast/ExpressionAccumulation.java

@ -38,7 +38,7 @@ import prism.PrismLangException;
public class ExpressionAccumulation extends Expression
{
AccumulationSymbol symbol;
AccumulationConstraint constraint;
AccumulationConstraintBasic constraint;
ExpressionRegular regexp;
TemporalOperatorBound bound;
ArrayList<Expression> recordSet;
@ -81,10 +81,10 @@ public class ExpressionAccumulation extends Expression
public void setSymbol(AccumulationSymbol symbol) {
this.symbol = symbol;
}
public AccumulationConstraint getConstraint() {
public AccumulationConstraintBasic getConstraint() {
return constraint;
}
public void setConstraint(AccumulationConstraint constraint) {
public void setConstraint(AccumulationConstraintBasic constraint) {
this.constraint = constraint;
}
public ExpressionRegular getRegularExpression() {

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

@ -418,7 +418,7 @@ public class ASTTraverse implements ASTVisitor
return null;
}
public void visitPost(ExpressionAccumulation e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
// -----------------------------------------------------------------------------------
public void visitPre(AccumulationFactor e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(AccumulationFactor e) throws PrismLangException
{
@ -428,8 +428,8 @@ public class ASTTraverse implements ASTVisitor
return null;
}
public void visitPost(AccumulationFactor e) throws PrismLangException { defaultVisitPost(e); }
public void visitPre(AccumulationConstraint e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(AccumulationConstraint e) throws PrismLangException
public void visitPre(AccumulationConstraintBasic e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(AccumulationConstraintBasic e) throws PrismLangException
{
visitPre(e);
for (AccumulationFactor factor : e.getFactors()) {
@ -439,7 +439,7 @@ public class ASTTraverse implements ASTVisitor
visitPost(e);
return null;
}
public void visitPost(AccumulationConstraint e) throws PrismLangException { defaultVisitPost(e); }
public void visitPost(AccumulationConstraintBasic e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(ExpressionITE e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(ExpressionITE e) throws PrismLangException

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

@ -429,7 +429,7 @@ public class ASTTraverseModify implements ASTVisitor
return e;
}
public void visitPost(ExpressionAccumulation e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
// -----------------------------------------------------------------------------------
public void visitPre(AccumulationFactor e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(AccumulationFactor e) throws PrismLangException
{
@ -439,8 +439,8 @@ public class ASTTraverseModify implements ASTVisitor
return e;
}
public void visitPost(AccumulationFactor e) throws PrismLangException { defaultVisitPost(e); }
public void visitPre(AccumulationConstraint e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(AccumulationConstraint e) throws PrismLangException
public void visitPre(AccumulationConstraintBasic e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(AccumulationConstraintBasic e) throws PrismLangException
{
visitPre(e);
for (AccumulationFactor factor : e.getFactors()) {
@ -450,7 +450,7 @@ public class ASTTraverseModify implements ASTVisitor
visitPost(e);
return e;
}
public void visitPost(AccumulationConstraint e) throws PrismLangException { defaultVisitPost(e); }
public void visitPost(AccumulationConstraintBasic e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(ExpressionITE e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(ExpressionITE e) throws PrismLangException

2
prism/src/parser/visitor/ASTVisitor.java

@ -52,7 +52,7 @@ public interface ASTVisitor
public Object visit(RewardStruct e) throws PrismLangException;
public Object visit(RewardStructItem e) throws PrismLangException;
public Object visit(AccumulationFactor e) throws PrismLangException;
public Object visit(AccumulationConstraint e) throws PrismLangException;
public Object visit(AccumulationConstraintBasic e) throws PrismLangException;
public Object visit(QuotedString quotedString) throws PrismLangException;
// ASTElement/SystemDefn classes
public Object visit(SystemInterleaved e) throws PrismLangException;

4
prism/src/parser/visitor/ReplaceAccumulationBox.java

@ -1,6 +1,6 @@
package parser.visitor;
import parser.ast.AccumulationConstraint;
import parser.ast.AccumulationConstraintBasic;
import parser.ast.AccumulationSymbol;
import parser.ast.Expression;
import parser.ast.ExpressionAccumulation;
@ -25,7 +25,7 @@ public class ReplaceAccumulationBox extends ASTTraverseModify {
if (!sym.isBox()) { return expr; }
// Negate the constraint
AccumulationConstraint newConstr = accexp.getConstraint().negate();
AccumulationConstraintBasic newConstr = accexp.getConstraint().negate();
// Switch the symbol
AccumulationSymbol newSym;

Loading…
Cancel
Save