Browse Source

Clean up

accumulation
Sascha Wunderlich 7 years ago
parent
commit
20712738e2
  1. 3
      prism/src/explicit/AccumulationTransformation.java
  2. 49
      prism/src/parser/PrismParser.jj
  3. 4
      prism/src/parser/ast/ExpressionAccumulation.java

3
prism/src/explicit/AccumulationTransformation.java

@ -73,6 +73,9 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
// Get the first ExpressionAccumulation
ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression();
mc.getLog().println(" [AT] for " + accexp);
if (accexp.isNullary() && !accexp.hasFireOn()) {
mc.getLog().println(" ... a simple expression.");
}
// Get the rewards and build the product
switch(originalModel.getModelType()) {

49
prism/src/parser/PrismParser.jj

@ -1176,6 +1176,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
expr = ExpressionTemporalUnary(prop, pathprop)
{ exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp; }
|
// START ACCUMULATION
// Accumulation symbol
<ACCUNTIL> { accexp = new ExpressionAccumulation(AccumulationSymbol.ACCUNTIL); accexp.setOperand1(ret); }
// Regular expression, should be star-free
@ -1201,6 +1202,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
<RPARENTH>)?
ret = ExpressionTemporalUnary(prop, pathprop)
{ accexp.setOperand2(ret); ret = accexp; }
// END ACCUMULATION
)?
{ return ret; }
}
@ -1276,53 +1278,6 @@ ExpressionAccumulation ExpressionAccumulationNullary(boolean prop, boolean pathp
{ return ret; }
}
ExpressionAccumulation ExpressionAccumulationBinary(boolean prop, boolean pathprop) :
{
ExpressionAccumulation ret = new ExpressionAccumulation(AccumulationSymbol.ACCUNTIL);
AccumulationConstraint constr;
TemporalOperatorBound bound;
Expression reg;
ArrayList<Expression> fireOn;
Expression op1;
Expression op2;
}
{
<LPARENTH>
( op1 = Expression(prop, pathprop) { ret.setOperand1(op1); } )
<RPARENTH>
// Accumulation symbol
<ACCUNTIL>
// Regular expression, should be star-free
<LPARENTH>
(
( <REGEXP_MARKER> reg = ExpressionRegularUnary(prop, false) { ret.setRegularExpression((ExpressionRegular)reg); } )
| ( bound = BoundExpression() { ret.setBoundExpression(bound); } )
)
<RPARENTH>
// Weight constraint
<LPARENTH>
(
constr = ExpressionAccumulationConstraint()
{ ret.setConstraint(constr); }
)
<RPARENTH>
// Fire set (= !StutterSet)
(<LPARENTH>
(
fireOn = ExpressionAccumulationFire()
{ ret.setFireOn(fireOn); }
)
<RPARENTH>)?
<LPARENTH>
( op2 = Expression(prop, pathprop) { ret.setOperand2(op2); } )
<RPARENTH>
{ return ret; }
}
ArrayList<Expression> ExpressionAccumulationFire() :
{
ArrayList<Expression> ret = new ArrayList<Expression>();

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

@ -122,6 +122,10 @@ public class ExpressionAccumulation extends Expression
return fireOn != null;
}
public boolean isNullary() {
return symbol.isDia() || symbol.isBox();
}
// Add a toString
public String toString() {
String ret = "";

Loading…
Cancel
Save