From f4ab03013f50cde5c7c51b1623f8cd9cb95be882 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 6 Jul 2015 10:57:28 +0000
Subject: [PATCH] Add methods to the explicit.Model interface to get a (cached)
 PredecessorRelation. [from Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10192 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/Model.java          | 19 +++++++++++++++-
 prism/src/explicit/ModelExplicit.java  | 30 ++++++++++++++++++++++++++
 prism/src/explicit/SubNondetModel.java | 29 +++++++++++++++++++++++++
 3 files changed, 77 insertions(+), 1 deletion(-)

diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java
index fbdd2362..8a420a52 100644
--- a/prism/src/explicit/Model.java
+++ b/prism/src/explicit/Model.java
@@ -253,4 +253,21 @@ public interface Model
 	 * Report info/stats about the model, tabulated, as a string.
 	 */
 	public String infoStringTable();
-}
\ No newline at end of file
+
+	/** Has this model a stored PredecessorRelation? */
+	public boolean hasStoredPredecessorRelation();
+
+	/**
+	 * If there is a PredecessorRelation stored for this model, return that.
+	 * Otherwise, create one and return that. If {@code storeIfNew},
+	 * store it for later use.
+	 *
+	 * @param parent a PrismComponent (for obtaining the log)
+	 * @param storeIfNew if the predecessor relation is newly created, store it
+	 */
+	public PredecessorRelation getPredecessorRelation(prism.PrismComponent parent, boolean storeIfNew);
+
+	/** Clear any stored predecessor relation, e.g., because the model was modified */
+	public void clearPredecessorRelation();
+
+}
diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index 301dd84a..dfda6bd0 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/prism/src/explicit/ModelExplicit.java
@@ -69,6 +69,11 @@ public abstract class ModelExplicit implements Model
 	/** (Optionally) some labels (atomic propositions) associated with the model,
 	 * represented as a String->BitSet mapping from their names to the states that satisfy them. */
 	protected Map<String, BitSet> labels = new TreeMap<String, BitSet>();
+	
+	/**
+	 * (Optionally) the stored predecessor relation. Becomes inaccurate after the model is changed!
+	 */
+	protected PredecessorRelation predecessorRelation = null;
 
 	// Mutators
 
@@ -439,4 +444,29 @@ public abstract class ModelExplicit implements Model
 			return false;
 		return true;
 	}
+
+	@Override
+	public boolean hasStoredPredecessorRelation() {
+		return (predecessorRelation != null);
+	}
+
+	@Override
+	public PredecessorRelation getPredecessorRelation(prism.PrismComponent parent, boolean storeIfNew) {
+		if (predecessorRelation != null) {
+			return predecessorRelation;
+		}
+
+		PredecessorRelation pre = PredecessorRelation.forModel(parent, this);
+
+		if (storeIfNew) {
+			predecessorRelation = pre;
+		}
+		return pre;
+	}
+
+	@Override
+	public void clearPredecessorRelation() {
+		predecessorRelation = null;
+	}
+
 }
\ No newline at end of file
diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java
index bd2d34d3..dcf55342 100644
--- a/prism/src/explicit/SubNondetModel.java
+++ b/prism/src/explicit/SubNondetModel.java
@@ -62,6 +62,11 @@ public class SubNondetModel implements NondetModel
 	private Map<Integer, Map<Integer, Integer>> actionLookupTable = new HashMap<Integer, Map<Integer, Integer>>();
 	private Map<Integer, Integer> inverseStateLookupTable = new HashMap<Integer, Integer>();
 
+	/**
+	 * (Optionally) the stored predecessor relation. Becomes inaccurate after the model is changed!
+	 */
+	protected PredecessorRelation predecessorRelation;
+
 	private int numTransitions = 0;
 	private int maxNumChoices = 0;
 	private int numChoices = 0;
@@ -495,4 +500,28 @@ public class SubNondetModel implements NondetModel
 	{
 		return actionLookupTable.get(s).get(i);
 	}
+
+	@Override
+	public boolean hasStoredPredecessorRelation() {
+		return (predecessorRelation != null);
+	}
+
+	@Override
+	public PredecessorRelation getPredecessorRelation(prism.PrismComponent parent, boolean storeIfNew) {
+		if (predecessorRelation != null) {
+			return predecessorRelation;
+		}
+
+		PredecessorRelation pre = PredecessorRelation.forModel(parent, this);
+
+		if (storeIfNew) {
+			predecessorRelation = pre;
+		}
+		return pre;
+	}
+
+	@Override
+	public void clearPredecessorRelation() {
+		predecessorRelation = null;
+	}
 }