accumulation: support unary accumulation ops

prism/src/explicit/AccumulationProduct.java

@@ -98,7 +98,12 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 	
 	protected final AccumulationState<Component> updateAccumulationState(final int modelFromStateId, final AccumulationState<Component> accstate, final double[] weights) throws PrismException {
 		// If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop...
-		if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; }
+		if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) {
+			// We still need to return an "empty" accstate.
+			AccumulationState<Component> newAccstate = this.accStates.getById(0);
+			newAccstate.lastRestartNr = numberOfTracks-1;
+			return newAccstate;
+		}
 		
 		// If this is not a recorded action, we can return the same accstate. Copies are made on modification.
 		if(!recordIn(modelFromStateId)) { return accstate; }

prism/src/parser/PrismParser.jj

@@ -514,10 +514,10 @@ TOKEN :
 |	< QMARK:		"?" >
 |	< CARET:		"^" >
 	// Accumulation
-|	< ACCDIAPLUS:   "<+>" >
-|	< ACCDIAMINUS:  "<->" >
-|	< ACCBOXPLUS:   "[+]" >
-|	< ACCBOXMINUS:  "[-]" >
+|	< ACCDIAPLUS:   "<+>"|"F+" >
+|	< ACCDIAMINUS:  "<->"|"F-" >
+|	< ACCBOXPLUS:   "[+]"|"G+" >
+|	< ACCBOXMINUS:  "[-]"|"G-" >
 |   < ACCUNTIL:     "U+"  >
 	// Regular expressions
 |	< REG_INT:			(["1"-"9"](["0"-"9"])*)|("0") >
@@ -1180,26 +1180,26 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) :
 		// Accumulation symbol
 		<ACCUNTIL> { accexp = new ExpressionAccumulation(AccumulationSymbol.ACCUNTIL); accexp.setOperand1(ret); }
 		// Regular expression, should be star-free
-		<LPARENTH>
+		<LBRACE>
 		(
 			  ( <REGEXP_MARKER> reg = ExpressionRegularUnary(prop, false) { accexp.setRegularExpression((ExpressionRegular)reg); } )
 			| ( bound = BoundExpression() { accexp.setBoundExpression(bound); } )
 		)
-		<RPARENTH>
+		<RBRACE>
 		// Weight constraint
-		<LPARENTH>
+		<LBRACE>
 		(
 			constr = ExpressionAccumulationConstraint()
 			{ accexp.setConstraint(constr); }
 		)
-		<RPARENTH>
-		// Fire set (= !StutterSet)
-		(<LPARENTH>
+		<RBRACE>
+		// Record set (= !StutterSet)
+		(<LBRACE>
 		(
 			fireOn = ExpressionAccumulationFire()
-			{ accexp.setFireOn(fireOn); }
+			{ accexp.setRecordSet(fireOn); }
 		)
-		<RPARENTH>)?
+		<RBRACE>)?
 		ret = ExpressionTemporalUnary(prop, pathprop)
 		{ accexp.setOperand2(ret); ret = accexp; }
 		// END ACCUMULATION
@@ -1231,20 +1231,21 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) :
 	|
 		ret = ExpressionITE(prop, pathprop)
 	|
-		ret = ExpressionAccumulationNullary(prop, pathprop)
+		ret = ExpressionAccumulationUnary(prop, pathprop)
 	)
 	{ return ret; }
 }
 
 /* START
    Accumulation Specification */
-ExpressionAccumulation ExpressionAccumulationNullary(boolean prop, boolean pathprop) :
+ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathprop) :
 {
 	ExpressionAccumulation ret;
 	AccumulationConstraint constr;
 	TemporalOperatorBound bound;
 	Expression reg;
 	ArrayList<Expression> fireOn;
+	Expression tmp;
 }
 {
 	// Accumulation symbol
@@ -1255,26 +1256,30 @@ ExpressionAccumulation ExpressionAccumulationNullary(boolean prop, boolean pathp
 		| ( <ACCBOXMINUS> { ret = new ExpressionAccumulation(AccumulationSymbol.ACCBOXMINUS); } )
 	)
 	// Regular expression, should be star-free
-	<LPARENTH>
+	<LBRACE>
 	(
 		  ( <REGEXP_MARKER> reg = ExpressionRegularUnary(prop, false) { ret.setRegularExpression((ExpressionRegular)reg); } )
 		| ( bound = BoundExpression() { ret.setBoundExpression(bound); } )
 	)
-	<RPARENTH>
+	<RBRACE>
 	// Weight constraint
-	<LPARENTH>
+	<LBRACE>
 	(
 		constr = ExpressionAccumulationConstraint()
 		{ ret.setConstraint(constr); }
 	)
-	<RPARENTH>
-	// Fire set (= !StutterSet)
-	(<LPARENTH>
+	<RBRACE>
+	// Record set (= !StutterSet)
+	(<LBRACE>
 	(
 		fireOn = ExpressionAccumulationFire()
-		{ ret.setFireOn(fireOn); }
+		{ ret.setRecordSet(fireOn); }
 	)
-	<RPARENTH>)?
+	<RBRACE>)?
+	(
+		tmp = ExpressionTemporalUnary(prop, pathprop)
+		{ ret.setOperand2(tmp); }
+	)?
 	{ return ret; }
 }
 

prism/src/parser/ast/ExpressionAccumulation.java

@@ -134,7 +134,7 @@ public class ExpressionAccumulation extends Expression
 	}
 	
 	public boolean isNullary() {
-		return symbol.isDia() || symbol.isBox();
+		return (symbol.isDia() || symbol.isBox()) && operand2 == null;
 	}
 	
 	// Add a toString