Bug fix for explicit engine model import - we should not assume that the initial state is 0. This also highlights a bug that ModelExplicit should store initial states as a state, not a list, but that issue is not fixed here.

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

prism/src/explicit/CTMCModelChecker.java

@@ -933,7 +933,8 @@ public class CTMCModelChecker extends ProbModelChecker
 			mc = new CTMCModelChecker(null);
 			ctmc = new CTMCSimple();
 			ctmc.buildFromPrismExplicit(args[0]);
-			//System.out.println(dtmc);
+			ctmc.addInitialState(0);
+			//System.out.println(ctmc);
 			labels = mc.loadLabelsFile(args[1]);
 			//System.out.println(labels);
 			target = labels.get(args[2]);

prism/src/explicit/DTMCModelChecker.java

@@ -1622,6 +1622,7 @@ public class DTMCModelChecker extends ProbModelChecker
 				mc = new DTMCModelChecker(null);
 				dtmc = new DTMCSimple();
 				dtmc.buildFromPrismExplicit(args[0]);
+				dtmc.addInitialState(0);
 				//System.out.println(dtmc);
 				Map<String, BitSet> labels = mc.loadLabelsFile(args[1]);
 				//System.out.println(labels);

prism/src/explicit/DTMCSimple.java

@@ -172,8 +172,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple
 		} 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/MDPSimple.java

@@ -370,8 +370,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 		} 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/ModelExplicit.java

@@ -163,6 +163,8 @@ public abstract class ModelExplicit implements 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/PrismSTPGAbstractRefine.java

@@ -95,6 +95,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 			throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 		}
 		modelConcrete.buildFromPrismExplicit(traFile);
+		modelConcrete.addInitialState(0);
 		if (buildEmbeddedDtmc) {
 			// TODO: do more efficiently (straight from tra file?)
 			mainLog.println("Concrete " + "CTMC" + ": " + modelConcrete.infoString());