From 8775d3a99303fe06adc54d1dd25206cdcb21915d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 1 Dec 2015 10:40:42 +0000
Subject: [PATCH] Small fix in Expression static constructors to make return
 types more clearly specified. [from Steffen Marcker]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10959 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ast/Expression.java | 39 +++++++++++++++++-----------
 1 file changed, 24 insertions(+), 15 deletions(-)

diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 1b61c050..ffaa345b 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -533,27 +533,27 @@ public abstract class Expression extends ASTElement
 
 	// Static constructors for convenience
 
-	public static Expression True()
+	public static ExpressionLiteral True()
 	{
 		return new ExpressionLiteral(TypeBool.getInstance(), true);
 	}
 
-	public static Expression False()
+	public static ExpressionLiteral False()
 	{
 		return new ExpressionLiteral(TypeBool.getInstance(), false);
 	}
 
-	public static Expression Int(int i)
+	public static ExpressionLiteral Int(int i)
 	{
 		return new ExpressionLiteral(TypeInt.getInstance(), i);
 	}
 
-	public static Expression Double(double d)
+	public static ExpressionLiteral Double(double d)
 	{
 		return new ExpressionLiteral(TypeDouble.getInstance(), d);
 	}
 
-	public static Expression Literal(Object o) throws PrismLangException
+	public static ExpressionLiteral Literal(Object o) throws PrismLangException
 	{
 		if (o instanceof Integer) {
 			return Int(((Integer) o).intValue());
@@ -566,56 +566,65 @@ public abstract class Expression extends ASTElement
 		}
 	}
 
-	public static Expression Not(Expression expr)
+	public static ExpressionUnaryOp Not(Expression expr)
 	{
 		return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, expr);
 	}
 
-	public static Expression And(Expression expr1, Expression expr2)
+	public static ExpressionBinaryOp And(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.AND, expr1, expr2);
 	}
 
-	public static Expression Or(Expression expr1, Expression expr2)
+	public static ExpressionBinaryOp Or(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.OR, expr1, expr2);
 	}
 
-	public static Expression Iff(Expression expr1, Expression expr2)
+	public static ExpressionBinaryOp Iff(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.IFF, expr1, expr2);
 	}
 
-	public static Expression Implies(Expression expr1, Expression expr2)
+	public static ExpressionBinaryOp Implies(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, expr1, expr2);
 	}
 
-	public static Expression Plus(Expression expr1, Expression expr2)
+	public static ExpressionBinaryOp Plus(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.PLUS, expr1, expr2);
 	}
 
-	public static Expression Minus(Expression expr1, Expression expr2)
+	public static ExpressionUnaryOp Minus(Expression expr)
+	{
+		return new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, expr);
+	}
+
+	public static ExpressionBinaryOp Minus(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.MINUS, expr1, expr2);
 	}
 
-	public static Expression Times(Expression expr1, Expression expr2)
+	public static ExpressionBinaryOp Times(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.TIMES, expr1, expr2);
 	}
 
-	public static Expression Divide(Expression expr1, Expression expr2)
+	public static ExpressionBinaryOp Divide(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.DIVIDE, expr1, expr2);
 	}
 
-	public static Expression Parenth(Expression expr)
+	public static ExpressionUnaryOp Parenth(Expression expr)
 	{
 		return new ExpressionUnaryOp(ExpressionUnaryOp.PARENTH, expr);
 	}
 
+	public static ExpressionTemporal Next(Expression expr) {
+		return new ExpressionTemporal(ExpressionTemporal.P_X, null, expr);
+	}
+
 	// Static testers for convenience
 
 	public static boolean isTrue(Expression expr)