Initial states for explicit model import can (should) be specified with importlabels.

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

prism/src/prism/Explicit2MTBDD.java

@@ -48,6 +48,7 @@ public class Explicit2MTBDD
 	// files to read in from
 	private File statesFile;
 	private File transFile;
+	private File labelsFile;
 
 	// initial state info
 	private String initString;
@@ -108,13 +109,14 @@ public class Explicit2MTBDD
 
 	// constructor
 	
-	public Explicit2MTBDD(Prism prism, File sf, File tf, int t, String is)
+	public Explicit2MTBDD(Prism prism, File sf, File tf, File lf, int t, String is)
 	{
 		this.prism = prism;
 		mainLog = prism.getMainLog();
 		techLog = prism.getTechLog();
 		statesFile = sf;
 		transFile = tf;
+		labelsFile = lf;
 		// set type at this point
 		// if no preference stated, assume default of mdp
 		switch (t) {
@@ -437,11 +439,7 @@ public class Explicit2MTBDD
 // 		JDD.Deref(tmp);
 		
 		// calculate dd for initial state
-		start = JDD.Constant(1);
-		for (i = 0; i < numVars; i++) {
-			tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1);
-			start = JDD.And(start, tmp);
-		}
+		buildInit();
 				
 		// compute state rewards
 		computeStateRewards();
@@ -822,7 +820,84 @@ public class Explicit2MTBDD
 			throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of transition matrix file \"" + transFile + "\"");
 		}
 	}
-
+	
+	// calculate dd for initial state
+	
+	private void buildInit() throws PrismException
+	{
+		BufferedReader in;
+		String s, s1, s2, ss[];
+		int i, r, lineNum = 0, count = 0;
+		JDDNode tmp;
+		
+		// If no labels file provided, just use state 0 (i.e. min value for each var) 
+		if (labelsFile == null) {
+			start = JDD.Constant(1);
+			for (i = 0; i < numVars; i++) {
+				tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], 0, 1);
+				start = JDD.And(start, tmp);
+			}
+		}
+		// Otherwise, construct from labels file 
+		else {
+			start = JDD.Constant(0);
+			try {
+				// open file for reading
+				in = new BufferedReader(new FileReader(labelsFile));
+				// read first line (label names) and ignore
+				in.readLine(); lineNum = 1;
+				// read remaining lines
+				s = in.readLine(); lineNum++;
+				numStates = 0;
+				while (s != null) {
+					// split string
+					s = s.trim();
+					ss = s.split(":");
+					s1 = ss[0].trim();
+					s2 = ss[1].trim();
+					// search right hand part for 0 (which is index of "init" label)
+					ss = s2.split(" ");
+					for (i = 0; i < ss.length; i++) {
+						if (ss[i].trim().equals("0")) {
+							count++;
+							r = Integer.parseInt(s1);
+							System.out.println("XXX" + r);
+							// set element in init states bdd
+							// case where we don't have a state list...
+							if (statesFile == null) {
+								tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[0], r, 1);
+							}
+							// case where we do have a state list...
+							else {
+								tmp = JDD.Constant(1);
+								for (i = 0; i < numVars; i++) {
+									tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], statesArray[r][i], 1));
+								}
+							}
+							// add it into bdd
+							JDD.Ref(tmp);
+							start = JDD.Or(start, tmp);
+							JDD.Deref(tmp);
+						}
+					}
+					// read next line
+					s = in.readLine(); lineNum++;
+				}
+				// close file
+				in.close();
+			}
+			catch (IOException e) {
+				throw new PrismException("File I/O error reading from \"" + statesFile + "\"");
+			}
+			catch (NumberFormatException e) {
+				throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\"");
+			}
+			if (count < 1) {
+				throw new PrismException("No initial states found in labels file");
+			}
+		}
+	}
+	
 	// read info about state rewards from states file
 	
 	public void computeStateRewards() throws PrismException

prism/src/prism/Prism.java

@@ -859,15 +859,28 @@ public class Prism implements PrismSettingsListener
 		return model;
 	}
 	
-	public ModulesFile parseExplicitModel(File statesFile, File transFile, int typeOverride, String initString) throws PrismException
+	/**
+	 * Builds a model from files containing an explicit list of transitions/etc.
+	 * This is step 1 of the process; buildExplicitModel(...) should be called subsequently.
+	 * @param statesFile File containing the list of states (optional, can be null)
+	 * @param transFile File containing the list of transitions (required)
+	 * @param typeOverride Type of model to be built (see ModulesFile) (optional, use 0 if not required)
+	 * @param initString Specification of initial state (optional, can be null)
+	 * @throws PrismException
+	 */
+	public ModulesFile parseExplicitModel(File statesFile, File transFile, File labelsFile, int typeOverride, String initString) throws PrismException
 	{
 		// create Explicit2MTBDD object
-		exp2mtbdd = new Explicit2MTBDD(this, statesFile, transFile, typeOverride, initString);
+		exp2mtbdd = new Explicit2MTBDD(this, statesFile, transFile, labelsFile, typeOverride, initString);
 		
 		// build state space
 		return exp2mtbdd.buildStates();
 	}
 	
+	/**
+	 * Builds a model from files containing an explicit list of transitions/etc.
+	 * This is step 2 of the process; parseExplicitModel(...) should have been called first.
+	 */
 	public Model buildExplicitModel() throws PrismException
 	{
 		long l; // timer

prism/src/prism/PrismCL.java

@@ -41,6 +41,7 @@ public class PrismCL
 	private boolean importpepa = false;
 	private boolean importtrans = false;
 	private boolean importstates = false;
+	private boolean importlabels = false;
 	private boolean steadystate = false;
 	private boolean dotransient = false;
 	private boolean exporttrans = false;
@@ -77,6 +78,7 @@ public class PrismCL
 	private String techLogFilename = "stdout";
 	private String modelFilename = null;
 	private String importStatesFilename = null;
+	private String importLabelsFilename = null;
 	private String propertiesFilename = null;
 	private String exportTransFilename = null;
 	private String exportStateRewardsFilename = null;
@@ -415,6 +417,7 @@ public class PrismCL
 	private void doParsing() throws PrismException
 	{
 		int i;
+		File sf = null, lf = null; 
 		
 		// parse model
 		
@@ -431,13 +434,17 @@ public class PrismCL
 				case ModulesFile.STOCHASTIC: mainLog.print("CTMC"); break;
 				default: mainLog.print("MDP"); break;
 				}
+				mainLog.print(") from \"" + modelFilename + "\"");
 				if (importstates) {
-					mainLog.print(") from files \"" + importStatesFilename + "\" and \"" + modelFilename + "\"...\n");
-					modulesFile = prism.parseExplicitModel(new File(importStatesFilename), new File(modelFilename), typeOverride, importInitString);
-				} else {
-					mainLog.print(") from file \"" + modelFilename + "\"...\n");
-					modulesFile = prism.parseExplicitModel(null, new File(modelFilename), typeOverride, importInitString);
+					mainLog.print(", \"" + importStatesFilename + "\"");
+					sf = new File(importStatesFilename);
 				}
+				if (importlabels) {
+					mainLog.print(", \"" + importLabelsFilename + "\"");
+					lf = new File(importLabelsFilename);
+				}
+				mainLog.println("...");
+				modulesFile = prism.parseExplicitModel(sf, new File(modelFilename), lf, typeOverride, importInitString);
 			}
 			else {
 				mainLog.print("\nParsing model file \"" + modelFilename + "\"...\n");
@@ -937,6 +944,16 @@ public class PrismCL
 						errorAndExit("No file specified for -"+sw+" switch");
 					}
 				}
+				// import labels for explicit model import
+				else if (sw.equals("importlabels")) {
+					if (i < args.length-1) {
+						importlabels = true;
+						importLabelsFilename = args[++i];
+					}
+					else {
+						errorAndExit("No file specified for -"+sw+" switch");
+					}
+				}
 				// import initial states info for explicit model import
 				else if (sw.equals("importinit")) {
 					if (i < args.length-1) {
@@ -1475,6 +1492,7 @@ public class PrismCL
 		mainLog.println("-importpepa .................... Model description is in PEPA, not the PRISM language");
 		mainLog.println("-importtrans <file> ............ Import the transition matrix directly from a text file");
 		mainLog.println("-importstates <file>............ Import the list of states directly from a text file");
+		mainLog.println("-importlabels <file>............ Import the list of labels directly from a text file");
 		mainLog.println("-importinit <expr>.............. Specify the initial state for explicitly imported models");
 		mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC");
 		mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC");