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

@@ -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();

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();

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();