diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index f3cc8934..8db9af2f 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/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]); diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java index 391dec77..09a039c6 100644 --- a/prism/src/prism/TestModelGenerator.java +++ b/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);