Add -exportprodvector switch, which exports solution vector over product model after checking LTL-based properties. Currently, supported in explicit engine, or symbolic engines where the result ends up being a vector of doubles (not an MTBDD).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11305 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCModelChecker.java

@@ -114,6 +114,14 @@ public class DTMCModelChecker extends ProbModelChecker
 		mcProduct.inheritSettings(this);
 		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs(product.getProductModel(), acc).soln, product.getProductModel());
 
+		// Output vector over product, if required
+		if (getExportProductVector()) {
+				mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"...");
+				PrismFileLog out = new PrismFileLog(getExportProductVectorFilename());
+				probsProduct.print(out, false, false, false, false);
+				out.close();
+		}
+		
 		// Mapping probabilities in the original model
 		probs = product.projectToOriginalModel(probsProduct);
 		probsProduct.clear();
@@ -177,6 +185,14 @@ public class DTMCModelChecker extends ProbModelChecker
 		mcProduct.inheritSettings(this);
 		rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc).soln, product.getProductModel());
 		
+		// Output vector over product, if required
+		if (getExportProductVector()) {
+				mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"...");
+				PrismFileLog out = new PrismFileLog(getExportProductVectorFilename());
+				rewardsProduct.print(out, false, false, false, false);
+				out.close();
+		}
+		
 		// Mapping rewards in the original model
 		rewards = product.projectToOriginalModel(rewardsProduct);
 		rewardsProduct.clear();

prism/src/explicit/MDPModelChecker.java

@@ -131,6 +131,14 @@ public class MDPModelChecker extends ProbModelChecker
 			probsProduct.plusConstant(1.0);
 		}
 
+		// Output vector over product, if required
+		if (getExportProductVector()) {
+				mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"...");
+				PrismFileLog out = new PrismFileLog(getExportProductVectorFilename());
+				probsProduct.print(out, false, false, false, false);
+				out.close();
+		}
+		
 		// Mapping probabilities in the original model
 		probs = product.projectToOriginalModel(probsProduct);
 		probsProduct.clear();
@@ -196,6 +204,14 @@ public class MDPModelChecker extends ProbModelChecker
 		mcProduct.inheritSettings(this);
 		rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc, minMax.isMin()).soln, product.getProductModel());
 		
+		// Output vector over product, if required
+		if (getExportProductVector()) {
+				mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"...");
+				PrismFileLog out = new PrismFileLog(getExportProductVectorFilename());
+				rewardsProduct.print(out, false, false, false, false);
+				out.close();
+		}
+		
 		// Mapping rewards in the original model
 		rewards = product.projectToOriginalModel(rewardsProduct);
 		rewardsProduct.clear();

prism/src/explicit/StateModelChecker.java

@@ -101,6 +101,8 @@ public class StateModelChecker extends PrismComponent
 	protected String exportProductTransFilename = null;
 	protected boolean exportProductStates = false;
 	protected String exportProductStatesFilename = null;
+	protected boolean exportProductVector = false;
+	protected String exportProductVectorFilename = null;
 	
 	// Store the final results vector after model checking?
 	protected boolean storeVector = false;
@@ -200,6 +202,8 @@ public class StateModelChecker extends PrismComponent
 		setExportProductTransFilename(other.getExportProductTransFilename());
 		setExportProductStates(other.getExportProductStates());
 		setExportProductStatesFilename(other.getExportProductStatesFilename());
+		setExportProductVector(other.getExportProductVector());
+		setExportProductVectorFilename(other.getExportProductVectorFilename());
 		setStoreVector(other.getStoreVector());
 		setGenStrat(other.getGenStrat());
 		setDoBisim(other.getDoBisim());
@@ -253,6 +257,16 @@ public class StateModelChecker extends PrismComponent
 		exportProductStatesFilename = s;
 	}
 
+	public void setExportProductVector(boolean b)
+	{
+		exportProductVector = b;
+	}
+
+	public void setExportProductVectorFilename(String s)
+	{
+		exportProductVectorFilename = s;
+	}
+
 	/**
 	 * Specify whether or not to store the final results vector after model checking.
 	 */
@@ -314,6 +328,16 @@ public class StateModelChecker extends PrismComponent
 		return exportProductStatesFilename;
 	}
 
+	public boolean getExportProductVector()
+	{
+		return exportProductVector;
+	}
+
+	public String getExportProductVectorFilename()
+	{
+		return exportProductVectorFilename;
+	}
+
 	/**
 	 * Whether or not to store the final results vector after model checking.
 	 */

prism/src/prism/NondetModelChecker.java

@@ -1224,6 +1224,14 @@ public class NondetModelChecker extends NonProbModelChecker
 			probsProduct.subtractFromOne();
 		}
 
+		// Output vector over product, if required
+		if (prism.getExportProductVector()) {
+				mainLog.println("\nExporting product solution vector matrix to file \"" + prism.getExportProductVectorFilename() + "\"...");
+				PrismFileLog out = new PrismFileLog(prism.getExportProductVectorFilename());
+				probsProduct.print(out, false, false, false, false);
+				out.close();
+		}
+		
 		// Convert probability vector to original model
 		// First, filter over DRA start states
 		startMask = mcLtl.buildStartMask(da, labelDDs, daDDRowVars);

prism/src/prism/Prism.java

@@ -191,6 +191,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	protected String exportProductTransFilename = null;
 	protected boolean exportProductStates = false;
 	protected String exportProductStatesFilename = null;
+	protected boolean exportProductVector = false;
+	protected String exportProductVectorFilename = null;
 	// Store the final results vector after model checking?
 	protected boolean storeVector = false;
 	// Generate/store a strategy during model checking?
@@ -568,6 +570,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		exportProductStatesFilename = s;
 	}
 
+	public void setExportProductVector(boolean b) throws PrismException
+	{
+		exportProductVector = b;
+	}
+
+	public void setExportProductVectorFilename(String s) throws PrismException
+	{
+		exportProductVectorFilename = s;
+	}
+
 	/**
 	 * Specify whether or not to store the final results vector after model checking.
 	 */
@@ -883,6 +895,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		return exportProductStatesFilename;
 	}
 
+	public boolean getExportProductVector()
+	{
+		return exportProductVector;
+	}
+
+	public String getExportProductVectorFilename()
+	{
+		return exportProductVectorFilename;
+	}
+
 	/**
 	 * Whether or not to store the final results vector after model checking.
 	 */
@@ -3625,6 +3647,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		mc.setExportProductTransFilename(exportProductTransFilename);
 		mc.setExportProductStates(exportProductStates);
 		mc.setExportProductStatesFilename(exportProductStatesFilename);
+		mc.setExportProductVector(exportProductVector);
+		mc.setExportProductVectorFilename(exportProductVectorFilename);
 		mc.setStoreVector(storeVector);
 		mc.setGenStrat(genStrat);
 		mc.setDoBisim(doBisim);

prism/src/prism/PrismCL.java

@@ -1471,6 +1471,15 @@ public class PrismCL implements PrismModelListener
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export product vector to file (hidden option)
+				else if (sw.equals("exportprodvector")) {
+					if (i < args.length - 1) {
+						prism.setExportProductVector(true);
+						prism.setExportProductVectorFilename(args[++i]);
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export model to plain text file (deprecated option so hidden)
 				else if (sw.equals("exportplain")) {
 					if (i < args.length - 1) {