From 16231307d647a53272da234f8c5a793a6596f13c Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 26 Aug 2010 15:29:21 +0000
Subject: [PATCH] c-closure fixes for PTAs (was missing from new forwards
 recahability algorithm).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2056 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/pta/ForwardsReach.java | 12 +++++++++---
 prism/src/pta/LocZone.java       | 25 +++++++++++--------------
 2 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/prism/src/pta/ForwardsReach.java b/prism/src/pta/ForwardsReach.java
index 919529e0..16ddf88b 100644
--- a/prism/src/pta/ForwardsReach.java
+++ b/prism/src/pta/ForwardsReach.java
@@ -161,8 +161,10 @@ public class ForwardsReach
 				count = 0;
 				for (Edge edge : transition.getEdges()) {
 					// Do "discrete post" for this edge
+					// (followed by c-closure)
 					lz2 = lz.deepCopy();
 					lz2.dPost(edge);
+					lz2.cClosure(pta);
 					// If non-empty, create edge, also adding state to X if new 
 					if (!lz2.zone.isEmpty()) {
 						if (Yset.add(lz2)) {
@@ -263,9 +265,10 @@ public class ForwardsReach
 
 		// Build initial symbolic state (NB: assume initial location = 0)
 		z = DBM.createZero(pta);
-		z.up(pta.getInvariantConstraints(0));
-		z.cClosure(cMax);
 		init = new LocZone(0, z);
+		// And do tpost/c-closure
+		init.tPost(pta);
+		init.cClosure(pta);
 
 		// Reachability loop
 		Zset.add(init);
@@ -300,8 +303,11 @@ public class ForwardsReach
 				count = 0;
 				for (Edge edge : transition.getEdges()) {
 					// Build "post" zone for this edge
+					// (dpost, then tpost, then c-closure) 
 					lz2 = lz.deepCopy();
-					lz2.post(edge);
+					lz2.dPost(edge);
+					lz2.tPost(pta);
+					lz2.cClosure(pta);
 					// If non-empty, create edge, also adding state to Y if new 
 					if (!lz2.zone.isEmpty()) {
 						if (Zset.add(lz2)) {
diff --git a/prism/src/pta/LocZone.java b/prism/src/pta/LocZone.java
index 66e376a0..35210ac7 100644
--- a/prism/src/pta/LocZone.java
+++ b/prism/src/pta/LocZone.java
@@ -40,26 +40,13 @@ public class LocZone
 	}
 
 	/**
-	 * Do combined discrete *then* time post operation wrt. an edge.
-	 * Note: time part includes c-closure.
-	 */
-	public void post(Edge edge)
-	{
-		PTA pta = edge.getParent().getParent();
-		dPost(edge);
-		tPost(pta);
-	}
-
-	/**
-	 * Do time part of post operation (including c-closure).
+	 * Do time part of post operation (not including c-closure).
 	 * Note: pta is passed in just for efficiency, could find it if we wanted.
 	 */
 	public void tPost(PTA pta)
 	{
 		// Time successor (up)
 		zone.up(pta.getInvariantConstraints(loc));
-		// c-Closure
-		zone.cClosure(pta.getMaxClockConstraint());
 	}
 	
 	/**
@@ -82,6 +69,16 @@ public class LocZone
 		loc = edge.getDestination();
 	}
 
+	/**
+	 * Do c-closure.
+	 * Note: pta is passed in just for efficiency, could find it if we wanted.
+	 */
+	public void cClosure(PTA pta)
+	{
+		// c-Closure
+		zone.cClosure(pta.getMaxClockConstraint());
+	}
+	
 	/**
 	 * dPre: discrete predecessor
 	 */