General tidy up of initial state handling in simulator, including a few GUI bug fixes. GUI default is to use the default initial state. For generation of simulation paths, there is a separate menu item to start from a specified state (and no option to switch asking on/off). Additional tidying and documentation in related parts of code too.

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

prism/src/explicit/ConstructModel.java

@@ -43,7 +43,6 @@ public class ConstructModel
 	// Basic info needed about model
 	private ModulesFile modulesFile;
 	private ModelType modelType;
-	private Values initialState;
 
 	public ConstructModel(SimulatorEngine engine, PrismLog mainLog)
 	{
@@ -51,11 +50,10 @@ public class ConstructModel
 		this.mainLog = mainLog;
 	}
 
-	public Model construct(ModulesFile modulesFile, Values initialState) throws PrismException
+	public Model construct(ModulesFile modulesFile) throws PrismException
 	{
 		this.modulesFile = modulesFile;
 		modelType = modulesFile.getModelType();
-		this.initialState = initialState;
 
 		IndexedSet<State> states;
 		LinkedList<State> explore;
@@ -106,7 +104,10 @@ public class ConstructModel
 		states = new IndexedSet<State>(true);
 		explore = new LinkedList<State>();
 		// Add initial state to lists/model
-		state = new State(modulesFile.getInitialValues());
+		if (modulesFile.getInitialStates() != null) {
+			throw new PrismException("Explicit model construction does not support multiple initial states");
+		}
+		state = modulesFile.getDefaultInitialState();
 		states.add(state);
 		explore.add(state);
 		model.addState();
@@ -240,7 +241,7 @@ public class ConstructModel
 				undefinedConstants.defineUsingConstSwitch(args[2]);
 			modulesFile.setUndefinedConstants(undefinedConstants.getMFConstantValues());
 			ConstructModel constructModel = new ConstructModel(prism.getSimulator(), mainLog);
-			Model model = constructModel.construct(modulesFile, modulesFile.getInitialValues());
+			Model model = constructModel.construct(modulesFile);
 			model.exportToPrismExplicitTra(args[1]);
 		} catch (FileNotFoundException e) {
 			System.out.println("Error: " + e.getMessage());

prism/src/parser/State.java

@@ -75,16 +75,32 @@ public class State implements Comparable<State>
 
 	/**
 	 * Construct by copying existing Values object.
+	 * Need access to a ModulesFile in case variables are not ordered correctly.
+	 * Throws an exception if any variables are undefined. 
 	 * @param v Values object to copy.
+	 * @param mf Corresponding ModulesFile (for variable info/ordering)
 	 */
-	//FIXME:don't assume v has correct order  
-	public State(Values v) throws PrismLangException
+	public State(Values v, ModulesFile mf) throws PrismLangException
 	{
-		int i, n;
+		int i, j, n;
 		n = v.getNumValues();
+		if (n != mf.getNumVars()) {
+			throw new PrismLangException("Wrong number of variables in state");
+		}
 		varValues = new Object[n];
-		for (i = 0; i < n; i++)
+		for (i = 0; i < n; i++) {
+			varValues[i] = null;
+		}
+		for (i = 0; i < n; i++) {
+			j = mf.getVarIndex(v.getName(i));
+			if (j == -1) {
+				throw new PrismLangException("Unknown variable " + v.getName(i) + " in state");
+			}
+			if (varValues[i] != null) {
+				throw new PrismLangException("Duplicated variable " + v.getName(i) + " in state");
+			}
 			varValues[i] = v.getValue(i);
+		}
 	}
 
 	/**

prism/src/parser/Values.java

@@ -30,6 +30,7 @@ import java.util.*;
 import java.text.*;
 
 import parser.type.*;
+import parser.ast.ModulesFile;
 import prism.PrismLangException;
 
 // class to store a list of typed constant/variable values
@@ -60,6 +61,22 @@ public class Values //implements Comparable
 		values = (ArrayList<Object>)v.values.clone();
 	}
 	
+	/**
+	 * Construct a new Values object  by copying existing State object.
+	 * Need access to a ModulesFile for variable names.
+	 * @param s State object to copy.
+	 * @param mf Corresponding ModulesFile (for variable info/ordering)
+	 */
+	public Values(State s, ModulesFile mf)
+	{
+		this();
+		int i, n;
+		n = s.varValues.length;
+		for (i = 0; i < n; i++) {
+			addValue(mf.getVarName(i), s.varValues[i]);
+		}
+	}
+	
 	// add value (type of value detetmined by type of Object)
 	// (note: no checking for duplication/inconsistencies/etc.)
 	

prism/src/parser/ast/ModulesFile.java

@@ -298,6 +298,12 @@ public class ModulesFile extends ASTElement
 		return getRewardStruct(0);
 	}
 
+	/**
+	 * Get the expression used in init...endinit to define the initial states of the model.
+	 * This is null if absent, i.e. the model has a single initial state defined by the
+	 * initial values for each individual variable.  
+	 * If non-null, we have to assume that there may be multiple initial states. 
+	 */
 	public Expression getInitialStates()
 	{
 		return initStates;
@@ -721,8 +727,52 @@ public class ModulesFile extends ASTElement
 		return constantValues;
 	}
 
-	// create a Values object to represent (a unique) initial state
+	/**
+	 * Create a State object representing the default initial state of this model.
+	 * If there are potentially multiple initial states (because the model has an 
+	 * init...endinit specification), this method returns null;
+	 * Assumes that values for constants have been provided for the model.
+	 * Note: This method replaces the old getInitialValues() method,
+	 * since State objects are now preferred to Values objects for efficiency.
+	 */
+	public State getDefaultInitialState() throws PrismLangException
+	{
+		int i, j, count, n, n2;
+		Module module;
+		Declaration decl;
+		State initialState;
+
+		if (initStates != null) {
+			return null;
+		}
 
+		// Create State object
+		initialState = new State(getNumVars());
+		// Then add values for all globals and all locals, in that order
+		count = 0;
+		n = getNumGlobals();
+		for (i = 0; i < n; i++) {
+			decl = getGlobal(i);
+			initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues, null));
+		}
+		n = getNumModules();
+		for (i = 0; i < n; i++) {
+			module = getModule(i);
+			n2 = module.getNumDeclarations();
+			for (j = 0; j < n2; j++) {
+				decl = module.getDeclaration(j);
+				initialState.setValue(count++, decl.getStartOrDefault().evaluate(constantValues, null));
+			}
+		}
+
+		return initialState;
+	}
+
+	/**
+	 * Create a Values object representing the default initial state of this model.
+	 * Deprecated: Use getDefaultInitialState() instead
+	 * (or new Values(getDefaultInitialState(), modulesFile)).
+	 */
 	public Values getInitialValues() throws PrismLangException
 	{
 		int i, j, n, n2;
@@ -792,7 +842,7 @@ public class ModulesFile extends ASTElement
 
 	/**
 	 * Create a VarList object storing information about all variables in this model.
-	 * Assumes that values for constants have been provided for the model,.
+	 * Assumes that values for constants have been provided for the model.
 	 * Also performs various syntactic checks on the variables.   
 	 */
 	public VarList createVarList() throws PrismLangException

prism/src/prism/Prism.java

@@ -1471,17 +1471,30 @@ public class Prism implements PrismSettingsListener
 		return res;
 	}
 	
-	// check if a property is suitable for analysis with the simulator
-	
+	/**
+	 * Check if a property is suitable for analysis with the simulator.
+	 * If not, an explanatory exception is thrown.
+	 * @param expr The property to check.
+	 */
 	public void checkPropertyForSimulation(Expression expr) throws PrismException
 	{
 		getSimulator().checkPropertyForSimulation(expr);
 	}
 	
-	// model check using simulator
-	// returns result or throws an exception in case of error
-	
-	public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, Values initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException
+	/**
+	 * Perform approximate model checking of a property on a model, using the simulator.
+	 * Sampling starts from the initial state provided or, if null, the default
+	 * initial state is used, selecting randomly (each time) if there are more than one.
+	 * Returns a Result object, except in case of error, where an Exception is thrown.
+	 * Note: All constants in the model/property files must have already been defined.
+	 * @param modulesFile Model for simulation, constants defined
+	 * @param propertiesFile Properties file containing property to check, constants defined
+	 * @param expr The property to check
+	 * @param initialState Initial state (if null, use default, selecting randomly if needed)
+	 * @param maxPathLength The maximum path length for sampling
+	 * @param simMethod Object specifying details of method to use for simulation
+	 */
+	public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression expr, State initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException
 	{
 		Object res = null;
 		
@@ -1489,16 +1502,26 @@ public class Prism implements PrismSettingsListener
 		expr.checkValid(modulesFile.getModelType());
 		
 		// Do model checking
-		res = getSimulator().modelCheckSingleProperty(modulesFile, propertiesFile, expr, new State(initialState), maxPathLength, simMethod);
+		res = getSimulator().modelCheckSingleProperty(modulesFile, propertiesFile, expr, initialState, maxPathLength, simMethod);
 		
 		return new Result(res);
 	}
 	
-	// model check using simulator (several properties simultaneously)
-	// returns an array of results, some of which may be Exception objects if there were errors
-	// in the case of an error which affects all properties, an exception is thrown
-	
-	public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, List<Expression> exprs, Values initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException
+	/**
+	 * Perform approximate model checking of several properties (simultaneously) on a model, using the simulator.
+	 * Sampling starts from the initial state provided or, if null, the default
+	 * initial state is used, selecting randomly (each time) if there are more than one.
+	 * Returns an array of results, some of which may be Exception objects if there were errors.
+	 * In the case of an error which affects all properties, an exception is thrown.
+	 * Note: All constants in the model/property files must have already been defined.
+	 * @param modulesFile Model for simulation, constants defined
+	 * @param propertiesFile Properties file containing properties to check, constants defined
+	 * @param exprs The properties to check
+	 * @param initialState Initial state (if null, use default, selecting randomly if needed)
+	 * @param maxPathLength The maximum path length for sampling
+	 * @param simMethod Object specifying details of method to use for simulation
+	 */
+	public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, List<Expression> exprs, State initialState, int maxPathLength, SimulationMethod simMethod) throws PrismException
 	{
 		Object[] res = null;
 		
@@ -1507,33 +1530,50 @@ public class Prism implements PrismSettingsListener
 			expr.checkValid(modulesFile.getModelType());
 		
 		// Do model checking
-		res = getSimulator().modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, new State(initialState), maxPathLength, simMethod);
+		res = getSimulator().modelCheckMultipleProperties(modulesFile, propertiesFile, exprs, initialState, maxPathLength, simMethod);
 		
 		Result[] resArray = new Result[res.length];
 		for (int i = 0; i < res.length; i++) resArray[i] = new Result(res[i]);
 		return resArray;
 	}
 	
-	// model check using simulator (ranging over some constants - from properties file only)
-	// results are stored in the ResultsCollection, some of which may be Exception objects if there were errors
-	// in the case of an error which affects all properties, an exception is thrown
-	
-	public void modelCheckSimulatorExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, ResultsCollection results, Expression propertyToCheck, Values initialState, int pathLength, SimulationMethod simMethod) throws PrismException, InterruptedException
+	/**
+	 * Perform an approximate model checking experiment on a model, using the simulator.
+	 * Perform an approximate model checking experiment on a model, using the simulator
+	 * (specified by values for undefined constants from the property only).
+	 * Sampling starts from the initial state provided or, if null, the default
+	 * initial state is used, selecting randomly (each time) if there are more than one.
+	 * Results are stored in the ResultsCollection object passed in,
+	 * some of which may be Exception objects if there were errors.
+	 * In the case of an error which affects all properties, an exception is thrown.
+	 * Note: All constants in the model file must have already been defined.
+	 * @param modulesFile Model for simulation, constants defined
+	 * @param propertiesFile Properties file containing property to check, constants defined
+	 * @param undefinedConstants Details of constant ranges defining the experiment
+	 * @param resultsCollection Where to store the results
+	 * @param expr The property to check
+	 * @param initialState Initial state (if null, is selected randomly)
+	 * @param maxPathLength The maximum path length for sampling
+	 * @param simMethod Object specifying details of method to use for simulation
+	 * @throws PrismException if something goes wrong with the sampling algorithm
+	 * @throws InterruptedException if the thread is interrupted
+	 */
+	public void modelCheckSimulatorExperiment(ModulesFile modulesFile, PropertiesFile propertiesFile, UndefinedConstants undefinedConstants, ResultsCollection results, Expression propertyToCheck, State initialState, int pathLength, SimulationMethod simMethod) throws PrismException, InterruptedException
 	{
-		getSimulator().modelCheckExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, new State(initialState), pathLength, simMethod);
+		getSimulator().modelCheckExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, pathLength, simMethod);
 	}
 	
 	/**
 	 * Generate a random path through the model using the simulator.
 	 * @param modulesFile The model
-	 * @param initialState Initial state (if null, is selected randomly)
 	 * @param details Information about the path to be generated
+	 * @param maxPathLength The maximum length of path to generate
 	 * @param file File to output the path to (stdout if null)
 	 */
 	public void generateSimulationPath(ModulesFile modulesFile, String details, int maxPathLength, File file) throws PrismException, PrismLangException
 	{
 		GenerateSimulationPath genPath = new GenerateSimulationPath(getSimulator(), mainLog);
-		genPath.generateSimulationPath(modulesFile, modulesFile.getInitialValues(), details, maxPathLength, file);
+		genPath.generateSimulationPath(modulesFile, null, details, maxPathLength, file);
 	}
 	
 	/**

prism/src/prism/PrismCL.java

@@ -326,8 +326,8 @@ public class PrismCL
 								mainLog.println("Model constants: " + definedMFConstants);
 						mainLog.println("Property constants: " + undefinedConstants.getPFDefinedConstantsString());
 						simMethod = processSimulationOptions(propertiesToCheck[j]);
-						prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results[j], propertiesToCheck[j], modulesFile
-								.getInitialValues(), simMaxPath, simMethod);
+						prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results[j], propertiesToCheck[j], null,
+								simMaxPath, simMethod);
 					} catch (PrismException e) {
 						// in case of (overall) error, report it, store as result for property, and proceed
 						error(e.getMessage());
@@ -390,8 +390,7 @@ public class PrismCL
 							// approximate (simulation-based) model checking
 							else {
 								simMethod = processSimulationOptions(propertiesToCheck[j]);
-								res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertiesToCheck[j],
-										modulesFileToCheck.getInitialValues(), simMaxPath, simMethod);
+								res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertiesToCheck[j], null, simMaxPath, simMethod);
 								simMethod.reset();
 							}
 						} catch (PrismException e) {
@@ -694,7 +693,7 @@ public class PrismCL
 			try {
 				explicit.ConstructModel constructModel = new explicit.ConstructModel(prism.getSimulator(), mainLog);
 				mainLog.println("\nConstructing model explicitly...");
-				explicit.Model modelExplicit = constructModel.construct(modulesFileToBuild, modulesFileToBuild.getInitialValues());
+				explicit.Model modelExplicit = constructModel.construct(modulesFileToBuild);
 				tmpFile = File.createTempFile("explicitbuildtest", ".tra").getAbsolutePath();
 				tmpFile = "explicitbuildtest.tra";
 				mainLog.println("\nExporting (explicit) model to \"" + tmpFile + "1\"...");
@@ -944,7 +943,6 @@ public class PrismCL
 					exit();
 				}
 
-
 				// property/properties given in command line
 				else if (sw.equals("pctl") || sw.equals("csl")) {
 					if (i < args.length - 1) {
@@ -1735,7 +1733,7 @@ public class PrismCL
 				else if (sw.equals("explicitbuildtest")) {
 					explicitbuildtest = true;
 				}
-				
+
 				// unknown switch - error
 				else {
 					errorAndExit("Invalid switch -" + sw + " (type \"prism -help\" for full list)");
@@ -1819,10 +1817,10 @@ public class PrismCL
 
 		// See if property to be checked is a reward (R) operator
 		boolean isReward = (expr instanceof ExpressionReward);
-		
+
 		// See if property to be checked is quantitative (=?)
 		boolean isQuant = Expression.isQuantitative(expr);
-		
+
 		// Pick defaults for simulation settings not set from command-line
 		if (!simApproxGiven)
 			simApprox = prism.getSettings().getDouble(PrismSettings.SIMULATOR_DEFAULT_APPROX);
@@ -1832,7 +1830,7 @@ public class PrismCL
 			simNumSamples = prism.getSettings().getInteger(PrismSettings.SIMULATOR_DEFAULT_NUM_SAMPLES);
 		if (!simWidthGiven)
 			simWidth = prism.getSettings().getDouble(PrismSettings.SIMULATOR_DEFAULT_WIDTH);
-		
+
 		if (!reqIterToConcludeGiven)
 			reqIterToConclude = prism.getSettings().getInteger(PrismSettings.SIMULATOR_DECIDE);
 		if (!simMaxRewardGiven)
@@ -1845,7 +1843,7 @@ public class PrismCL
 		if (simMethodName == null) {
 			simMethodName = isQuant ? "ci" : "sprt";
 		}
-		
+
 		// CI
 		if (simMethodName.equals("ci")) {
 			if (simWidthGiven && simConfidenceGiven && simNumSamplesGiven) {
@@ -1924,10 +1922,9 @@ public class PrismCL
 			if (simNumSamplesGiven) {
 				mainLog.println("\nWarning: Option -simsamples is not used for the SPRT method and is being ignored");
 			}
-		}
-		else
+		} else
 			throw new PrismException("Unknown simulation method \"" + simMethodName + "\"");
-			
+
 		return aSimMethod;
 	}
 
@@ -2065,7 +2062,7 @@ public class PrismCL
 		}
 		mainLog.println();
 	}
-	
+
 	// report (non-fatal) error
 
 	private void error(String s)

prism/src/prism/PrismSettings.java

@@ -107,7 +107,6 @@ public class PrismSettings implements Observer
 	public static final String SIMULATOR_MAX_REWARD					= "simulator.maxReward";
 	public static final	String SIMULATOR_SIMULTANEOUS				= "simulator.simultaneous";
 	public static final String SIMULATOR_FIELD_CHOICE				= "simulator.fieldChoice";
-	public static final	String SIMULATOR_NEW_PATH_ASK_INITIAL		= "simulator.newPathAskDefault";
 	public static final	String SIMULATOR_NEW_PATH_ASK_VIEW			= "simulator.newPathAskView";
 	public static final	String SIMULATOR_RENDER_ALL_VALUES			= "simulator.renderAllValues";
 	public static final String SIMULATOR_NETWORK_FILE				= "simulator.networkFile";
@@ -265,8 +264,6 @@ public class PrismSettings implements Observer
 																			"Check multiple properties simultaneously over the same set of execution paths (simulator only)." },
 			{ CHOICE_TYPE,		SIMULATOR_FIELD_CHOICE,					"Values used in dialog",				"2.1",		"Last used values",			"Last used values,Always use defaults",
 																			"How to choose values for the simulation dialog: remember previously used values or revert to the defaults each time." },
-			{ BOOLEAN_TYPE,		SIMULATOR_NEW_PATH_ASK_INITIAL,			"Ask for initial state",				"2.1",		new Boolean(true),			"",
-																			"Prompt for details of initial state when creating a new simulation path." },
 			{ BOOLEAN_TYPE,		SIMULATOR_NEW_PATH_ASK_VIEW,			"Ask for view configuration",			"2.1",		new Boolean(false),			"",
 																			"Display dialog with display options when creating a new simulation path." },
 			{ CHOICE_TYPE,		SIMULATOR_RENDER_ALL_VALUES,			"Path render style",					"3.2",		"Render all values",		"Render changes,Render all values",
@@ -307,7 +304,7 @@ public class PrismSettings implements Observer
 		}
 	};
 	
-	public static final String[] oldPropertyNames = {"simulator.apmcStrategy", "simulator.engine"};
+	public static final String[] oldPropertyNames = {"simulator.apmcStrategy", "simulator.engine", "simulator.newPathAskDefault"};
 	
 	public DefaultSettingOwner[] optionOwners;
 	private Hashtable<String,Setting> data;

prism/src/simulator/GenerateSimulationPath.java

@@ -46,7 +46,7 @@ public class GenerateSimulationPath
 
 	// Basic info needed for path
 	private ModulesFile modulesFile;
-	private Values initialState;
+	private State initialState;
 	private int maxPathLength;
 	private File file;
 	
@@ -72,7 +72,7 @@ public class GenerateSimulationPath
 	 * @param details Information about the path to be generated
 	 * @param file File to output the path to (stdout if null)
 	 */
-	public void generateSimulationPath(ModulesFile modulesFile, Values initialState, String details, int maxPathLength,
+	public void generateSimulationPath(ModulesFile modulesFile, State initialState, String details, int maxPathLength,
 			File file) throws PrismException
 	{
 		this.modulesFile = modulesFile;
@@ -221,7 +221,7 @@ public class GenerateSimulationPath
 		// generate path
 		engine.createNewPath(modulesFile);
 		for (j = 0; j < simPathRepeat; j++) {
-			engine.initialisePath(new State(initialState));
+			engine.initialisePath(initialState);
 			i = 0;
 			t = 0.0;
 			done = false;

prism/src/simulator/SimulatorEngine.java

@@ -190,7 +190,7 @@ public class SimulatorEngine
 
 	/**
 	 * Initialise (or re-initialise) the simulation path, starting with a specific (or random) initial state.
-	 * @param initialState Initial state (if null, is selected randomly)
+	 * @param initialState Initial state (if null, use default, selecting randomly if needed)
 	 */
 	public void initialisePath(State initialState) throws PrismException
 	{
@@ -198,9 +198,13 @@ public class SimulatorEngine
 		if (initialState != null) {
 			currentState.copy(initialState);
 		}
-		// Or pick a random one
+		// Or pick default/random one
 		else {
-			throw new PrismException("Random initial start state not yet supported");
+			if (modulesFile.getInitialStates() == null) {
+				currentState.copy(modulesFile.getDefaultInitialState());
+			} else {
+				throw new PrismException("Random choice of multiple initial states not yet supported");
+			}
 		}
 		updater.calculateStateRewards(currentState, tmpStateRewards);
 		// Initialise stored path
@@ -520,7 +524,7 @@ public class SimulatorEngine
 	public boolean queryIsInitial() throws PrismLangException
 	{
 		// Currently init...endinit is not supported so this is easy to check
-		return path.getCurrentState().equals(new State(modulesFile.getInitialValues()));
+		return path.getCurrentState().equals(modulesFile.getDefaultInitialState());
 	}
 
 	/**
@@ -531,7 +535,7 @@ public class SimulatorEngine
 	public boolean queryIsInitial(int step) throws PrismLangException
 	{
 		// Currently init...endinit is not supported so this is easy to check
-		return ((PathFull) path).getState(step).equals(new State(modulesFile.getInitialValues()));
+		return ((PathFull) path).getState(step).equals(modulesFile.getDefaultInitialState());
 	}
 
 	/**
@@ -1094,7 +1098,9 @@ public class SimulatorEngine
 
 	/**
 	 * Perform approximate model checking of a property on a model, using the simulator.
-	 * Sampling starts from the initial state provided or, if null, a random initial state each time.
+	 * Sampling starts from the initial state provided or, if null, the default
+	 * initial state is used, selecting randomly (each time) if there are more than one.
+	 * Returns a Result object, except in case of error, where an Exception is thrown.
 	 * Note: All constants in the model/property files must have already been defined.
 	 * @param modulesFile Model for simulation, constants defined
 	 * @param propertiesFile Properties file containing property to check, constants defined
@@ -1122,7 +1128,10 @@ public class SimulatorEngine
 
 	/**
 	 * Perform approximate model checking of properties on a model, using the simulator.
-	 * Sampling starts from the initial state provided or, if null, a random initial state each time.
+	 * Sampling starts from the initial state provided or, if null, the default
+	 * initial state is used, selecting randomly (each time) if there are more than one.
+	 * Returns an array of results, some of which may be Exception objects if there were errors.
+	 * In the case of an error which affects all properties, an exception is thrown.
 	 * Note: All constants in the model/property files must have already been defined.
 	 * @param modulesFile Model for simulation, constants defined
 	 * @param propertiesFile Properties file containing property to check, constants defined
@@ -1226,9 +1235,14 @@ public class SimulatorEngine
 	}
 
 	/**
-	 * Perform an approximate model checking experiment on a model, using the simulator.
-	 * Sampling starts from the initial state provided or, if null, a random initial state each time.
-	 * Note: All constants in the model/property files must have already been defined.
+	 * Perform an approximate model checking experiment on a model, using the simulator
+	 * (specified by values for undefined constants from the property only).
+	 * Sampling starts from the initial state provided or, if null, the default
+	 * initial state is used, selecting randomly (each time) if there are more than one.
+	 * Results are stored in the ResultsCollection object passed in,
+	 * some of which may be Exception objects if there were errors.
+	 * In the case of an error which affects all properties, an exception is thrown.
+	 * Note: All constants in the model file must have already been defined.
 	 * @param modulesFile Model for simulation, constants defined
 	 * @param propertiesFile Properties file containing property to check, constants defined
 	 * @param undefinedConstants Details of constant ranges defining the experiment

prism/src/userinterface/GUISimulationPicker.java

@@ -70,7 +70,7 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 	private JTable initValuesTable;
 	private DefineValuesTable initValuesModel;
 
-	// Last valid contents of tetx boxes
+	// Last valid contents of text boxes
 	private String lastWidth;
 	private String lastConf;
 	private String lastNumSamples;
@@ -79,6 +79,7 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 	private boolean atLeastOneQuant;
 
 	// Variables declaration - do not modify//GEN-BEGIN:variables
+	// Note: this code has now been modified manually; form is no longer used.
 	javax.swing.JTextField widthField;
 	javax.swing.JComboBox selectSimulationMethod;
 	javax.swing.JComboBox automaticCalculateCombo;
@@ -116,6 +117,7 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 	private javax.swing.JButton okayButton;
 	javax.swing.JTextField pathLengthField;
 	javax.swing.JPanel topPanel;
+	javax.swing.JCheckBox useDefaultInitialCheck;
 
 	// End of variables declaration//GEN-END:variables
 
@@ -176,16 +178,18 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 
 		// create "initial state" table
 		initValuesModel = new DefineValuesTable();
-		initValuesTable = new JTable();
+		initValuesTable = new GreyableJTable();
 		initValuesTable.setModel(initValuesModel);
 		initValuesTable.setSelectionMode(DefaultListSelectionModel.SINGLE_INTERVAL_SELECTION);
 		initValuesTable.setCellSelectionEnabled(true);
 
 		// set up simulation information based on previous info (or defaults - see above)
 		information = lastSimulationInformation;
-		// set initial state as passed in to constructor
-		information.setInitialState(modulesFile.getInitialValues());
 
+		// currently, we deliberately do not recall the last initial state used
+		// since it may no longer be valid due to changes in the model
+		information.setInitialState(null);
+		
 		// initialise
 		initComponents();
 		this.getRootPane().setDefaultButton(okayButton);
@@ -206,6 +210,7 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 	 * initialize the form.
 	 * WARNING: Do NOT modify this code. The content of this method is
 	 * always regenerated by the Form Editor.
+	 * Note: this code has now been modified manually; form is no longer used.
 	 */
 	private void initComponents()//GEN-BEGIN:initComponents
 	{
@@ -248,6 +253,7 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 		jPanel19 = new javax.swing.JPanel();
 		jPanel20 = new javax.swing.JPanel();
 		//distributedCheck = new javax.swing.JCheckBox();
+		useDefaultInitialCheck = new javax.swing.JCheckBox();
 
 		addWindowListener(new java.awt.event.WindowAdapter()
 		{
@@ -307,9 +313,22 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 		gridBagConstraints.gridx = 0;
 		gridBagConstraints.gridy = 4;
 		jPanel1.add(jPanel5, gridBagConstraints);
-
+		
+		useDefaultInitialCheck.setText("Use default initial state");
+		useDefaultInitialCheck.addActionListener(new java.awt.event.ActionListener()
+		{
+			public void actionPerformed(java.awt.event.ActionEvent evt)
+			{
+				useDefaultInitialCheckActionPerformed(evt);
+			}
+		});
+		gridBagConstraints = new java.awt.GridBagConstraints();
+		gridBagConstraints.gridx = 1;
+		gridBagConstraints.gridy = 1;
+		gridBagConstraints.fill = java.awt.GridBagConstraints.BOTH;
+		jPanel1.add(useDefaultInitialCheck, gridBagConstraints);
+		
 		topPanel.setLayout(new java.awt.BorderLayout());
-
 		gridBagConstraints = new java.awt.GridBagConstraints();
 		gridBagConstraints.gridx = 1;
 		gridBagConstraints.gridy = 3;
@@ -784,47 +803,34 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 		topPanel.setPreferredSize(new Dimension(300, 300));
 	}
 
+	/**
+	 * Populate dialog using 'information' field.
+	 */
 	private void initValues()
 	{
-
-		Value v;
+		// Use default initial state?
+		// (currently always the case on initialisation)
 		if (information.getInitialState() == null) {
-			/*
-			int n,i,j,n2;
-			Declaration decl;
-			Module module;
-			
-			// first add all globals
-			n = mf.getNumGlobals();
-			for (i = 0; i < n; i++)
-			{
-				decl = mf.getGlobal(i);
-				v = new Value(decl.getName(), decl.getType(), "");
-				initValuesModel.addValue(v);
+			// Tick box
+			useDefaultInitialCheck.setSelected(true);
+			// Put variable names in table, but no values
+			for (int i = 0; i < modulesFile.getNumVars(); i++) {
+				initValuesModel.addValue(new Value(modulesFile.getVarName(i), modulesFile.getVarType(i), null));
 			}
-			// then add all module variables
-			n = mf.getNumModules();
-			for (i = 0; i < n; i++)
-			{
-				module = mf.getModule(i);
-				n2 = module.getNumDeclarations();
-				for (j = 0; j < n2; j++)
-				{
-					decl = module.getDeclaration(j);
-					v = new Value(decl.getName(), decl.getType(), "");
-					initValuesModel.addValue(v);
-				}
-			}
-			*/
+			// Disable table
+			if (initValuesTable.getCellEditor() != null)
+			initValuesTable.getCellEditor().stopCellEditing();
+			initValuesTable.getSelectionModel().clearSelection();
 			initValuesTable.setEnabled(false);
 		} else {
-			for (int i = 0; i < information.getInitialState().getNumValues(); i++) {
-				try {
-					v = new Value(information.getInitialState().getName(i), information.getInitialState().getType(i), information.getInitialState().getValue(i));
-					initValuesModel.addValue(v);
-				} catch (Exception e) {
-				}
+			// Untick box
+			useDefaultInitialCheck.setSelected(false);
+			// Set up table (from information)
+			// Need to add to add some validity checks here if re-enabled
+			for (int i = 0; i < modulesFile.getNumVars(); i++) {
+				initValuesModel.addValue(new Value(modulesFile.getVarName(i), modulesFile.getVarType(i), information.getInitialState().getValue(i)));
 			}
+			initValuesTable.setEnabled(true);
 		}
 
 		// populate parameter text boxes
@@ -842,10 +848,6 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 		//distributedCheck.setSelected(information.isDistributed());
 	}
 
-	/** Call this static method to construct a new GUIValuesPicker to define
-	 *  initialState.  If you don't want any default values, then pass in null for
-	 *  initDefaults
-	 */
 	/**
 	 * Create a new GUIConstantsPicker dialog to define info for simulation-based property checking.
 	 * @param parent Parent GUI window
@@ -940,23 +942,72 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 			}
 			information.setMaxPathLength(maxPathLength);
 			// Store initial state
-			Values newInitState = new Values();
-			for (i = 0; i < initValuesModel.getNumValues(); i++) {
-				parameter = initValuesModel.getValue(i).name;
-				newInitState.addValue(initValuesModel.getValue(i).name, initValuesModel.getValue(i).value);
+			if (useDefaultInitialCheck.isSelected()) {
+				information.setInitialState(null);
+			} else {
+				Values newInitState = new Values();
+				for (i = 0; i < initValuesModel.getNumValues(); i++) {
+					parameter = initValuesModel.getValue(i).name;
+					Object parameterValue = null;
+					if (initValuesModel.getValue(i).type instanceof TypeBool) {
+						String bool = initValuesModel.getValue(i).value.toString();
+						if (!(bool.equals("true") || bool.equals("false")))
+							throw new NumberFormatException();
+						parameterValue = new Boolean(bool);
+					} else if (initValuesModel.getValue(i).type instanceof TypeInt) {
+						parameterValue = new Integer(initValuesModel.getValue(i).value.toString());
+					} else { 
+						throw new NumberFormatException();
+					}
+					newInitState.addValue(parameter, parameterValue);
+				}
+				information.setInitialState(newInitState);
 			}
-			information.setInitialState(newInitState);
-
+			
 			//information.setDistributed(distributedCheck.isSelected());
 			cancelled = false;
 			lastSimulationInformation = information;
 			dispose();
 		} catch (NumberFormatException e) {
-			gui.errorDialog("Invalid number value entered for parameter \"" + parameter + "\"");
+			gui.errorDialog("Invalid value entered for parameter \"" + parameter + "\"");
 		}
 
 	}//GEN-LAST:event_okayButtonActionPerformed
 
+	private void useDefaultInitialCheckActionPerformed(java.awt.event.ActionEvent evt)
+	{
+		// If ticking...
+		if (useDefaultInitialCheck.isSelected()) {
+			// Clear values in table
+			for (int i = 0; i < modulesFile.getNumVars(); i++) {
+				initValuesModel.getValue(i).value = null;
+			}
+			// Disable table
+			if (initValuesTable.getCellEditor() != null)
+			initValuesTable.getCellEditor().stopCellEditing();
+			initValuesTable.getSelectionModel().clearSelection();
+			initValuesTable.setEnabled(false);
+		}
+		// If unticking
+		else {
+			// Set up table (based on default initial state)
+			try {
+				State defaultInitialState = modulesFile.getDefaultInitialState();
+				if (defaultInitialState == null)
+					throw new PrismException("");
+				for (int i = 0; i < modulesFile.getNumVars(); i++) {
+					initValuesModel.getValue(i).value = defaultInitialState.varValues[i];
+				}
+			} catch (PrismException e) {
+				// In case of error, clear values
+				for (int i = 0; i < modulesFile.getNumVars(); i++) {
+					initValuesModel.getValue(i).value = null;
+				}
+			}
+			initValuesTable.setEnabled(true);
+		}
+	}
+	
 	private void cancelButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_cancelButtonActionPerformed
 	{//GEN-HEADEREND:event_cancelButtonActionPerformed
 		dispose();
@@ -1028,7 +1079,7 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 			case 1:
 				return v.type.getTypeString();
 			case 2:
-				return v.value.toString();
+				return v.value == null ? "" : v.value.toString();
 			default:
 				return "";
 			}
@@ -1095,7 +1146,28 @@ public class GUISimulationPicker extends javax.swing.JDialog implements KeyListe
 
 		public String toString()
 		{
-			return name + "=" + value.toString();
+			return name + "=" + value;
+		}
+	}
+
+	public class GreyableJTable extends JTable
+	{
+		private static final long serialVersionUID = 1L;
+		private TableCellRenderer tableCellRenderer = new TableCellRenderer()
+		{
+			private static final long serialVersionUID = 1L;
+
+			public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column)
+			{
+				Component c = GreyableJTable.super.getCellRenderer(row, column).getTableCellRendererComponent(table, value, isSelected, hasFocus, row, column);
+				c.setEnabled(table != null && table.isEnabled());
+				return c;
+			}
+		};
+
+		public TableCellRenderer getCellRenderer(int row, int column)
+		{
+			return tableCellRenderer;
 		}
 	}
 }

prism/src/userinterface/properties/GUIExperiment.java

@@ -35,7 +35,6 @@ import pta.DigitalClocks;
 
 import javax.swing.*;
 
-import simulator.method.APMCapproximation;
 import userinterface.*;
 import java.util.*;
 import userinterface.util.*;
@@ -261,7 +260,7 @@ public class GUIExperiment
 
 					// only do explicit model construction if necessary
 					if (!useSimulation && modulesFile.getModelType() != ModelType.PTA) {
-						
+
 						// build model
 						try {
 							logln("\n-------------------------------------------");
@@ -297,9 +296,9 @@ public class GUIExperiment
 					if (useSimulation && !reuseInfo) {
 						try {
 							info = null;
-							info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), propertyToCheck, modulesFile, "("+definedMFConstants+")");
-						}
-						catch (PrismException e) {
+							info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), propertyToCheck, modulesFile, "(" + definedMFConstants
+									+ ")");
+						} catch (PrismException e) {
 							// in case of error, report it (in log only), store as result, and go on to the next model
 							errorLog(e.getMessage());
 							try {
@@ -320,7 +319,7 @@ public class GUIExperiment
 						// if there are multiple models, offer the chance to reuse simulation info
 						if (undefinedConstants.getNumModelIterations() > 1 && !reuseInfoAsked) {
 							reuseInfoAsked = true;
-							int q = guiProp.questionYesNo("Do you want to reuse the same initial state and simulation\n"
+							int q = guiProp.questionYesNo("Do you want to reuse the same simulation\n"
 									+ "parameters for the remaining models in this experiment?\n" + "If not you will be prompted for new values for each one.");
 							if (q == 0)
 								reuseInfo = true;
@@ -358,8 +357,17 @@ public class GUIExperiment
 								if (definedMFConstants.getNumValues() > 0)
 									logln("Model constants: " + definedMFConstants);
 							logln("Property constants: " + undefinedConstants.getPFDefinedConstantsString());
-							prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, info
-									.getInitialState(), info.getMaxPathLength(), info.createSimulationMethod());
+							// convert initial Values -> State
+							// (remember: null means use default or pick randomly)
+							parser.State initialState;
+							if (info.getInitialState() == null) {
+								initialState = null;
+							} else {
+								initialState = new parser.State(info.getInitialState(), modulesFile);
+							}
+							// do simulation
+							prism.modelCheckSimulatorExperiment(modulesFile, propertiesFile, undefinedConstants, results, propertyToCheck, initialState, info
+									.getMaxPathLength(), info.createSimulationMethod());
 							// update progress meter
 							// (all properties simulated simultaneously so can't get more accurate feedback at the moment anyway)
 							table.progressChanged();
@@ -434,7 +442,17 @@ public class GUIExperiment
 								}
 								// approximate (simulation-based) model checking
 								else {
-									res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertyToCheck, info.getInitialState(), info.getMaxPathLength(), info.createSimulationMethod());
+									// convert initial Values -> State
+									// (remember: null means use default or pick randomly)
+									parser.State initialState;
+									if (info.getInitialState() == null) {
+										initialState = null;
+									} else {
+										initialState = new parser.State(info.getInitialState(), modulesFileToCheck);
+									}
+									// do simulation
+									res = prism.modelCheckSimulator(modulesFileToCheck, propertiesFile, propertyToCheck, initialState, info.getMaxPathLength(),
+											info.createSimulationMethod());
 								}
 							} catch (PrismException e) {
 								// in case of error, report it (in log only), store exception as the result and proceed

prism/src/userinterface/properties/computation/SimulateModelCheckThread.java

@@ -43,7 +43,7 @@ import userinterface.properties.*;
  *  This thread handles the calling of simulation-based
  *  model checking (sampling) with the given modules file (constants
  *  defined), properties file (constants defined), list of properties to
- *  be (approximately) verified and initial state.
+ *  be (approximately) verified and initial state (default/random if null).
  */
 public class SimulateModelCheckThread extends GUIComputationThread
 {
@@ -53,7 +53,6 @@ public class SimulateModelCheckThread extends GUIComputationThread
 	private ArrayList<GUIProperty> guiProps;
 	private Values definedMFConstants;
 	private Values definedPFConstants;
-	private Values initialState;
 	private int maxPathLength;
 	private SimulationInformation info;
 
@@ -69,7 +68,6 @@ public class SimulateModelCheckThread extends GUIComputationThread
 		this.definedMFConstants = definedMFConstants;
 		this.definedPFConstants = definedPFConstants;
 		this.info = info;
-		this.initialState = info.getInitialState();
 		this.maxPathLength = info.getMaxPathLength();
 	}
 
@@ -132,7 +130,14 @@ public class SimulateModelCheckThread extends GUIComputationThread
 				if (definedPFConstants != null)
 					if (definedPFConstants.getNumValues() > 0)
 						logln("Property constants: " + definedPFConstants);
-				
+				// convert initial Values -> State
+				// (remember: null means use default or pick randomly)
+				parser.State initialState;
+				if (info.getInitialState() == null) {
+					initialState = null;
+				} else {
+					initialState = new parser.State(info.getInitialState(), mf);
+				}
 				// do simulation
 				results = prism.modelCheckSimulatorSimultaneously(mf, pf, properties, initialState, maxPathLength, method);
 				method.reset();
@@ -180,6 +185,15 @@ public class SimulateModelCheckThread extends GUIComputationThread
 					if (definedPFConstants != null)
 						if (definedPFConstants.getNumValues() > 0)
 							logln("Property constants: " + definedPFConstants);
+					// convert initial Values -> State
+					// (remember: null means use default or pick randomly)
+					parser.State initialState;
+					if (info.getInitialState() == null) {
+						initialState = null;
+					} else {
+						initialState = new parser.State(info.getInitialState(), mf);
+					}
+					// do simulation
 					result = prism.modelCheckSimulator(mf, pf,  pf.getProperty(i), initialState, maxPathLength, method);
 					method.reset();
 				}

prism/src/userinterface/simulator/GUIInitialStatePicker.java

@@ -102,8 +102,8 @@ public class GUIInitialStatePicker extends javax.swing.JDialog implements KeyLis
 		setResizable(true);
 		setLocationRelativeTo(getParent()); // centre
 		
-		this.askOption = gui.getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL);
-		optionCheckBox.setSelected(this.askOption);
+		//this.askOption = gui.getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL);
+		//optionCheckBox.setSelected(this.askOption);
 	}
     
 	/** This method is called from within the constructor to
@@ -162,7 +162,7 @@ public class GUIInitialStatePicker extends javax.swing.JDialog implements KeyLis
             }
         });
 
-        bottomPanel.add(optionCheckBox, java.awt.BorderLayout.WEST);
+        //bottomPanel.add(optionCheckBox, java.awt.BorderLayout.WEST);
         optionCheckBox.getAccessibleContext().setAccessibleName("optionCheckBox");
 
         allPanel.add(bottomPanel, java.awt.BorderLayout.SOUTH);
@@ -265,48 +265,33 @@ public class GUIInitialStatePicker extends javax.swing.JDialog implements KeyLis
     
 	private void okayButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_okayButtonActionPerformed
 	{//GEN-HEADEREND:event_okayButtonActionPerformed
-		int i, n;
-		Value c;
-            
-		if (optionCheckBox.isSelected() != this.askOption)
-		{
-			this.askOption = !this.askOption;
-			try
-			{
-				gui.getPrism().getSettings().set(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL, this.askOption);
-			}
-			catch (PrismException e)
-			{
-			
-			}			
-		}
-            
-		if(initValuesTable.getCellEditor() != null)initValuesTable.getCellEditor().stopCellEditing();
-            
+		if(initValuesTable.getCellEditor() != null)
+			initValuesTable.getCellEditor().stopCellEditing();
             
 		String parameter = "";
-		try
-		{
-			
-                
+		try {
 			Values newInitState = new Values();
-                
-			//check each value of values
-			for(i = 0; i < initValuesModel.getNumValues(); i++)
-			{
+			// check each variable value
+			for (int i = 0; i < initValuesModel.getNumValues(); i++) {
 				parameter = initValuesModel.getValue(i).name;
-				newInitState.addValue(initValuesModel.getValue(i).name, initValuesModel.getValue(i).value);
+				Object parameterValue = null;
+				if (initValuesModel.getValue(i).type instanceof TypeBool) {
+					String bool = initValuesModel.getValue(i).value.toString();
+					if (!(bool.equals("true") || bool.equals("false")))
+						throw new NumberFormatException();
+					parameterValue = new Boolean(bool);
+				} else if (initValuesModel.getValue(i).type instanceof TypeInt) {
+					parameterValue = new Integer(initValuesModel.getValue(i).value.toString());
+				} else { 
+					throw new NumberFormatException();
+				}
+				newInitState.addValue(parameter, parameterValue);
 			}
 			initialState = newInitState;
-                
-			
 			cancelled = false;
-                
-			
 			dispose();
 		}
-		catch(NumberFormatException e)
-		{
+		catch(NumberFormatException e) {
 			gui.errorDialog("Invalid number value entered for "+parameter+" parameter");
 		}
 	}//GEN-LAST:event_okayButtonActionPerformed

prism/src/userinterface/simulator/GUISimulator.java

@@ -73,7 +73,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	private SimulationView view;
 
 	//Actions
-	private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, resetPath, exportPath, configureView;
+	private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, newPathFromState, resetPath, exportPath, configureView;
 
 	/** Creates a new instance of GUISimulator */
 	public GUISimulator(GUIPrism gui)
@@ -269,7 +269,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		}
 	}
 
-	public void a_newPath()
+	public void a_newPath(boolean chooseInitialState)
 	{
 		Values initialState;
 		try {
@@ -297,59 +297,58 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			parsedModel.setUndefinedConstants(lastConstants);
 			pf.setUndefinedConstants(lastPropertyConstants);
 
-			// now determine the initial state for simulation
-
-			// first select a default state (the initial state) which may or may not end up being used
-			Values defaultInitialState = new Values();
-			defaultInitialState.addValues(parsedModel.getInitialValues());
-
-			boolean modelChanged = false;
-
-			// we will pass in lastInitialState to the dialog
-			// but first make sure it is ok, i.e.
-			// (a) it is non-null
-			if (lastInitialState == null) {
-				lastInitialState = defaultInitialState;
-				modelChanged = true;
+			// check here for possibility of multiple initial states
+			// (not supported yet) to avoid problems below
+			if (parsedModel.getInitialStates() != null) {
+				throw new PrismException("The simulator does not not yet handle models with multiple states");
+			}
+			
+			// do we need to ask for an initial state for simulation?
+			// no: just use default/random
+			if (!chooseInitialState) {
+				initialState = null;
 			}
-			// (b) var names/types are correct
+			// yes: 
 			else {
-				boolean match = true;
-				int i, n;
-				n = defaultInitialState.getNumValues();
-				if (lastInitialState.getNumValues() != defaultInitialState.getNumValues()) {
-					match = false;
-				} else {
-					for (i = 0; i < n; i++) {
-						if (!lastInitialState.contains(defaultInitialState.getName(i))) {
-							match = false;
-							break;
-						} else {
-							int index = lastInitialState.getIndexOf(defaultInitialState.getName(i));
-							if (lastInitialState.getType(index) != defaultInitialState.getType(i)) {
+				// first, pick default values for chooser dialog
+				
+				// default initial state if none specified previously
+				if (lastInitialState == null) {
+					lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel);
+				}
+				// otherwise, check previously used state for validity
+				else {
+					boolean match = true;
+					int i, n;
+					n = parsedModel.getNumVars();
+					if (lastInitialState.getNumValues() != n) {
+						match = false;
+					} else {
+						for (i = 0; i < n; i++) {
+							if (!lastInitialState.contains(parsedModel.getVarName(i))) {
 								match = false;
 								break;
+							} else {
+								int index = lastInitialState.getIndexOf(parsedModel.getVarName(i));
+								if (!lastInitialState.getType(index).equals(parsedModel.getVarType(i))) {
+									match = false;
+									break;
+								}
 							}
 						}
 					}
+					// if there's a problem, just use the default
+					if (!match) {
+						lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel);
+					}
 				}
-				if (!match) // if there's a problem, just use the default
-				{
-					lastInitialState = defaultInitialState;
-					modelChanged = true;
-				}
-			}
-
-			// if required, we prompt the user for an initial state
-			if (isAskForInitialState()) {
+				
+				initialState = null;
 				initialState = GUIInitialStatePicker.defineInitalValuesWithDialog(getGUI(), lastInitialState, parsedModel);
-				// if user clicked cancel from dialog...
-
+				// if user clicked cancel from dialog, bail out
 				if (initialState == null) {
 					return;
 				}
-			} else {
-				initialState = lastInitialState;
 			}
 
 			tableScroll.setViewportView(pathTable);
@@ -359,8 +358,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			// Create a new path in the simulator and add labels/properties 
 			engine.createNewPath(parsedModel);
 			pathActive = true;
+			engine.initialisePath(initialState == null ? null : new parser.State(initialState, parsedModel));
 			repopulateFormulae(pf);
-			engine.initialisePath(new State(initialState));
 
 			totalTimeLabel.setText(formatDouble(engine.getTotalTimeForPath()));
 			pathLengthLabel.setText("" + engine.getPathSize());
@@ -812,6 +811,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	protected void doEnables()
 	{
 		newPath.setEnabled(parsedModel != null && !computing);
+		newPathFromState.setEnabled(parsedModel != null && !computing);
 		resetPath.setEnabled(pathActive && !computing);
 		exportPath.setEnabled(pathActive && !computing);
 		randomExploration.setEnabled(pathActive && !computing);
@@ -835,6 +835,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		//configureViewButton.setEnabled(pathActive && !computing);
 
 		//newPath.setEnabled(parsedModel != null && !computing);
+		//newPathFromState.setEnabled(parsedModel != null && !computing);
 		//newPathButton.setEnabled(parsedModel != null && !computing);
 
 		currentUpdatesTable.setEnabled(pathActive);
@@ -1419,7 +1420,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			public void actionPerformed(ActionEvent e)
 			{
 				GUISimulator.this.tabToFront();
-				a_newPath();
+				a_newPath(false);
 			}
 		};
 
@@ -1429,6 +1430,20 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		newPath.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStates.png"));
 		newPath.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_F8, 0));
 
+		newPathFromState = new AbstractAction()
+		{
+			public void actionPerformed(ActionEvent e)
+			{
+				GUISimulator.this.tabToFront();
+				a_newPath(true);
+			}
+		};
+
+		newPathFromState.putValue(Action.LONG_DESCRIPTION, "Creates a new path from a chosen state.");
+		//newPathFromState.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_N));
+		newPathFromState.putValue(Action.NAME, "New path from state");
+		newPathFromState.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStates.png"));
+
 		resetPath = new AbstractAction()
 		{
 			public void actionPerformed(ActionEvent e)
@@ -1525,6 +1540,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 		pathPopupMenu = new JPopupMenu();
 		pathPopupMenu.add(newPath);
+		pathPopupMenu.add(newPathFromState);
 		pathPopupMenu.add(resetPath);
 		pathPopupMenu.add(exportPath);
 		pathPopupMenu.addSeparator();
@@ -1537,6 +1553,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 		simulatorMenu = new JMenu("Simulator");
 		simulatorMenu.add(newPath);
+		simulatorMenu.add(newPathFromState);
 		simulatorMenu.add(resetPath);
 		simulatorMenu.add(exportPath);
 		simulatorMenu.addSeparator();
@@ -1635,7 +1652,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 	private void newPathButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_newPathButtonActionPerformed
 	{//GEN-HEADEREND:event_newPathButtonActionPerformed
-		a_newPath();
+		a_newPath(false);
 	}//GEN-LAST:event_newPathButtonActionPerformed
 
 	/**
@@ -1708,7 +1725,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		if (!computing) {
 			if (e.getClickCount() == 2 && e.getSource() == pathTablePlaceHolder) {
 				if (newPath.isEnabled())
-					a_newPath();
+					a_newPath(false);
 			}
 			if (e.isPopupTrigger()
 					&& (e.getSource() == pathTablePlaceHolder || e.getSource() == pathTable || e.getSource() == pathTable.getTableHeader() || e.getSource() == tableScroll)) {
@@ -1867,7 +1884,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	 */
 	public boolean isAskForInitialState()
 	{
-		return getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL);
+		return false; //getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL);
 	}
 
 	/**
@@ -1876,7 +1893,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	 */
 	public void setAskForInitialState(boolean askForInitialState) throws PrismException
 	{
-		getPrism().getSettings().set(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL, askForInitialState);
+		//getPrism().getSettings().set(PrismSettings.SIMULATOR_NEW_PATH_ASK_INITIAL, askForInitialState);
 	}
 
 	/**
@@ -3044,7 +3061,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 				// The step column
 				if (actionStart <= columnIndex && columnIndex < stepStart) {
-					return "Action label or module name";
+					return "Module name or [action] label";
 				} else if (stepStart <= columnIndex && columnIndex < cumulativeTimeStart) {
 					return "Index of state in path";
 				} else if (cumulativeTimeStart <= columnIndex && columnIndex < timeStart) {

prism/src/userinterface/simulator/GUISimulatorPathTable.java

@@ -282,7 +282,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 				{	
 					// unused:
 					stringValue = "?";
-					this.setToolTipText("Action label or module name for transition from state " + (row - 1) + " to " + (row) + " (not yet known)");
+					this.setToolTipText("Module name or [action] label for transition from state " + (row - 1) + " to " + (row) + " (not yet known)");
 				}
 				else
 				{
@@ -291,7 +291,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 					if (row == 0) {
 						tooltip = null;
 					} else {
-						tooltip = "Action label or module name for transition from state " + (row - 1) + " to " + (row);
+						tooltip = "Module name or [action] label for transition from state " + (row - 1) + " to " + (row);
 					}
 					this.setToolTipText(tooltip);
 				}