From 4e23441d172fc163429e1e51b0908e44bad76ab2 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 22 Dec 2016 13:16:08 +0000
Subject: [PATCH] ProbModel/NondetModel: add doReachability with seed states

Sometimes, we have additional knowledge which states of the model
(apart from the initial states) are guaranteed to be reachable.
The added method then provides a way to start the reachability computation
with those states as the seed, which can speed up the computation as less
unknown states have to be discovered.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11938 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NondetModel.java | 33 ++++++++++++++++++++++++++++++++
 prism/src/prism/ProbModel.java   | 21 ++++++++++++++++++++
 2 files changed, 54 insertions(+)

diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java
index 2b2e03f6..a21ae970 100644
--- a/prism/src/prism/NondetModel.java
+++ b/prism/src/prism/NondetModel.java
@@ -214,6 +214,39 @@ public class NondetModel extends ProbModel
 		setReach(reachable);
 	}
 
+	/**
+	 * Compute and store the set of reachable states,
+	 * where the parameter {@seed} provides an initial set of states
+	 * known to be reachable.
+	 * <br/>
+	 * Starts reachability computation from the union of {@code seed} and {@start}.
+	 * <br/>[ REFS: <i>result</i>, DEREFS: seed ]
+	 * @param seed set of states (over ddRowVars) that is known to be reachable
+	 */
+	public void doReachability(JDDNode seed)
+	{
+		JDDNode tmp;
+
+		// do sanity check on seed if checking is enabled
+		if (SanityJDD.enabled)
+			SanityJDD.checkIsStateSet(seed, getAllDDRowVars());
+
+		// remove any nondeterminism from the 0/1-transition function
+		JDD.Ref(trans01);
+		tmp = JDD.MaxAbstract(trans01, allDDNondetVars);
+
+		// S = union of initial states and seed. seed is dereferenced here.
+		JDDNode S = JDD.Or(start.copy(), seed);
+
+		// compute reachable states
+		JDDNode reachable = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, S);
+		JDD.Deref(tmp);
+		JDD.Deref(S);
+
+		// set the reachable states, compute numStates, create the ODD, etc
+		setReach(reachable);
+	}
+
 	// remove non-reachable states from various dds
 	// (and calculate num transitions, etc.)
 	// (and build mask)
diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java
index cef47c55..dbc4c1a4 100644
--- a/prism/src/prism/ProbModel.java
+++ b/prism/src/prism/ProbModel.java
@@ -570,6 +570,27 @@ public class ProbModel implements Model
 		setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, start));
 	}
 
+	/**
+	 * Compute and store the set of reachable states, where the parameter {@seed}
+	 * provides an initial set of states known to be reachable.
+	 * <br/>
+	 * Starts reachability computation from the union of {@code seed} and {@start}.
+	 * <br/>[ REFS: <i>result</i>, DEREFS: seed ]
+	 * @param seed set of states (over ddRowVars) that is known to be reachable
+	 */
+	public void doReachability(JDDNode seed)
+	{
+		// do sanity check on seed if checking is enabled
+		if (SanityJDD.enabled)
+			SanityJDD.checkIsStateSet(seed, getAllDDRowVars());
+
+		// S = union of initial states and seed. seed is dereferenced here.
+		JDDNode S = JDD.Or(start.copy(), seed);
+		// compute and store reachable states
+		setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, S));
+		JDD.Deref(S);
+	}
+
 	// this method allows you to skip the reachability phase
 	// it is only here for experimental purposes - not general use.