Add support for -exportprodtrans and -exportprodstates switches to explicit engine.

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

prism/src/explicit/DTMCModelChecker.java

@@ -31,10 +31,15 @@ import java.util.BitSet;
 import java.util.List;
 import java.util.Map;
 
+import parser.VarList;
+import parser.ast.Declaration;
+import parser.ast.DeclarationIntUnbounded;
 import parser.ast.Expression;
 import parser.type.TypeDouble;
+import prism.Prism;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismFileLog;
 import prism.PrismNotSupportedException;
 import prism.PrismUtils;
 import acceptance.AcceptanceReach;
@@ -74,6 +79,24 @@ public class DTMCModelChecker extends ProbModelChecker
 		};
 		product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest, allowedAcceptance);
 
+		// Output product, if required
+		if (getExportProductTrans()) {
+				mainLog.println("\nExporting product transition matrix to file \"" + getExportProductTransFilename() + "\"...");
+				product.getProductModel().exportToPrismExplicitTra(getExportProductTransFilename());
+		}
+		if (getExportProductStates()) {
+			mainLog.println("\nExporting product state space to file \"" + getExportProductStatesFilename() + "\"...");
+			PrismFileLog out = new PrismFileLog(getExportProductStatesFilename());
+			VarList newVarList = (VarList) modulesFile.createVarList().clone();
+			String daVar = "_da";
+			while (newVarList.getIndex(daVar) != -1) {
+				daVar = "_" + daVar;
+			}
+			newVarList.addVar(0, new Declaration(daVar, new DeclarationIntUnbounded()), 1, null);
+			product.getProductModel().exportStates(Prism.EXPORT_PLAIN, modulesFile.createVarList(), out);
+			out.close();
+		}
+		
 		// Find accepting states + compute reachability probabilities
 		BitSet acc;
 		if (product.getAcceptance() instanceof AcceptanceReach) {

prism/src/explicit/LTLModelChecker.java

@@ -299,7 +299,7 @@ public class LTLModelChecker extends PrismComponent
 		int prodNumStates = modelNumStates * daSize;
 		int s_1, s_2, q_1, q_2;
 		BitSet s_labels = new BitSet(numAPs);
-		List<State> prodStatesList = null;
+		List<State> prodStatesList = null, daStatesList = null;
 
 		// Encoding: 
 		// each state s' = <s, q> = s * daSize + q
@@ -312,6 +312,10 @@ public class LTLModelChecker extends PrismComponent
 
 		if (dtmc.getStatesList() != null) {
 			prodStatesList = new ArrayList<State>();
+			daStatesList = new ArrayList<State>(da.size());
+			for (int i = 0; i < da.size(); i++) {
+				daStatesList.add(new State(1).setValue(0, i));
+			}
 		}
 
 		// We need results for all states of the original model in statesOfInterest
@@ -334,7 +338,7 @@ public class LTLModelChecker extends PrismComponent
 			map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1;
 			if (prodStatesList != null) {
 				// store DTMC state information for the product state
-				prodStatesList.add(dtmc.getStatesList().get(s_0));
+				prodStatesList.add(new State(daStatesList.get(q_0), dtmc.getStatesList().get(s_0)));
 			}
 		}
 
@@ -365,7 +369,7 @@ public class LTLModelChecker extends PrismComponent
 					map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1;
 					if (prodStatesList != null) {
 						// store DTMC state information for the product state
-						prodStatesList.add(dtmc.getStatesList().get(s_2));
+						prodStatesList.add(new State(daStatesList.get(q_2), dtmc.getStatesList().get(s_2)));
 					}
 				}
 				prodModel.setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob);
@@ -444,7 +448,7 @@ public class LTLModelChecker extends PrismComponent
 		int prodNumStates = modelNumStates * daSize;
 		int s_1, s_2, q_1, q_2;
 		BitSet s_labels = new BitSet(numAPs);
-		List<State> prodStatesList = null;
+		List<State> prodStatesList = null, daStatesList = null;
 
 
 		// Encoding: 
@@ -458,6 +462,10 @@ public class LTLModelChecker extends PrismComponent
 
 		if (mdp.getStatesList() != null) {
 			prodStatesList = new ArrayList<State>();
+			daStatesList = new ArrayList<State>(da.size());
+			for (int i = 0; i < da.size(); i++) {
+				daStatesList.add(new State(1).setValue(0, i));
+			}
 		}
 
 		// We need results for all states of the original model in statesOfInterest
@@ -480,7 +488,7 @@ public class LTLModelChecker extends PrismComponent
 			map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1;
 			if (prodStatesList != null) {
 				// store MDP state information for the product state
-				prodStatesList.add(mdp.getStatesList().get(s_0));
+				prodStatesList.add(new State(daStatesList.get(q_0), mdp.getStatesList().get(s_0)));
 			}
 		}
 
@@ -514,7 +522,7 @@ public class LTLModelChecker extends PrismComponent
 						map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1;
 						if (prodStatesList != null) {
 							// store MDP state information for the product state
-							prodStatesList.add(mdp.getStatesList().get(s_2));
+							prodStatesList.add(new State(daStatesList.get(q_2), mdp.getStatesList().get(s_2)));
 						}
 					}
 					prodDistr.set(map[s_2 * daSize + q_2], prob);

prism/src/explicit/MDPModelChecker.java

@@ -31,7 +31,12 @@ import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
 
+import parser.VarList;
+import parser.ast.Declaration;
+import parser.ast.DeclarationInt;
+import parser.ast.DeclarationIntUnbounded;
 import parser.ast.Expression;
+import prism.Prism;
 import prism.PrismComponent;
 import prism.PrismDevNullLog;
 import prism.PrismException;
@@ -83,7 +88,26 @@ public class MDPModelChecker extends ProbModelChecker
 		};
 
 		product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);
-
+		mainLog.println(product.getProductModel().getStatesList());
+		
+		// Output product, if required
+		if (getExportProductTrans()) {
+				mainLog.println("\nExporting product transition matrix to file \"" + getExportProductTransFilename() + "\"...");
+				product.getProductModel().exportToPrismExplicitTra(getExportProductTransFilename());
+		}
+		if (getExportProductStates()) {
+			mainLog.println("\nExporting product state space to file \"" + getExportProductStatesFilename() + "\"...");
+			PrismFileLog out = new PrismFileLog(getExportProductStatesFilename());
+			VarList newVarList = (VarList) modulesFile.createVarList().clone();
+			String daVar = "_da";
+			while (newVarList.getIndex(daVar) != -1) {
+				daVar = "_" + daVar;
+			}
+			newVarList.addVar(0, new Declaration(daVar, new DeclarationIntUnbounded()), 1, null);
+			product.getProductModel().exportStates(Prism.EXPORT_PLAIN, newVarList, out);
+			out.close();
+		}
+		
 		// Find accepting states + compute reachability probabilities
 		BitSet acc;
 		if (product.getAcceptance() instanceof AcceptanceReach) {

prism/src/explicit/ModelExplicit.java

@@ -153,6 +153,7 @@ public abstract class ModelExplicit implements Model
 	 */
 	public void setStatesList(List<State> statesList)
 	{
+		new Exception().printStackTrace();
 		this.statesList = statesList;
 	}
 

prism/src/explicit/StateModelChecker.java

@@ -86,6 +86,12 @@ public class StateModelChecker extends PrismComponent
 
 	// Additional flags/settings not included in PrismSettings
 
+	// Export product model info?
+	protected boolean exportProductTrans = false;
+	protected String exportProductTransFilename = null;
+	protected boolean exportProductStates = false;
+	protected String exportProductStatesFilename = null;
+	
 	// Store the final results vector after model checking?
 	protected boolean storeVector = false;
 
@@ -196,6 +202,26 @@ public class StateModelChecker extends PrismComponent
 		this.verbosity = verbosity;
 	}
 
+	public void setExportProductTrans(boolean b) throws PrismException
+	{
+		exportProductTrans = b;
+	}
+
+	public void setExportProductTransFilename(String s) throws PrismException
+	{
+		exportProductTransFilename = s;
+	}
+
+	public void setExportProductStates(boolean b) throws PrismException
+	{
+		exportProductStates = b;
+	}
+
+	public void setExportProductStatesFilename(String s) throws PrismException
+	{
+		exportProductStatesFilename = s;
+	}
+
 	/**
 	 * Specify whether or not to store the final results vector after model checking.
 	 */
@@ -227,6 +253,26 @@ public class StateModelChecker extends PrismComponent
 		return verbosity;
 	}
 
+	public boolean getExportProductTrans()
+	{
+		return exportProductTrans;
+	}
+
+	public String getExportProductTransFilename()
+	{
+		return exportProductTransFilename;
+	}
+
+	public boolean getExportProductStates()
+	{
+		return exportProductStates;
+	}
+
+	public String getExportProductStatesFilename()
+	{
+		return exportProductStatesFilename;
+	}
+
 	/**
 	 * Whether or not to store the final results vector after model checking.
 	 */

prism/src/prism/Prism.java

@@ -3571,6 +3571,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType, this);
 		mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
 		// Pass any additional local settings
+		mc.setExportProductTrans(exportProductTrans);
+		mc.setExportProductTransFilename(exportProductTransFilename);
+		mc.setExportProductStates(exportProductStates);
+		mc.setExportProductStatesFilename(exportProductStatesFilename);
 		mc.setStoreVector(storeVector);
 		mc.setGenStrat(genStrat);
 		mc.setDoBisim(doBisim);