From 883fc69e23b7dce3405b6893862aec9e2f5bd6f9 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 23 Aug 2016 15:02:21 +0000
Subject: [PATCH] Add "reach" option to -exportstrat (not actually used yet)
 [from Ganindu Prabhashana].

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11691 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Prism.java   | 18 ++++++++++++++++++
 prism/src/prism/PrismCL.java | 11 +++++++++++
 2 files changed, 29 insertions(+)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 8d496d8b..9c3bfca5 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -195,6 +195,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	protected boolean storeVector = false;
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false;
+	// Should any generated strategies should be restricted to the states reachable under them?
+	protected boolean restrictStratToReach = false;
 	// Do bisimulation minimisation before model checking?
 	protected boolean doBisim = false;
 
@@ -594,6 +596,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		this.genStrat = genStrat;
 	}
 
+	/**
+	 * Specify whether or not any generated strategies should be restricted to the states reachable under them.
+	 */
+	public void setRestrictStratToReach(boolean restrictStratToReach)
+	{
+		this.restrictStratToReach = restrictStratToReach;
+	}
+
 	/**
 	 * Specify whether or not to do bisimulation minimisation before model checking.
 	 */
@@ -928,6 +938,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		return genStrat;
 	}
 
+	/**
+	 * Whether or not any generated strategies should be restricted to the states reachable under them.
+	 */
+	public boolean getRestrictStratToReach()
+	{
+		return restrictStratToReach;
+	}
+
 	/**
 	 * Whether or not to do bisimulation minimisation before model checking.
 	 */
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 6795a287..a1fe642b 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -1985,6 +1985,17 @@ public class PrismCL implements PrismModelListener
 				else
 					throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat");
 			}
+			else if (opt.startsWith("reach")) {
+				if (!opt.startsWith("reach="))
+					throw new PrismException("No value provided for \"reach\" option of -exportstrat");
+				String optVal = opt.substring(6);
+				if (optVal.equals("true"))
+					prism.setRestrictStratToReach(true);
+				else if (optVal.equals("false"))
+					prism.setRestrictStratToReach(false);
+				else
+					throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat");
+			}
 			// Unknown option
 			else {
 				throw new PrismException("Unknown option \"" + opt + "\" for -exportstrat switch");