explicit: make state sorting optional

When constructing a model using the explicit engine, the set of
reachable states is always sorted. This is done purely for aesthetic
reasons and is potentially time-consuming for large models, so make it
optional (although enable it by default for backwards-compatibility, and
explicitly enable state sorting in the test cases that use
ConstructModel in case this default changes at a later time).

prism/src/explicit/ConstructModel.java

@@ -60,6 +60,8 @@ public class ConstructModel extends PrismComponent
 	protected boolean findDeadlocks = true;
 	/** Automatically fix deadlocks? */
 	protected boolean fixDeadlocks = true;
+	/** Sort the reachable states before constructing the model? */
+	protected boolean sortStates = true;
 	/** Build a sparse representation, if possible?
 	 *  (e.g. MDPSparse rather than MDPSimple data structure) */
 	protected boolean buildSparse = true;
@@ -95,6 +97,14 @@ public class ConstructModel extends PrismComponent
 		this.fixDeadlocks = fixDeadlocks;
 	}
 
+	/**
+	 * Sort the reachable states before constructing the model?
+	 */
+	public void setSortStates(boolean sortStates)
+	{
+		this.sortStates = sortStates;
+	}
+
 	/**
 	 * Build a sparse representation, if possible?
 	 * (e.g. MDPSparse rather than MDPSimple data structure)
@@ -308,10 +318,9 @@ public class ConstructModel extends PrismComponent
 			modelSimple.findDeadlocks(fixDeadlocks);
 		}
 
-		boolean sort = true;
 		int permut[] = null;
 
-		if (sort) {
+		if (sortStates) {
 			// Sort states and convert set to list
 			mainLog.println("Sorting reachable states list...");
 			permut = states.buildSortingPermutation();
@@ -324,28 +333,28 @@ public class ConstructModel extends PrismComponent
 		states = null;
 		//mainLog.println(statesList);
 
-		// Construct new explicit-state model (with correct state ordering)
+		// Construct new explicit-state model (with correct state ordering, if desired)
 		if (!justReach) {
 			switch (modelType) {
 			case DTMC:
 				if (buildSparse) {
-					model = sort ? new DTMCSparse(dtmc, permut) : new DTMCSparse(dtmc);
+					model = sortStates ? new DTMCSparse(dtmc, permut) : new DTMCSparse(dtmc);
 				} else {
-					model = sort ? new DTMCSimple(dtmc, permut) : (DTMCSimple) dtmc;
+					model = sortStates ? new DTMCSimple(dtmc, permut) : (DTMCSimple) dtmc;
 				}
 				break;
 			case CTMC:
-				model = sort ? new CTMCSimple(ctmc, permut) : (CTMCSimple) ctmc;
+				model = sortStates ? new CTMCSimple(ctmc, permut) : (CTMCSimple) ctmc;
 				break;
 			case MDP:
 				if (buildSparse) {
-					model = sort ? new MDPSparse(mdp, true, permut) : new MDPSparse(mdp);
+					model = sortStates ? new MDPSparse(mdp, true, permut) : new MDPSparse(mdp);
 				} else {
-					model = sort ? new MDPSimple(mdp, permut) : mdp;
+					model = sortStates ? new MDPSimple(mdp, permut) : mdp;
 				}
 				break;
 			case CTMDP:
-				model = sort ? new CTMDPSimple(ctmdp, permut) : mdp;
+				model = sortStates ? new CTMDPSimple(ctmdp, permut) : mdp;
 				break;
 			case STPG:
 			case SMG:
@@ -411,6 +420,7 @@ public class ConstructModel extends PrismComponent
 				undefinedConstants.defineUsingConstSwitch(args[2]);
 			modulesFile.setUndefinedConstants(undefinedConstants.getMFConstantValues());
 			ConstructModel constructModel = new ConstructModel(prism);
+			constructModel.setSortStates(true);
 			simulator.ModulesFileModelGenerator modelGen = new simulator.ModulesFileModelGenerator(modulesFile, constructModel);
 			Model model = constructModel.constructModel(modelGen);
 			model.exportToPrismExplicitTra(args[1]);

prism/src/prism/TestModelGenerator.java

@@ -196,6 +196,7 @@ public class TestModelGenerator implements ModelGenerator
 				// Direct usage of model constructor/checker 
 				TestModelGenerator modelGen = new TestModelGenerator(10);
 				ConstructModel constructModel = new ConstructModel(prism);
+				constructModel.setSortStates(true);
 				explicit.Model model = constructModel.constructModel(modelGen);
 				model.exportToDotFile(new PrismFileLog("test.dot"), null, true);
 				DTMCModelChecker mc = new DTMCModelChecker(prism);