diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 3abc4439..dcaf3550 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -68,6 +68,7 @@ public class PrismCL
 	private boolean simulate = false;
 	private boolean simpath = false;
 	private ModelType typeOverride = null;
+	private boolean orderingOverride = false;
 	private boolean explicit = false;
 	private boolean explicitbuild = false;
 	private boolean explicitbuildtest = false;
@@ -470,13 +471,10 @@ public class PrismCL
 		mainLog = new PrismFileLog("stdout");
 		techLog = new PrismFileLog("stdout");
 
-		// create prism object
+		// create prism object(s)
 		prism = new Prism(mainLog, techLog);
 		prismExpl = new PrismExplicit(mainLog, prism.getSettings());
 
-		// get prism defaults
-		verbose = prism.getVerbose();
-
 		// parse command line arguments
 		parseArguments(args);
 
@@ -488,6 +486,9 @@ public class PrismCL
 
 		// do some processing of the options
 		processOptions();
+
+		// store verbosity option locally
+		verbose = prism.getVerbose();
 	}
 
 	// parse model and properties
@@ -956,11 +957,12 @@ public class PrismCL
 		mainLog.println();
 	}
 
-	// parse command line arguments
-
-	public void parseArguments(String[] args) throws PrismException
+	/**
+	 * Process command-line arguments/switches.
+	 */
+	private void parseArguments(String[] args) throws PrismException
 	{
-		int i, j;
+		int i,  j;
 		double d;
 		String sw, s;
 		PrismLog log;
@@ -974,6 +976,10 @@ public class PrismCL
 
 				sw = args[i].substring(1);
 
+				// Note: the order of these switches should match the -help output (just to help keep track of things).
+				// But: processing of "PRISM" options is done elsewhere in PrismSettings
+				// Any "hidden" options, i.e. not in -help text/manual, are indicated as such.
+				
 				// print help
 				if (sw.equals("help") || sw.equals("-help") || sw.equals("?")) {
 					printHelp();
@@ -998,11 +1004,37 @@ public class PrismCL
 						errorAndExit("No property specified for -" + sw + " switch");
 					}
 				}
-				// do steady state
+				// which property to check
+				else if (sw.equals("prop") || sw.equals("property")) {
+					if (i < args.length - 1) {
+						try {
+							propertyToCheck = Integer.parseInt(args[++i]);
+							if (propertyToCheck < 1)
+								throw new NumberFormatException();
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
+					} else {
+						errorAndExit("No value specified for -" + sw + " switch");
+					}
+				}
+				// definition of undefined constants
+				else if (sw.equals("const")) {
+					if (i < args.length - 1) {
+						// store argument for later use (append if already partially specified)
+						if ("".equals(constSwitch))
+							constSwitch = args[++i].trim();
+						else
+							constSwitch += "," + args[++i].trim();
+					} else {
+						errorAndExit("Incomplete -" + sw + " switch");
+					}
+				}
+				// do steady-state probability computation
 				else if (sw.equals("steadystate") || sw.equals("ss")) {
 					steadystate = true;
 				}
-				// do steady state
+				// do transient probability computation
 				else if (sw.equals("transient") || sw.equals("tr")) {
 					if (i < args.length - 1) {
 						try {
@@ -1019,6 +1051,82 @@ public class PrismCL
 						errorAndExit("No value specified for -" + sw + " switch");
 					}
 				}
+				// generate random path with simulator
+				else if (sw.equals("simpath")) {
+					if (i < args.length - 2) {
+						simpath = true;
+						simpathDetails = args[++i];
+						simpathFilename = args[++i];
+					} else {
+						errorAndExit("The -" + sw + " switch requires two arguments (path details, filename)");
+					}
+				}
+				// disable model construction
+				else if (sw.equals("nobuild")) {
+					nobuild = true;
+				}
+				
+				// IMPORT OPTIONS:
+					
+				// change model type to pepa
+				else if (sw.equals("importpepa")) {
+					importpepa = true;
+				}
+				// import model from explicit format
+				else if (sw.equals("importtrans")) {
+					importtrans = true;
+				}
+				// import states for explicit model import
+				else if (sw.equals("importstates")) {
+					if (i < args.length - 1) {
+						importstates = true;
+						importStatesFilename = args[++i];
+					} else {
+						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 distribution e.g. for transient probability distribution
+				else if (sw.equals("importinitdist")) {
+					if (i < args.length - 1) {
+						importinitdist = true;
+						importInitDistFilename = args[++i];
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
+				// override model type to dtmc
+				else if (sw.equals("dtmc")) {
+					typeOverride = ModelType.DTMC;
+				}
+				// override model type to mdp
+				else if (sw.equals("mdp")) {
+					typeOverride = ModelType.MDP;
+				}
+				// override model type to ctmc
+				else if (sw.equals("ctmc")) {
+					typeOverride = ModelType.CTMC;
+				}
+						
+				// EXPORT OPTIONS:
+					
+				// export results
+				else if (sw.equals("exportresults")) {
+					if (i < args.length - 1) {
+						exportresults = true;
+						exportResultsFilename = args[++i];
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export transition matrix to file
 				else if (sw.equals("exporttrans")) {
 					if (i < args.length - 1) {
@@ -1075,23 +1183,25 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
-				// export to spy file
-				else if (sw.equals("exportspy")) {
-					if (i < args.length - 1) {
-						exportspy = true;
-						exportSpyFilename = args[++i];
-					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
-					}
+				// switch export mode to "matlab"
+				else if (sw.equals("exportmatlab")) {
+					exportType = Prism.EXPORT_MATLAB;
 				}
-				// export to dot file
-				else if (sw.equals("exportdot")) {
-					if (i < args.length - 1) {
-						exportdot = true;
-						exportDotFilename = args[++i];
-					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
-					}
+				// switch export mode to "mrmc"
+				else if (sw.equals("exportmrmc")) {
+					exportType = Prism.EXPORT_MRMC;
+				}
+				// switch export mode to "rows"
+				else if (sw.equals("exportrows")) {
+					exportType = Prism.EXPORT_ROWS;
+				}
+				// exported matrix entries are ordered
+				else if (sw.equals("exportordered") || sw.equals("ordered")) {
+					exportordered = true;
+				}
+				// exported matrix entries are unordered
+				else if (sw.equals("exportunordered") || sw.equals("unordered")) {
+					exportordered = false;
 				}
 				// export transition matrix graph to dot file
 				else if (sw.equals("exporttransdot")) {
@@ -1111,6 +1221,15 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export transition matrix MTBDD to dot file
+				else if (sw.equals("exportdot")) {
+					if (i < args.length - 1) {
+						exportdot = true;
+						exportDotFilename = args[++i];
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export bsccs to file
 				else if (sw.equals("exportbsccs")) {
 					if (i < args.length - 1) {
@@ -1120,6 +1239,22 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export steady-state probs (as opposed to displaying on screen) 
+				else if (sw.equals("exportsteadystate") || sw.equals("exportss")) {
+					if (i < args.length - 1) {
+						exportSteadyStateFilename = args[++i];
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
+				// export transient probs (as opposed to displaying on screen) 
+				else if (sw.equals("exporttransient") || sw.equals("exporttr")) {
+					if (i < args.length - 1) {
+						exportTransientFilename = args[++i];
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export prism model to file
 				else if (sw.equals("exportprism")) {
 					if (i < args.length - 1) {
@@ -1138,205 +1273,203 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
-				// export adversary to file
-				else if (sw.equals("exportadv")) {
+				// export reachability target info to file (hidden option)
+				else if (sw.equals("exporttarget")) {
 					if (i < args.length - 1) {
-						prism.setExportAdv(Prism.EXPORT_ADV_DTMC);
-						prism.setExportAdvFilename(args[++i]);
+						prism.setExportTarget(true);
+						prism.setExportTargetFilename(args[++i]);
 					} else {
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
-				// export adversary to file, as an mdp
-				else if (sw.equals("exportadvmdp")) {
+				// export model to plain text file (deprecated option so hidden)
+				else if (sw.equals("exportplain")) {
 					if (i < args.length - 1) {
-						prism.setExportAdv(Prism.EXPORT_ADV_MDP);
-						prism.setExportAdvFilename(args[++i]);
+						exporttrans = true;
+						exportType = Prism.EXPORT_PLAIN;
+						exportTransFilename = args[++i];
+						exportPlainDeprecated = true;
 					} else {
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
-				// export reachability target info to file
-				else if (sw.equals("exporttarget")) {
+				// export to spy file (hidden option)
+				else if (sw.equals("exportspy")) {
 					if (i < args.length - 1) {
-						prism.setExportTarget(true);
-						prism.setExportTargetFilename(args[++i]);
+						exportspy = true;
+						exportSpyFilename = args[++i];
 					} else {
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
-				// disable model construction
-				else if (sw.equals("nobuild")) {
-					nobuild = true;
+				
+				// NB: Following the ordering of the -help text, more options go here,
+				// but these are processed in the PrismSettings class; see below 
+				
+				// SIMULATION OPTIONS:
+				
+				// use simulator for approximate/statistical model checking
+				else if (sw.equals("sim")) {
+					simulate = true;
 				}
-				// set scc computation algorithm
-				else if (sw.equals("sccmethod") || sw.equals("bsccmethod")) {
+				// simulation-based model checking methods
+				else if (sw.equals("simmethod")) {
 					if (i < args.length - 1) {
 						s = args[++i];
-						if (s.equals("xiebeerel"))
-							prism.getSettings().set(PrismSettings.PRISM_SCC_METHOD, "Xie-Beerel");
-						else if (s.equals("lockstep"))
-							prism.getSettings().set(PrismSettings.PRISM_SCC_METHOD, "Lockstep");
-						else if (s.equals("sccfind"))
-							prism.getSettings().set(PrismSettings.PRISM_SCC_METHOD, "SCC-Find");
+						if (s.equals("ci") || s.equals("aci") || s.equals("apmc") || s.equals("sprt"))
+							simMethodName = s;
 						else
-							errorAndExit("Unrecognised option for -" + sw + " switch (options are: xiebeerel, lockstep, sccfind)");
+							errorAndExit("Unrecognised option for -" + sw + " switch (options are: ci, aci, apmc, sprt)");
 					} else {
 						errorAndExit("No parameter specified for -" + sw + " switch");
 					}
 				}
-				// export results
-				else if (sw.equals("exportresults")) {
+				// simulation number of samples
+				else if (sw.equals("simsamples")) {
 					if (i < args.length - 1) {
-						exportresults = true;
-						exportResultsFilename = args[++i];
+						try {
+							simNumSamples = Integer.parseInt(args[++i]);
+							if (simNumSamples <= 0)
+								throw new NumberFormatException("");
+							simNumSamplesGiven = true;
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
 					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
+						errorAndExit("No value specified for -" + sw + " switch");
 					}
 				}
-				// export steady-state probs (as opposed to displaying on screen) 
-				else if (sw.equals("exportsteadystate") || sw.equals("exportss")) {
+				// simulation confidence parameter
+				else if (sw.equals("simconf")) {
 					if (i < args.length - 1) {
-						exportSteadyStateFilename = args[++i];
+						try {
+							simConfidence = Double.parseDouble(args[++i]);
+							if (simConfidence <= 0 || simConfidence >= 1)
+								throw new NumberFormatException("");
+							simConfidenceGiven = true;
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
 					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
+						errorAndExit("No value specified for -" + sw + " switch");
 					}
 				}
-				// export transient probs (as opposed to displaying on screen) 
-				else if (sw.equals("exporttransient") || sw.equals("exporttr")) {
+				// simulation confidence interval width
+				else if (sw.equals("simwidth")) {
 					if (i < args.length - 1) {
-						exportTransientFilename = args[++i];
+						try {
+							simWidth = Double.parseDouble(args[++i]);
+							if (simWidth <= 0)
+								throw new NumberFormatException("");
+							simWidthGiven = true;
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
 					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
+						errorAndExit("No value specified for -" + sw + " switch");
 					}
 				}
-				// switch export mode to "matlab"
-				else if (sw.equals("exportmatlab")) {
-					exportType = Prism.EXPORT_MATLAB;
+				// simulation approximation parameter
+				else if (sw.equals("simapprox")) {
+					if (i < args.length - 1) {
+						try {
+							simApprox = Double.parseDouble(args[++i]);
+							if (simApprox <= 0)
+								throw new NumberFormatException("");
+							simApproxGiven = true;
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
+					} else {
+						errorAndExit("No value specified for -" + sw + " switch");
+					}
 				}
-				// switch export mode to "mrmc"
-				else if (sw.equals("exportmrmc")) {
-					exportType = Prism.EXPORT_MRMC;
+				// use the number of iterations given instead of automatically deciding whether the variance is null ot not
+				else if (sw.equals("simmanual")) {
+					simManual = true;
 				}
-				// switch export mode to "rows"
-				else if (sw.equals("exportrows")) {
-					exportType = Prism.EXPORT_ROWS;
-				}
-				// export model to plain text file (deprecated)
-				else if (sw.equals("exportplain")) {
-					if (i < args.length - 1) {
-						exporttrans = true;
-						exportType = Prism.EXPORT_PLAIN;
-						exportTransFilename = args[++i];
-						exportPlainDeprecated = true;
-					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
-					}
-				}
-				// exported matrix entries are ordered
-				else if (sw.equals("exportordered") || sw.equals("ordered")) {
-					exportordered = true;
-				}
-				// exported matrix entries are unordered
-				else if (sw.equals("exportunordered") || sw.equals("unordered")) {
-					exportordered = false;
-				}
-				// change model type to pepa
-				else if (sw.equals("importpepa")) {
-					importpepa = true;
-				}
-				// import model from explicit format
-				else if (sw.equals("importtrans")) {
-					importtrans = true;
-				}
-				// import states for explicit model import
-				else if (sw.equals("importstates")) {
+				// simulation number of samples to conclude S^2=0 or not
+				else if (sw.equals("simvar")) {
 					if (i < args.length - 1) {
-						importstates = true;
-						importStatesFilename = args[++i];
+						try {
+							reqIterToConclude = Integer.parseInt(args[++i]);
+							if (reqIterToConclude <= 0)
+								throw new NumberFormatException("");
+							reqIterToConcludeGiven = true;
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
 					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
+						errorAndExit("No value specified for -" + sw + " switch");
 					}
 				}
-				// import labels for explicit model import
-				else if (sw.equals("importlabels")) {
+				// maximum value of reward
+				else if (sw.equals("simmaxrwd")) {
 					if (i < args.length - 1) {
-						importlabels = true;
-						importLabelsFilename = args[++i];
+						try {
+							simMaxReward = Double.parseDouble(args[++i]);
+							if (simMaxReward <= 0.0)
+								throw new NumberFormatException("");
+							simMaxRewardGiven = true;
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
 					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
+						errorAndExit("No value specified for -" + sw + " switch");
 					}
 				}
-				// import initial distribution e.g. for transient probability distribution
-				else if (sw.equals("importinitdist")) {
+				// simulation max path length
+				else if (sw.equals("simpathlen")) {
 					if (i < args.length - 1) {
-						importinitdist = true;
-						importInitDistFilename = args[++i];
+						try {
+							simMaxPath = Integer.parseInt(args[++i]);
+							if (simMaxPath <= 0)
+								throw new NumberFormatException("");
+							simMaxPathGiven = true;
+						} catch (NumberFormatException e) {
+							errorAndExit("Invalid value for -" + sw + " switch");
+						}
 					} else {
-						errorAndExit("No file specified for -" + sw + " switch");
+						errorAndExit("No value specified for -" + sw + " switch");
 					}
 				}
-				// override model type to dtmc
-				else if (sw.equals("dtmc")) {
-					typeOverride = ModelType.DTMC;
+
+				// FURTHER OPTIONS - NEED TIDYING/FIXING
+				
+				// zero-reward loops check on
+				else if (sw.equals("zerorewardcheck")) {
+					prism.setCheckZeroLoops(true);
 				}
-				// override model type to mdp
-				else if (sw.equals("mdp")) {
-					typeOverride = ModelType.MDP;
+				// MDP solution method
+				else if (sw.equals("valiter")) {
+					prism.setMDPSolnMethod(Prism.MDP_VALITER);
 				}
-				// override model type to ctmc
-				else if (sw.equals("ctmc")) {
-					typeOverride = ModelType.CTMC;
+				else if (sw.equals("politer")) {
+					prism.setMDPSolnMethod(Prism.MDP_POLITER);
 				}
-				// use simulator
-				else if (sw.equals("sim")) {
-					simulate = true;
+				else if (sw.equals("modpoliter")) {
+					prism.setMDPSolnMethod(Prism.MDP_MODPOLITER);
 				}
-				// use the number of iterations given instead of automatically deciding whether the variance is null ot not
-				else if (sw.equals("simmanual")) {
-					simManual = true;
+				// fix deadlocks
+				else if (sw.equals("fixdl")) {
+					fixdl = true;
 				}
-				// generate path with simulator
-				else if (sw.equals("simpath")) {
-					if (i < args.length - 2) {
-						simpath = true;
-						simpathDetails = args[++i];
-						simpathFilename = args[++i];
-					} else {
-						errorAndExit("The -" + sw + " switch requires two arguments (path details, filename)");
-					}
+				// enable explicit-state engine
+				else if (sw.equals("explicit")) {
+					explicit = true;
 				}
-				// which property to check
-				else if (sw.equals("prop") || sw.equals("property")) {
-					if (i < args.length - 1) {
-						try {
-							propertyToCheck = Integer.parseInt(args[++i]);
-							if (propertyToCheck < 1)
-								throw new NumberFormatException();
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
+				// explicit-state model construction
+				else if (sw.equals("explicitbuild")) {
+					explicitbuild = true;
 				}
-
-				// definition of undefined constants
-				else if (sw.equals("const")) {
-					if (i < args.length - 1) {
-						// store argument for later use (append if already partially specified)
-						if ("".equals(constSwitch))
-							constSwitch = args[++i].trim();
-						else
-							constSwitch += "," + args[++i].trim();
-					} else {
-						errorAndExit("Incomplete -" + sw + " switch");
-					}
+				// (hidden) option for testing of prototypical explicit-state model construction
+				else if (sw.equals("explicitbuildtest")) {
+					explicitbuildtest = true;
 				}
+				
+				// MISCELLANEOUS UNDOCUMENTED/UNUSED OPTIONS:
 
-				// logs
-
-				// specify main log
+				// specify main log (hidden option)
 				else if (sw.equals("mainlog")) {
 					if (i < args.length - 1) {
 						mainLogFilename = args[++i];
@@ -1351,7 +1484,7 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
-				// specify mtbdd log
+				// specify mtbdd log (hidden option)
 				else if (sw.equals("techlog")) {
 					if (i < args.length - 1) {
 						techLogFilename = args[++i];
@@ -1365,27 +1498,7 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
-
-				// engine
-
-				// set engine to 'mtbdd'
-				else if (sw.equals("mtbdd") || sw.equals("m")) {
-					prism.setEngine(Prism.MTBDD);
-					// and change default ordering
-					prism.setOrdering(2);
-				}
-				// set engine to 'sparse'
-				else if (sw.equals("sparse") || sw.equals("s")) {
-					prism.setEngine(Prism.SPARSE);
-				}
-				// set engine to 'hybrid'
-				else if (sw.equals("hybrid") || sw.equals("h")) {
-					prism.setEngine(Prism.HYBRID);
-				}
-
-				// model construction options
-
-				// mtbdd construction method
+				// mtbdd construction method (hidden option)
 				else if (sw.equals("c1")) {
 					prism.setConstruction(1);
 				} else if (sw.equals("c2")) {
@@ -1393,418 +1506,29 @@ public class PrismCL
 				} else if (sw.equals("c3")) {
 					prism.setConstruction(3);
 				}
-				// mtbdd variable ordering
+				// mtbdd variable ordering (hidden option)
 				else if (sw.equals("o1")) {
 					prism.setOrdering(1);
+					orderingOverride = true;
+				} else if (sw.equals("o2")) {
 				} else if (sw.equals("o2")) {
 					prism.setOrdering(2);
+					orderingOverride = true;
+				} else if (sw.equals("o2")) {
 				}
-				// zero-reward loops check on
-				else if (sw.equals("zerorewardcheck")) {
-					prism.setCheckZeroLoops(true);
-				}
-				// reachability off
+				// reachability off (hidden option)
 				else if (sw.equals("noreach")) {
 					prism.setDoReach(false);
 				}
-				// prob/rate checks off
-				else if (sw.equals("noprobchecks")) {
-					prism.setDoProbChecks(false);
-				}
-
-				// model checking options
-
-				// linear equation solver method
-				else if (sw.equals("power") || sw.equals("pow") || sw.equals("pwr")) {
-					prism.setLinEqMethod(Prism.POWER);
-				} else if (sw.equals("jacobi") || sw.equals("jac")) {
-					prism.setLinEqMethod(Prism.JACOBI);
-				} else if (sw.equals("gaussseidel") || sw.equals("gs")) {
-					prism.setLinEqMethod(Prism.GAUSSSEIDEL);
-					prism.setMDPSolnMethod(Prism.MDP_GAUSSSEIDEL);
-				} else if (sw.equals("bgaussseidel") || sw.equals("bgs")) {
-					prism.setLinEqMethod(Prism.BGAUSSSEIDEL);
-				} else if (sw.equals("pgaussseidel") || sw.equals("pgs")) {
-					prism.setLinEqMethod(Prism.PGAUSSSEIDEL);
-				} else if (sw.equals("bpgaussseidel") || sw.equals("bpgs")) {
-					prism.setLinEqMethod(Prism.BPGAUSSSEIDEL);
-				} else if (sw.equals("jor")) {
-					prism.setLinEqMethod(Prism.JOR);
-					prism.setLinEqMethodParam(0.9);
-				} else if (sw.equals("sor")) {
-					prism.setLinEqMethod(Prism.SOR);
-					prism.setLinEqMethodParam(0.9);
-				} else if (sw.equals("bsor")) {
-					prism.setLinEqMethod(Prism.BSOR);
-					prism.setLinEqMethodParam(0.9);
-				} else if (sw.equals("psor")) {
-					prism.setLinEqMethod(Prism.PSOR);
-					prism.setLinEqMethodParam(0.9);
-				} else if (sw.equals("bpsor")) {
-					prism.setLinEqMethod(Prism.BPSOR);
-					prism.setLinEqMethodParam(0.9);
-				}
-				// linear equation solver parameter
-				else if (sw.equals("omega")) {
-					if (i < args.length - 1) {
-						try {
-							d = Double.parseDouble(args[++i]);
-							prism.setLinEqMethodParam(d);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// MDP solution method
-				else if (sw.equals("valiter")) {
-					prism.setMDPSolnMethod(Prism.MDP_VALITER);
-				}
-				else if (sw.equals("politer")) {
-					prism.setMDPSolnMethod(Prism.MDP_POLITER);
-				}
-				else if (sw.equals("modpoliter")) {
-					prism.setMDPSolnMethod(Prism.MDP_MODPOLITER);
-				}
-				// termination criterion (iterative methods)
-				else if (sw.equals("absolute") || sw.equals("abs")) {
-					prism.setTermCrit(Prism.ABSOLUTE);
-				} else if (sw.equals("relative") || sw.equals("rel")) {
-					prism.setTermCrit(Prism.RELATIVE);
-				}
-				// termination criterion parameter
-				else if (sw.equals("epsilon") || sw.equals("e")) {
-					if (i < args.length - 1) {
-						try {
-							d = Double.parseDouble(args[++i]);
-							if (d < 0)
-								throw new NumberFormatException("");
-							prism.setTermCritParam(d);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// max iters
-				else if (sw.equals("maxiters")) {
-					if (i < args.length - 1) {
-						try {
-							j = Integer.parseInt(args[++i]);
-							if (j < 0)
-								throw new NumberFormatException("");
-							prism.setMaxIters(j);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// verbose on
-				else if (sw.equals("verbose") || sw.equals("v")) {
-					prism.setVerbose(true);
-					verbose = true;
-				}
-				// extra dd info on
-				else if (sw.equals("extraddinfo")) {
-					prism.setExtraDDInfo(true);
-				}
-				// extra reach info on
-				else if (sw.equals("extrareachinfo")) {
-					prism.setExtraReachInfo(true);
-				}
-				// precomputation algs off
-				else if (sw.equals("nopre")) {
-					prism.setPrecomp(false);
-				}
-				// fairness on
-				else if (sw.equals("fair")) {
-					prism.setFairness(true);
-				}
-				// fairness off
-				else if (sw.equals("nofair")) {
-					prism.setFairness(false);
-				}
-				// fix deadlocks
-				else if (sw.equals("fixdl")) {
-					fixdl = true;
-				}
-				// no bscc computation
+				// no bscc computation (hidden option)
 				else if (sw.equals("nobscc")) {
 					prism.setBSCCComp(false);
 				}
-				// no steady-state detection
-				else if (sw.equals("nossdetect")) {
-					prism.setDoSSDetect(false);
-				}
-				// sparse bits info
-				else if (sw.equals("sbmax")) {
-					if (i < args.length - 1) {
-						try {
-							j = Integer.parseInt(args[++i]);
-							if (j < 0)
-								throw new NumberFormatException();
-							prism.setSBMaxMem(j);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				} else if (sw.equals("sbl")) {
-					if (i < args.length - 1) {
-						try {
-							j = Integer.parseInt(args[++i]);
-							if (j < -1)
-								throw new NumberFormatException();
-							prism.setNumSBLevels(j);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// hybrid sor info
-				else if (sw.equals("sormax") || sw.equals("gsmax")) {
-					if (i < args.length - 1) {
-						try {
-							j = Integer.parseInt(args[++i]);
-							if (j < 0)
-								throw new NumberFormatException();
-							prism.setSORMaxMem(j);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				} else if (sw.equals("sorl") || sw.equals("gsl")) {
-					if (i < args.length - 1) {
-						try {
-							j = Integer.parseInt(args[++i]);
-							if (j < -1)
-								throw new NumberFormatException();
-							prism.setNumSORLevels(j);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// turn off compact option for sparse matrix storage
-				else if (sw.equals("nocompact")) {
-					prism.setCompact(false);
-				}
-				// cudd settings
-				else if (sw.equals("cuddmaxmem")) {
-					if (i < args.length - 1) {
-						try {
-							j = Integer.parseInt(args[++i]);
-							if (j < 0)
-								throw new NumberFormatException();
-							prism.setCUDDMaxMem(j);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				} else if (sw.equals("cuddepsilon")) {
-					if (i < args.length - 1) {
-						try {
-							d = Double.parseDouble(args[++i]);
-							if (d < 0)
-								throw new NumberFormatException("");
-							prism.setCUDDEpsilon(d);
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-
-				// simulation-based model checking methods
-				else if (sw.equals("simmethod")) {
-					if (i < args.length - 1) {
-						s = args[++i];
-						if (s.equals("ci") || s.equals("aci") || s.equals("apmc") || s.equals("sprt"))
-							simMethodName = s;
-						else
-							errorAndExit("Unrecognised option for -" + sw + " switch (options are: ci, aci, apmc, sprt)");
-					} else {
-						errorAndExit("No parameter specified for -" + sw + " switch");
-					}
-				}
-				// simulation confidence interval width
-				else if (sw.equals("simwidth")) {
-					if (i < args.length - 1) {
-						try {
-							simWidth = Double.parseDouble(args[++i]);
-							if (simWidth <= 0)
-								throw new NumberFormatException("");
-							simWidthGiven = true;
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// simulation approximation parameter
-				else if (sw.equals("simapprox")) {
-					if (i < args.length - 1) {
-						try {
-							simApprox = Double.parseDouble(args[++i]);
-							if (simApprox <= 0)
-								throw new NumberFormatException("");
-							simApproxGiven = true;
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// simulation confidence parameter
-				else if (sw.equals("simconf")) {
-					if (i < args.length - 1) {
-						try {
-							simConfidence = Double.parseDouble(args[++i]);
-							if (simConfidence <= 0 || simConfidence >= 1)
-								throw new NumberFormatException("");
-							simConfidenceGiven = true;
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// simulation number of samples
-				else if (sw.equals("simsamples")) {
-					if (i < args.length - 1) {
-						try {
-							simNumSamples = Integer.parseInt(args[++i]);
-							if (simNumSamples <= 0)
-								throw new NumberFormatException("");
-							simNumSamplesGiven = true;
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// simulation number of samples to conclude S^2=0 or not
-				else if (sw.equals("simvar")) {
-					if (i < args.length - 1) {
-						try {
-							reqIterToConclude = Integer.parseInt(args[++i]);
-							if (reqIterToConclude <= 0)
-								throw new NumberFormatException("");
-							reqIterToConcludeGiven = true;
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// maximum value of reward
-				else if (sw.equals("simmaxrwd")) {
-					if (i < args.length - 1) {
-						try {
-							simMaxReward = Double.parseDouble(args[++i]);
-							if (simMaxReward <= 0.0)
-								throw new NumberFormatException("");
-							simMaxRewardGiven = true;
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-				// simulation max path length
-				else if (sw.equals("simpathlen")) {
-					if (i < args.length - 1) {
-						try {
-							simMaxPath = Integer.parseInt(args[++i]);
-							if (simMaxPath <= 0)
-								throw new NumberFormatException("");
-							simMaxPathGiven = true;
-						} catch (NumberFormatException e) {
-							errorAndExit("Invalid value for -" + sw + " switch");
-						}
-					} else {
-						errorAndExit("No value specified for -" + sw + " switch");
-					}
-				}
-
-				// enable symmetry reduction
-				else if (sw.equals("symm")) {
-					if (i < args.length - 2) {
-						prism.getSettings().set(PrismSettings.PRISM_SYMM_RED_PARAMS, args[++i] + " " + args[++i]);
-					} else {
-						errorAndExit("-symm switch requires two parameters (num. modules before/after symmetric ones)");
-					}
-				}
-
-				// pta model checking methods
-				else if (sw.equals("ptamethod")) {
-					if (i < args.length - 1) {
-						s = args[++i];
-						if (s.equals("digital"))
-							prism.getSettings().set(PrismSettings.PRISM_PTA_METHOD, "Digital clocks");
-						else if (s.equals("games"))
-							prism.getSettings().set(PrismSettings.PRISM_PTA_METHOD, "Stochastic games");
-						else if (s.equals("bisim"))
-							prism.getSettings().set(PrismSettings.PRISM_PTA_METHOD, "Bisimulation minimisation");
-						else
-							errorAndExit("Unrecognised option for -" + sw + " switch (options are: digital, games)");
-					} else {
-						errorAndExit("No parameter specified for -" + sw + " switch");
-					}
-				}
-
-				// abstraction-refinement engine options string (append if already partially specified)
-				else if (sw.equals("aroptions")) {
-					if (i < args.length - 1) {
-						String arOptions = prism.getSettings().getString(PrismSettings.PRISM_AR_OPTIONS);
-						if ("".equals(arOptions))
-							arOptions = args[++i].trim();
-						else
-							arOptions += "," + args[++i].trim();
-						prism.getSettings().set(PrismSettings.PRISM_AR_OPTIONS, arOptions);
-					} else {
-						errorAndExit("No parameter specified for -" + sw + " switch");
-					}
-				}
 
-				// enable explicit-state engine
-				else if (sw.equals("explicit")) {
-					explicit = true;
-				}
+				// Other switches - pass to PrismSettings
 				
-				// explicit-state model construction
-				else if (sw.equals("explicitbuild")) {
-					explicitbuild = true;
-				}
-				
-				// (hidden) option for testing of prototypical explicit-state model construction
-				else if (sw.equals("explicitbuildtest")) {
-					explicitbuildtest = true;
-				}
-
-				// unknown switch - error
 				else {
-					errorAndExit("Invalid switch -" + sw + " (type \"prism -help\" for full list)");
+					i = prism.getSettings().setFromCommandLineSwitch(args, i) - 1;
 				}
 			}
 			// otherwise argument must be a filename
@@ -1853,6 +1577,15 @@ public class PrismCL
 			exit();
 		}
 
+		// default to alternative ordering for MTBDD engine
+		if (prism.getEngine() == Prism.MTBDD && !orderingOverride) {
+			try {
+				prism.setOrdering(2);
+			} catch (PrismException e) {
+				// Can't go wrong
+			}
+		}
+
 		// explicit overrides explicit build
 		if (explicit) {
 			explicitbuild = false;
@@ -2014,7 +1747,7 @@ public class PrismCL
 		mainLog.println("-version ....................... Display tool version");
 		mainLog.println();
 		mainLog.println("-pctl <prop> (or -csl <prop>) .. Model check the PCTL/CSL property <prop>");
-		mainLog.println("-property <n> (or -prop <n>) ... Only model check property <n> from the properties file");
+		mainLog.println("-property <n> (or -prop <n>) ... Only model check property <n>");
 		mainLog.println("-const <vals> .................. Define constant values as <vals> (e.g. for experiments)");
 		mainLog.println("-steadystate (or -ss) .......... Compute steady-state probabilities (D/CTMCs only)");
 		mainLog.println("-transient <x> (or -tr <x>) .... Compute transient probabilities for time <x> (D/CTMCs only)");
@@ -2026,7 +1759,6 @@ public class PrismCL
 		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("-importinitdist <expr>.......... Specify the initial probability distribution for transient analysis");
 		mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC");
 		mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC");
@@ -2037,6 +1769,7 @@ public class PrismCL
 		mainLog.println("-exporttrans <file> ............ Export the transition matrix to a file");
 		mainLog.println("-exportstaterewards <file> ..... Export the state rewards vector to a file");
 		mainLog.println("-exporttransrewards <file> ..... Export the transition rewards matrix to a file");
+		mainLog.println("-exportrewards <file1> <file2>.. Export state/transition rewards to files 1/2");
 		mainLog.println("-exportstates <file> ........... Export the list of reachable states to a file");
 		mainLog.println("-exportlabels <file> ........... Export the list of labels and satisfying states to a file");
 		mainLog.println("-exportmatlab .................. When exporting matrices/vectors/labels/etc., use Matlab format");
@@ -2052,8 +1785,6 @@ public class PrismCL
 		mainLog.println("-exporttransient <file> ........ Export transient probabilities to a file");
 		mainLog.println("-exportprism <file> ............ Export final PRISM model to a file");
 		mainLog.println("-exportprismconst <file> ....... Export final PRISM model with expanded constants to a file");
-		mainLog.println("-exportadv <file> .............. Export an adversary from MDP model checking (as a DTMC)");
-		mainLog.println("-exportadvmdp <file> ........... Export an adversary from MDP model checking (as an MDP)");
 		mainLog.println();
 		mainLog.println("ENGINES/METHODS:");
 		mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine");
@@ -2081,13 +1812,17 @@ public class PrismCL
 		mainLog.println();
 		mainLog.println("MODEL CHECKING OPTIONS:");
 		mainLog.println("-nopre ......................... Skip (optional) precomputation algorithms");
-		mainLog.println("-fair .......................... Use fairness (for probabilistic reachability in MDPs)");
-		mainLog.println("-nofair ........................ Don't use fairness (for probabilistic reachability in MDPs) [default]");
+		mainLog.println("-fair .......................... Use fairness (for model checking of MDPs)");
+		mainLog.println("-nofair ........................ Don't use fairness (for model checking of MDPs) [default]");
 		mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states");
 		mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates");
 		mainLog.println("-zerorewardcheck ............... Check for absence of zero-reward loops");
 		mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations");
 		mainLog.println("-sccmethod <name> .............. Specify SCC computation method (xiebeerel, lockstep, sccfind)");
+		mainLog.println("-symm <string> ................. Symmetry reduction options string");
+		mainLog.println("-aroptions <string> ............ Abstraction-refinement engine options string");
+		mainLog.println("-exportadv <file> .............. Export an adversary from MDP model checking (as a DTMC)");
+		mainLog.println("-exportadvmdp <file> ........... Export an adversary from MDP model checking (as an MDP)");
 		mainLog.println();
 		mainLog.println("OUTPUT OPTIONS:");
 		mainLog.println("-verbose (or -v) ............... Verbose mode: print out state lists and probability vectors");
diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java
index 585c93ab..9237794f 100644
--- a/prism/src/prism/PrismSettings.java
+++ b/prism/src/prism/PrismSettings.java
@@ -34,12 +34,11 @@ import java.awt.*;
 import javax.swing.*;
 import java.util.regex.*;
 
+import parser.ast.*;
 import settings.*;
 
-
 public class PrismSettings implements Observer
 {
-	
 	//Default Constants
 	public static final String DEFAULT_STRING = "";
 	public static final int DEFAULT_INT = 0;
@@ -171,7 +170,7 @@ public class PrismSettings implements Observer
 	
 	// Property table:
 	// * Datatype = type of choice (see type constants at top of this file)
-	// * Key= internal key, used programmatically; need to add this to key list above
+	// * Key = internal key, used programmatically; need to add this to key list above
 	// * Display name = display name; used e.g. in GUI options dialog
 	// * Version = last public version of PRISM in which this setting did *not* appear
 	//   (the main use for this is to allow a new default setting to be provided in a new version of PRISM)
@@ -207,7 +206,7 @@ public class PrismSettings implements Observer
 			{ BOOLEAN_TYPE,		PRISM_PRECOMPUTATION,					"Use precomputation",					"2.1",			new Boolean(true),															"",																							
 																			"Use model checking precomputation algorithms (Prob0, Prob1, etc.), where optional." },
 			{ BOOLEAN_TYPE,		PRISM_FAIRNESS,							"Use fairness",							"2.1",			new Boolean(false),															"",																							
-																			"Constrain to fair adversaries when model checking probabilistic reachability properties of MDPs." },
+																			"Constrain to fair adversaries when model checking MDPs." },
 			{ BOOLEAN_TYPE,		PRISM_DO_PROB_CHECKS,					"Do probability/rate checks",			"2.1",			new Boolean(true),															"",																							
 																			"Perform sanity checks on model probabilities/rates when constructing probabilistic models." },
 			{ BOOLEAN_TYPE,		PRISM_DO_SS_DETECTION,					"Use steady-state detection",			"2.1",			new Boolean(true),															"0,",																						
@@ -236,11 +235,11 @@ public class PrismSettings implements Observer
 																			"Number of MTBDD levels descended for hybrid engine data structures block division with GS/SOR." },
 			{ INTEGER_TYPE,		PRISM_SOR_MAX_MEM,						"Hybrid GS memory (KB)",				"2.1",			new Integer(1024),															"0,",																						
 																			"Maximum memory usage for hybrid engine data structures block division with GS/SOR (KB)." },
-			{ INTEGER_TYPE,		PRISM_CUDD_MAX_MEM,						"CUDD max. memory (KB)",				"2.1",			new Integer(204800),														"0,",																						
+			{ INTEGER_TYPE,		PRISM_CUDD_MAX_MEM,						"CUDD max. memory (KB)",				"2.1",			new Integer(409600),														"0,",																						
 																			"Maximum memory available to CUDD (underlying BDD/MTBDD library) in KB (Note: Restart PRISM after changing this.)" },
 			{ DOUBLE_TYPE,		PRISM_CUDD_EPSILON,						"CUDD epsilon",							"2.1",			new Double(1.0E-15),														"0.0,",																						
 																			"Epsilon value used by CUDD (underlying BDD/MTBDD library) for terminal cache comparisons." },
-			// ADVERSARIES/COUNTEREXAMPLES
+			// ADVERSARIES/COUNTEREXAMPLES:
 			{ CHOICE_TYPE,		PRISM_EXPORT_ADV,						"Adversary export",						"3.3",			"None",																	"None,DTMC,MDP",																
 																			"Type of adversary to generate and export during MDP model checking" },
 			{ STRING_TYPE,		PRISM_EXPORT_ADV_FILENAME,				"Adversary export filename",			"3.3",			"adv.tra",																	"",															
@@ -307,7 +306,7 @@ public class PrismSettings implements Observer
 		}
 	};
 	
-	public static final String[] oldPropertyNames = {"simulator.apmcStrategy", "simulator.engine", "simulator.newPathAskDefault"};
+	public static final String[] oldPropertyNames =  {"simulator.apmcStrategy", "simulator.engine", "simulator.newPathAskDefault"};
 	
 	public DefaultSettingOwner[] optionOwners;
 	private Hashtable<String,Setting> data;
@@ -315,6 +314,9 @@ public class PrismSettings implements Observer
 	
 	private ArrayList<PrismSettingsListener> settingsListeners;
 	
+	/**
+	 * Default constructor: set all options to default values. 
+	 */
 	public PrismSettings()
 	{
 		optionOwners = new DefaultSettingOwner[propertyOwnerIDs.length];
@@ -424,7 +426,25 @@ public class PrismSettings implements Observer
 		//populate a hash table with the keys
 		populateHashTable(counter);
 		settingsListeners = new ArrayList<PrismSettingsListener>();
-		
+	}
+	
+	/**
+	 * Copy constructor. 
+	 */
+	public PrismSettings(PrismSettings settings)
+	{
+		// Create anew with default values
+		// (that way, we get a fresh set of Setting objects)
+		this();
+		// Then, copy across options
+		for (Map.Entry<String,Setting> e : settings.data.entrySet()) {
+			try {
+				set(e.getKey(), e.getValue().getValue());
+			} catch (PrismException ex) {
+				// Should never happen
+				System.err.println(ex);
+			}
+		}
 	}
 	
 	private void populateHashTable(int size)
@@ -677,52 +697,348 @@ public class PrismSettings implements Observer
 		notifySettingsListeners();
 	}
 	
-	public synchronized void set(String key, Object value) throws PrismException
+	/**
+	 * Set an option by parsing one or more command-line arguments.
+	 * Reads the ith argument (assumed to be in the form "-switch")
+	 * and also any subsequent arguments required as parameters.
+	 * Return the index of the next argument to be read.
+	 * @param args Full list of arguments
+	 * @param i Index of first argument to read
+	 */
+	public synchronized int setFromCommandLineSwitch(String args[], int i) throws PrismException
 	{
-		Setting set = settingFromHash(key);
-		if(set == null)throw new PrismException("Property "+key+" is not valid.");
-		try
-		{
-			String oldValueString = set.toString();
-			
-			if(value instanceof Integer && set instanceof ChoiceSetting)
-			{
-				int iv = ((Integer)value).intValue();
-				((ChoiceSetting)set).setSelectedIndex(iv);
+		String sw, s;
+		int j;
+		double d;
+		
+		sw = args[i].substring(1);
+
+		// ENGINES/METHODS:
+		
+		// Main model checking engine
+		if (sw.equals("mtbdd") || sw.equals("m")) {
+			set(PRISM_ENGINE, "MTBDD");
+		}
+		else if (sw.equals("sparse") || sw.equals("s")) {
+			set(PRISM_ENGINE, "Sparse");
+		}
+		else if (sw.equals("hybrid") || sw.equals("h")) {
+			set(PRISM_ENGINE, "Hybrid");
+		}
+		// PTA model checking methods
+		else if (sw.equals("ptamethod")) {
+			if (i < args.length - 1) {
+				s = args[++i];
+				if (s.equals("digital"))
+					set(PRISM_PTA_METHOD, "Digital clocks");
+				else if (s.equals("games"))
+					set(PRISM_PTA_METHOD, "Stochastic games");
+				else if (s.equals("bisim"))
+					set(PRISM_PTA_METHOD, "Bisimulation minimisation");
+				else
+					throw new PrismException("Unrecognised option for -" + sw + " switch (options are: digital, games)");
+			} else {
+				throw new PrismException("No parameter specified for -" + sw + " switch");
 			}
-			else
-			{
-				set.setValue(value);
+		}
+
+		// NUMERICAL SOLUTION OPTIONS:
+		
+		// Linear equation solver method
+		else if (sw.equals("power") || sw.equals("pow") || sw.equals("pwr")) {
+			set(PRISM_LIN_EQ_METHOD, "Power");
+		} else if (sw.equals("jacobi") || sw.equals("jac")) {
+			set(PRISM_LIN_EQ_METHOD, "Jacobi");
+		} else if (sw.equals("gaussseidel") || sw.equals("gs")) {
+			set(PRISM_LIN_EQ_METHOD, "Gauss-Seidel");
+		} else if (sw.equals("bgaussseidel") || sw.equals("bgs")) {
+			set(PRISM_LIN_EQ_METHOD, "Backwards Gauss-Seidel");
+		} else if (sw.equals("pgaussseidel") || sw.equals("pgs")) {
+			set(PRISM_LIN_EQ_METHOD, "Pseudo-Gauss-Seidel");
+		} else if (sw.equals("bpgaussseidel") || sw.equals("bpgs")) {
+			set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-Gauss-Seidel");
+		} else if (sw.equals("jor")) {
+			set(PRISM_LIN_EQ_METHOD, "JOR");
+		} else if (sw.equals("sor")) {
+			set(PRISM_LIN_EQ_METHOD, "SOR");
+		} else if (sw.equals("bsor")) {
+			set(PRISM_LIN_EQ_METHOD, "Backwards SOR");
+		} else if (sw.equals("psor")) {
+			set(PRISM_LIN_EQ_METHOD, "Pseudo-SOR");
+		} else if (sw.equals("bpsor")) {
+			set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-SOR");
+		}
+		// Termination criterion (iterative methods)
+		else if (sw.equals("absolute") || sw.equals("abs")) {
+			set(PRISM_TERM_CRIT, "Absolute");
+		} else if (sw.equals("relative") || sw.equals("rel")) {
+			set(PRISM_TERM_CRIT, "Relative");
+		}
+		// Termination criterion parameter
+		else if (sw.equals("epsilon") || sw.equals("e")) {
+			if (i < args.length - 1) {
+				try {
+					d = Double.parseDouble(args[++i]);
+					if (d < 0)
+						throw new NumberFormatException("");
+					set(PRISM_TERM_CRIT_PARAM, d);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
 			}
-			
-			notifySettingsListeners();
-			
-			if(!set.toString().equals(oldValueString))modified = true;
 		}
-		catch(SettingException e)
-		{
-			throw new PrismException(e.getMessage());
+		// Linear equation solver over-relaxation parameter
+		else if (sw.equals("omega")) {
+			if (i < args.length - 1) {
+				try {
+					d = Double.parseDouble(args[++i]);
+					set(PRISM_LIN_EQ_METHOD_PARAM, d);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		// Max iters
+		else if (sw.equals("maxiters")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < 0)
+						throw new NumberFormatException("");
+					set(PRISM_MAX_ITERS, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+
+		// MODEL CHECKING OPTIONS:
+		
+		// Precomputation algs off
+		else if (sw.equals("nopre")) {
+			set(PRISM_PRECOMPUTATION, false);
+		}
+		// Fairness on/off
+		else if (sw.equals("fair")) {
+			set(PRISM_FAIRNESS, true);
+		}
+		else if (sw.equals("nofair")) {
+			set(PRISM_FAIRNESS, false);
+		}
+		// Prob/rate checks off
+		else if (sw.equals("noprobchecks")) {
+			set(PRISM_DO_PROB_CHECKS, false);
+		}
+		// No steady-state detection
+		else if (sw.equals("nossdetect")) {
+			set(PRISM_DO_SS_DETECTION, false);
+		}
+		// SCC computation algorithm
+		else if (sw.equals("sccmethod") || sw.equals("bsccmethod")) {
+			if (i < args.length - 1) {
+				s = args[++i];
+				if (s.equals("xiebeerel"))
+					set(PRISM_SCC_METHOD, "Xie-Beerel");
+				else if (s.equals("lockstep"))
+					set(PRISM_SCC_METHOD, "Lockstep");
+				else if (s.equals("sccfind"))
+					set(PRISM_SCC_METHOD, "SCC-Find");
+				else
+					throw new PrismException("Unrecognised option for -" + sw + " switch (options are: xiebeerel, lockstep, sccfind)");
+			} else {
+				throw new PrismException("No parameter specified for -" + sw + " switch");
+			}
+		}
+		// Enable symmetry reduction
+		else if (sw.equals("symm")) {
+			if (i < args.length - 2) {
+				set(PRISM_SYMM_RED_PARAMS, args[++i] + " " + args[++i]);
+			} else {
+				throw new PrismException("-symm switch requires two parameters (num. modules before/after symmetric ones)");
+			}
+		}
+		// Abstraction-refinement engine options string (append if already partially specified)
+		else if (sw.equals("aroptions")) {
+			if (i < args.length - 1) {
+				String arOptions = getString(PRISM_AR_OPTIONS);
+				if ("".equals(arOptions))
+					arOptions = args[++i].trim();
+				else
+					arOptions += "," + args[++i].trim();
+				set(PRISM_AR_OPTIONS, arOptions);
+			} else {
+				throw new PrismException("No parameter specified for -" + sw + " switch");
+			}
 		}
+		
+		// OUTPUT OPTIONS:
+		
+		// Verbosity
+		else if (sw.equals("verbose") || sw.equals("v")) {
+			set(PRISM_VERBOSE, true);
+		}
+		// Extra dd info on
+		else if (sw.equals("extraddinfo")) {
+			set(PRISM_EXTRA_DD_INFO, true);
+		}
+		// Extra reach info on
+		else if (sw.equals("extrareachinfo")) {
+			set(PRISM_EXTRA_REACH_INFO, true);
+		}
+		
+		// SPARSE/HYBRID/MTBDD OPTIONS:
+		
+		// Turn off compact option for sparse matrix storage
+		else if (sw.equals("nocompact")) {
+			set(PRISM_COMPACT, false);
+		}
+		// Sparse bits info
+		else if (sw.equals("sbl")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < -1)
+						throw new NumberFormatException();
+					set(PRISM_NUM_SB_LEVELS, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		else if (sw.equals("sbmax")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < 0)
+						throw new NumberFormatException();
+					set(PRISM_SB_MAX_MEM, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		// Hybrid SOR info
+		else if (sw.equals("sorl") || sw.equals("gsl")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < -1)
+						throw new NumberFormatException();
+					set(PRISM_NUM_SOR_LEVELS, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		else if (sw.equals("sormax") || sw.equals("gsmax")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < 0)
+						throw new NumberFormatException();
+					set(PRISM_SOR_MAX_MEM, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		// CUDD settings
+		else if (sw.equals("cuddmaxmem")) {
+			if (i < args.length - 1) {
+				try {
+					j = Integer.parseInt(args[++i]);
+					if (j < 0)
+						throw new NumberFormatException();
+					set(PRISM_CUDD_MAX_MEM, j);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		else if (sw.equals("cuddepsilon")) {
+			if (i < args.length - 1) {
+				try {
+					d = Double.parseDouble(args[++i]);
+					if (d < 0)
+						throw new NumberFormatException("");
+					set(PRISM_CUDD_EPSILON, d);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		}
+		
+		// ADVERSARIES/COUNTEREXAMPLES:
+		
+		// Export adversary to file
+		else if (sw.equals("exportadv")) {
+			if (i < args.length - 1) {
+				set(PRISM_EXPORT_ADV, "DTMC");
+				set(PRISM_EXPORT_ADV_FILENAME, args[++i]);
+			} else {
+				throw new PrismException("No file specified for -" + sw + " switch");
+			}
+		}
+		// Export adversary to file, as an MDP
+		else if (sw.equals("exportadvmdp")) {
+			if (i < args.length - 1) {
+				set(PRISM_EXPORT_ADV, "MDP");
+				set(PRISM_EXPORT_ADV_FILENAME, args[++i]);
+			} else {
+				throw new PrismException("No file specified for -" + sw + " switch");
+			}
+		}
+		
+		// unknown switch - error
+		else {
+			throw new PrismException("Invalid switch -" + sw + " (type \"prism -help\" for full list)");
+		}
+		
+		return i + 1;
 	}
 	
-	public synchronized void set(String key, String value) throws PrismException
+	/**
+	 * Set the value for an option, with the option key given as a String,
+	 * and the value as an Object of appropriate type or a String to be parsed.
+	 * For options of type ChoiceSetting, either a String or (0-indexed) Integer can be used.
+	 */
+	public synchronized void set(String key, Object value) throws PrismException
 	{
 		Setting set = settingFromHash(key);
-		for(int i = 0; (i < optionOwners.length) && (set==null); i++)
-		{
-			set = optionOwners[i].getFromKey(key);
-		}
-		if(set == null)throw new PrismException("Property "+key+" is not valid.");
+		if (set == null)
+			throw new PrismException("Property " + key + " is not valid");
 		try
 		{
-			Object obj = set.parseStringValue(value);
 			String oldValueString = set.toString();
-			
-			set.setValue(obj);
-			
+			if (value instanceof String) {
+				set.setValue(set.parseStringValue((String) value));
+			} else if (value instanceof Integer && set instanceof ChoiceSetting) {
+				int iv = ((Integer)value).intValue();
+				((ChoiceSetting) set).setSelectedIndex(iv);
+			} else {
+				set.setValue(value);
+			}
 			notifySettingsListeners();
-			
-			if(!set.toString().equals(oldValueString))modified = true;
+			if (!set.toString().equals(oldValueString))
+				modified = true;
 		}
 		catch(SettingException e)
 		{
@@ -733,31 +1049,12 @@ public class PrismSettings implements Observer
 	public synchronized void setFileSelector(String key, FileSelector select)
 	{
 		Setting set = settingFromHash(key);
-		if(set instanceof FileSetting)
-		{
+		if (set instanceof FileSetting) {
 			FileSetting fset = (FileSetting)set;
-			
 			fset.setFileSelector(select);
 		}
 	}
 	
-	//The following methods are kept in for legacy purposes
-	
-	public synchronized void set(String key, int value) throws PrismException
-	{
-		set(key, new Integer(value));
-	}
-	
-	public synchronized void set(String key, boolean value) throws PrismException
-	{
-		set(key, new Boolean(value));
-	}
-	
-	public synchronized void set(String key, double value) throws PrismException
-	{
-		set(key, new Double(value));
-	}
-	
 	public synchronized String getString(String key)
 	{
 		Setting set = settingFromHash(key);