From 20712738e2bd969ed927a02dfe74bb753bb11cb2 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Thu, 13 Dec 2018 09:49:05 +0100 Subject: [PATCH] Clean up --- .../explicit/AccumulationTransformation.java | 3 ++ prism/src/parser/PrismParser.jj | 49 +------------------ .../parser/ast/ExpressionAccumulation.java | 4 ++ 3 files changed, 9 insertions(+), 47 deletions(-) diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index c41adbcc..ee4318ad 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -73,6 +73,9 @@ public class AccumulationTransformation 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()) { diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 53a4c152..a2c4756e 100644 --- a/prism/src/parser/PrismParser.jj +++ b/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 { accexp = new ExpressionAccumulation(AccumulationSymbol.ACCUNTIL); accexp.setOperand1(ret); } // Regular expression, should be star-free @@ -1201,6 +1202,7 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : )? 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 fireOn; - - Expression op1; - Expression op2; -} -{ - - ( op1 = Expression(prop, pathprop) { ret.setOperand1(op1); } ) - - - // Accumulation symbol - - // Regular expression, should be star-free - - ( - ( reg = ExpressionRegularUnary(prop, false) { ret.setRegularExpression((ExpressionRegular)reg); } ) - | ( bound = BoundExpression() { ret.setBoundExpression(bound); } ) - ) - - // Weight constraint - - ( - constr = ExpressionAccumulationConstraint() - { ret.setConstraint(constr); } - ) - - // Fire set (= !StutterSet) - ( - ( - fireOn = ExpressionAccumulationFire() - { ret.setFireOn(fireOn); } - ) - )? - - - ( op2 = Expression(prop, pathprop) { ret.setOperand2(op2); } ) - - { return ret; } -} - ArrayList ExpressionAccumulationFire() : { ArrayList ret = new ArrayList(); diff --git a/prism/src/parser/ast/ExpressionAccumulation.java b/prism/src/parser/ast/ExpressionAccumulation.java index 75d8f90b..b93affc1 100644 --- a/prism/src/parser/ast/ExpressionAccumulation.java +++ b/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 = "";