More refactoring of ExpressionQuant and add "mode" field, currently ignored.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10032 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/parser/PrismParser.jj

@@ -1454,6 +1454,7 @@ Expression ExpressionParenth(boolean prop, boolean pathprop) :
 
 Expression ExpressionProb(boolean prop, boolean pathprop) :
 {
+	ExpressionIdent mode = null;
 	int r;
 	String relOp = null;
 	Expression prob = null;
@@ -1467,7 +1468,8 @@ Expression ExpressionProb(boolean prop, boolean pathprop) :
 	// This production is only allowed in expressions if the "prop" parameter is true
 	{ if (!prop) throw generateParseException(); }
 	// Various options for "P" keyword and attached symbols
-	(( begin = <P> (( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } )
+	(( begin = <P> ( <LPARENTH> mode = IdentifierExpression() <RPARENTH> )? (
+			( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } )
 	       |( <EQ> <QMARK> { relOp = "="; isBool = false; } )
 	       |( <MIN> <EQ> <QMARK> { relOp = "min="; isBool = false; } )
 	       |( <MAX> <EQ> <QMARK> { relOp = "max="; isBool = false; } )))
@@ -1477,6 +1479,7 @@ Expression ExpressionProb(boolean prop, boolean pathprop) :
 	// Path formula, optional filter
 	<LBRACKET> expr = Expression(prop, true) (filter = Filter())? <RBRACKET>
 	{
+		ret.setMode(mode == null ? null : mode.getName());
 		ret.setRelOp(relOp);
 		ret.setProb(prob);
 		ret.setExpression(expr);

prism/src/parser/ast/ExpressionProb.java

@@ -155,7 +155,7 @@ public class ExpressionProb extends ExpressionQuant
 	{
 		String s = "";
 
-		s += "P" + getRelOp();
+		s += "P" + getModeString() + getRelOp();
 		s += (getBound() == null) ? "?" : getBound().toString();
 		s += " [ " + getExpression();
 		if (getFilter() != null)

prism/src/parser/ast/ExpressionQuant.java

@@ -36,6 +36,8 @@ import prism.PrismException;
  */
 public abstract class ExpressionQuant extends Expression
 {
+	/** Optional "mode" to specify variants of the P/R/S operator */
+	protected String mode = null;
 	/** The attached relational operator (e.g. "<" in "P<0.1"). */
 	protected RelOp relOp = null;
 	/** The attached (probability/reward) bound, as an expression (e.g. "p" in "P<p"). Null if absent (e.g. "P=?"). */
@@ -48,6 +50,14 @@ public abstract class ExpressionQuant extends Expression
 
 	// Set methods
 
+	/**
+	 * Set the (optional) "mode" for this operator.
+	 */
+	public void setMode(String mode)
+	{
+		this.mode = mode;
+	}
+
 	/**
 	 * Set the attached relational operator (e.g. "<" in "P<0.1").
 	 * Uses the enum {@link RelOp}. For example: {@code setRelOp(RelOp.GT);}
@@ -93,6 +103,22 @@ public abstract class ExpressionQuant extends Expression
 
 	// Get methods
 
+	/**
+	 * Get the (optional) "mode" for this operator.
+	 */
+	public String getMode()
+	{
+		return mode;
+	}
+
+	/**
+	 * Get a string representing the model as a suffix for the operator.
+	 */
+	public String getModeString()
+	{
+		return mode == null ? "" : "(" + mode + ")";
+	}
+
 	/**
 	 * Get the attached relational operator (e.g. "<" in "P<0.1"), as a {@link RelOp}.
 	 */

prism/src/parser/ast/ExpressionReward.java

@@ -241,7 +241,7 @@ public class ExpressionReward extends ExpressionQuant
 	{
 		String s = "";
 		
-		s += "R";
+		s += "R" + getModeString();
 		if (rewardStructIndex != null) {
 			if (rewardStructIndex instanceof Expression) s += "{"+rewardStructIndex+"}";
 			else if (rewardStructIndex instanceof String) s += "{\""+rewardStructIndex+"\"}";

prism/src/parser/ast/ExpressionSS.java

@@ -141,7 +141,7 @@ public class ExpressionSS extends ExpressionQuant
 	{
 		String s = "";
 		
-		s += "S" + getRelOp();
+		s += "S" + getModeString() + getRelOp();
 		s += (getBound()==null) ? "?" : getBound().toString();
 		s += " [ " + getExpression();
 		if (getFilter() != null) s += " "+getFilter();