explicit model import: some more minor fixes to set correct initial states

Followup to SVN 11744.


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

prism/src/explicit/CTMDPModelChecker.java

@@ -284,6 +284,7 @@ public class CTMDPModelChecker extends ProbModelChecker
 			mc = new CTMDPModelChecker(null);
 			ctmdp = new CTMDPSimple();
 			ctmdp.buildFromPrismExplicit(args[0]);
+			ctmdp.addInitialState(0);
 			System.out.println(ctmdp);
 			labels = mc.loadLabelsFile(args[1]);
 			System.out.println(labels);

prism/src/explicit/MDPModelChecker.java

@@ -1754,6 +1754,7 @@ public class MDPModelChecker extends ProbModelChecker
 			mc = new MDPModelChecker(null);
 			mdp = new MDPSimple();
 			mdp.buildFromPrismExplicit(args[0]);
+			mdp.addInitialState(0);
 			//System.out.println(mdp);
 			labels = mc.loadLabelsFile(args[1]);
 			//System.out.println(labels);

prism/src/explicit/ModelSimple.java

@@ -44,6 +44,8 @@ public interface ModelSimple extends Model
 
 	/**
 	 * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file).
+	 * Note that initial states are not configured (since this info is not in the file),
+	 * so this needs to be done separately (using {@link #addInitialState(int)}.
 	 */
 	public abstract void buildFromPrismExplicit(String filename) throws PrismException;
 

prism/src/explicit/PrismExplicit.java

@@ -464,6 +464,7 @@ public class PrismExplicit extends PrismComponent
 			prism.exportLabelsToFile(null, Prism.EXPORT_PLAIN, new File("tmp.lab"));
 			DTMCSimple modelExplicit = new DTMCSimple();
 			modelExplicit.buildFromPrismExplicit("tmp.tra");
+			modelExplicit.addInitialState(0);
 			PrismExplicit pe = new PrismExplicit(prism.getMainLog(), prism.getSettings());
 			pe.modelCheck(modelExplicit, null, propertiesFile, propertiesFile.getProperty(0));
 		} catch (PrismException e) {

prism/src/explicit/STPGAbstrSimple.java

@@ -227,8 +227,6 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
 		} catch (NumberFormatException e) {
 			throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + getModelType());
 		}
-		// Set initial state (assume 0)
-		initialStates.add(0);
 	}
 
 	// Mutators (other)

prism/src/explicit/STPGModelChecker.java

@@ -918,6 +918,7 @@ public class STPGModelChecker extends ProbModelChecker
 			mc = new STPGModelChecker(null);
 			stpg = new STPGAbstrSimple();
 			stpg.buildFromPrismExplicit(args[0]);
+			stpg.addInitialState(0);
 			//System.out.println(stpg);
 			labels = mc.loadLabelsFile(args[1]);
 			//System.out.println(labels);