From ee2fa09c49860b362ec722c0eebfd543b2d1b83f Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 19 Feb 2010 22:50:20 +0000
Subject: [PATCH] Actions preserved in LTL (MDP) product for adversary export.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1754 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/LTLModelChecker.java | 17 +++++++++++++++--
 prism/src/prism/Model.java           |  2 +-
 prism/src/prism/ProbModel.java       |  6 +++---
 3 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index 54ff8a81..f93182a4 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -479,7 +479,17 @@ public class LTLModelChecker
 				model.getNumVars() + 1, newVarList, newVarDDRowVars, newVarDDColVars,
 				// Constants (no change)
 				model.getConstantValues());
-
+		
+		// Copy action info MTBDD across directly
+		// If present, just needs filtering to reachable states,
+		// which will get done below.
+		if (model.getTransActions() != null) {
+			JDD.Ref(model.getTransActions());
+			modelProd.setTransActions(model.getTransActions());
+		}
+		// Also need to copy set of action label strings
+		modelProd.setSynchs(new Vector<String>(model.getSynchs()));
+		
 		// Do reachability/etc. for the new model
 		modelProd.doReachability(prism.getExtraReachInfo());
 		modelProd.filterReachableStates();
@@ -487,7 +497,10 @@ public class LTLModelChecker
 		if (modelProd.getDeadlockStates().size() > 0) {
 			throw new PrismException("Model-DRA product has deadlock states");
 		}
-
+		
+		//try { prism.exportStatesToFile(modelProd, Prism.EXPORT_PLAIN, new java.io.File("prod.sta")); }
+		//catch (java.io.FileNotFoundException e) {}
+		
 		// Reference DRA DD vars (if being returned)
 		if (draDDRowVarsCopy != null)
 			draDDRowVarsCopy.refAll();
diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java
index b013165f..23a9d901 100644
--- a/prism/src/prism/Model.java
+++ b/prism/src/prism/Model.java
@@ -98,7 +98,7 @@ public interface Model
 	
 	ODDNode getODD();
 
-	void setSynchs(Vector<String> synchs);
+	void setSynchs(List<String> synchs);
 	void resetTrans(JDDNode trans);
 	void resetTransRewards(int i, JDDNode transRewards);
 	void doReachability();
diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java
index a494c920..7e873d09 100644
--- a/prism/src/prism/ProbModel.java
+++ b/prism/src/prism/ProbModel.java
@@ -52,7 +52,7 @@ public class ProbModel implements Model
 	protected Values constantValues; // values of constants
 	// actions
 	protected int numSynchs; // number of synchronising actions
-	protected Vector<String> synchs; // synchronising action labels
+	protected List<String> synchs; // synchronising action labels
 	// rewards
 	protected int numRewardStructs; // number of reward structs
 	protected String[] rewardStructNames; // reward struct names
@@ -161,7 +161,7 @@ public class ProbModel implements Model
 	}
 
 	/**
-	 * Get vector of action label names. 
+	 * Get list of action label names. 
 	 */
 	public List<String> getSynchs()
 	{
@@ -439,7 +439,7 @@ public class ProbModel implements Model
 	/**
 	 * Set vector of action label names. 
 	 */
-	public void setSynchs(Vector<String> synchs)
+	public void setSynchs(List<String> synchs)
 	{
 		this.synchs = synchs;
 		this.numSynchs = synchs.size();