From ee4f2d294192c95ad2757ff85ebd56dd35834aa9 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 30 Aug 2016 13:47:54 +0000
Subject: [PATCH] ExpressionTemporal: static constructors for the temporal
 operators

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

diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java
index 1024ebaf..528a34d2 100644
--- a/prism/src/parser/ast/ExpressionTemporal.java
+++ b/prism/src/parser/ast/ExpressionTemporal.java
@@ -486,6 +486,45 @@ public class ExpressionTemporal extends Expression
 		return isFinally(e) && isGlobally(((ExpressionTemporal) e).getOperand2());
 	}
 
+
+	// ---- static constructors for building temporal expressions -----------------
+
+	/** Construct a ExpressionTemporal for "X expr" */
+	public static ExpressionTemporal Next(Expression expr)
+	{
+		return new ExpressionTemporal(P_X, null, expr);
+	}
+
+	/** Construct a ExpressionTemporal for "F expr" */
+	public static ExpressionTemporal Finally(Expression expr)
+	{
+		return new ExpressionTemporal(P_F, null, expr);
+	}
+
+	/** Construct a ExpressionTemporal for "G expr" */
+	public static ExpressionTemporal Globally(Expression expr)
+	{
+		return new ExpressionTemporal(P_G, null, expr);
+	}
+
+	/** Construct a ExpressionTemporal for "expr1 U expr2" */
+	public static ExpressionTemporal Globally(Expression expr1, Expression expr2)
+	{
+		return new ExpressionTemporal(P_U, expr1, expr2);
+	}
+
+	/** Construct a ExpressionTemporal for "expr1 W expr2" */
+	public static ExpressionTemporal WeakUntil(Expression expr1, Expression expr2)
+	{
+		return new ExpressionTemporal(P_W, expr1, expr2);
+	}
+
+	/** Construct a ExpressionTemporal for "expr1 R expr2" */
+	public static ExpressionTemporal Release(Expression expr1, Expression expr2)
+	{
+		return new ExpressionTemporal(P_R, expr1, expr2);
+	}
+
 }
 
 //------------------------------------------------------------------------------