From b0f5ffeeeed9a1e0c390aedbac3a9785296cd163 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 19 Jul 2017 12:31:28 +0000
Subject: [PATCH] SimpleLTL: extendNextStepWithAP

This method transforms X phi operators to X ("label" & phi).
This will be used to ensure "strong" semantics for the next-step
operator for co-safe LTL reward computations.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12060 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/jltl2ba/SimpleLTL.java | 47 ++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/prism/src/jltl2ba/SimpleLTL.java b/prism/src/jltl2ba/SimpleLTL.java
index 67ab5c06..37a5f92f 100644
--- a/prism/src/jltl2ba/SimpleLTL.java
+++ b/prism/src/jltl2ba/SimpleLTL.java
@@ -941,6 +941,53 @@ public class SimpleLTL {
 		return true;
 	}
 
+	/**
+	 * Transform LTL formula by extend each<br>
+	 * X phi<br>
+	 * node in the syntax tree to<br>
+	 * X (label & phi).
+	 * <br>
+	 * The LTL formula has to consist only of basic operators (see toBasicOperators()).
+	 * @param label the label of the atomic proposition
+	 * @return the transformed LTL formula
+	 */
+	public SimpleLTL extendNextStepWithAP(String label)
+	{
+		switch (kind) {
+		case TRUE:
+		case FALSE:
+		case AP:
+			return this.clone();
+		case NOT: {
+			SimpleLTL newLeft = left.extendNextStepWithAP(label);
+			return new SimpleLTL(kind, newLeft);
+		}
+		case NEXT: {
+			SimpleLTL newLeft = left.extendNextStepWithAP(label);
+			// transform X phi to X ("label" & phi)
+			return new SimpleLTL(LTLType.NEXT,
+					new SimpleLTL(LTLType.AND, new SimpleLTL(label), newLeft));
+		}
+		case OR:
+		case AND:
+		case RELEASE:
+		case UNTIL: {
+			SimpleLTL newLeft = left.extendNextStepWithAP(label);
+			SimpleLTL newRight = right.extendNextStepWithAP(label);
+			return new SimpleLTL(kind, newLeft, newRight);
+		}
+		case FINALLY:
+		case GLOBALLY: {
+			SimpleLTL newLeft = left.extendNextStepWithAP(label);
+			return new SimpleLTL(kind, newLeft);
+		}
+		case EQUIV:
+		case IMPLIES:
+			throw new UnsupportedOperationException("Extending Next operator with AP not supported for " + kind.toString() + " operator, only for basic operators: " + this);
+		}
+		throw new UnsupportedOperationException();
+	}
+
 	public SimpleLTL toDNF() throws PrismException
 	{
 		switch (kind) {