From 79c4f594d5b9d79175ee506996a3a4922311d3a5 Mon Sep 17 00:00:00 2001 From: Chris Novakovic Date: Mon, 17 Dec 2018 12:07:17 +0000 Subject: [PATCH] Expose state sorting option in PRISM's core functionality Although it is possible to enable or disable state sorting in an explicit ModelGenerator directly, it is not possible to do so via the prism.Prism class, which is the more common way to interact with the PRISM API. Create a new setting PRISM_SORT_STATES to control this behaviour in underlying explicit ModelGenerators, and add methods for controlling its value in prism.Prism. --- prism/src/prism/Prism.java | 12 ++++++++++++ prism/src/prism/PrismSettings.java | 3 +++ 2 files changed, 15 insertions(+) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 3776d1ef96..7814e6bf7f 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -399,6 +399,11 @@ public void setFixDeadlocks(boolean b) throws PrismException settings.set(PrismSettings.PRISM_FIX_DEADLOCKS, b); } + public void setSortStates(boolean b) throws PrismException + { + settings.set(PrismSettings.PRISM_SORT_STATES, b); + } + public void setDoProbChecks(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_DO_PROB_CHECKS, b); @@ -730,6 +735,11 @@ public boolean getFixDeadlocks() return settings.getBoolean(PrismSettings.PRISM_FIX_DEADLOCKS); } + public boolean getSortStates() + { + return settings.getBoolean(PrismSettings.PRISM_SORT_STATES); + } + public boolean getDoProbChecks() { return settings.getBoolean(PrismSettings.PRISM_DO_PROB_CHECKS); @@ -2014,6 +2024,7 @@ private void doBuildModel() throws PrismException } ConstructModel constructModel = new ConstructModel(this); constructModel.setFixDeadlocks(getFixDeadlocks()); + constructModel.setSortStates(getSortStates()); currentModelExpl = constructModel.constructModel(currentModelGenerator); currentModel = null; } @@ -2029,6 +2040,7 @@ private void doBuildModel() throws PrismException } else { ConstructModel constructModel = new ConstructModel(this); constructModel.setFixDeadlocks(getFixDeadlocks()); + constructModel.setSortStates(getSortStates()); currentModelExpl = constructModel.constructModel(currentModelGenerator); currentModel = null; } diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index e3ab7f1358..36db5d0b45 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -79,6 +79,7 @@ public class PrismSettings implements Observer public static final String PRISM_PROB1 = "prism.prob1"; public static final String PRISM_PRE_REL = "prism.preRel"; public static final String PRISM_FIX_DEADLOCKS = "prism.fixDeadlocks"; + public static final String PRISM_SORT_STATES = "prism.sortStates"; public static final String PRISM_DO_PROB_CHECKS = "prism.doProbChecks"; public static final String PRISM_SUM_ROUND_OFF = "prism.sumRoundOff"; public static final String PRISM_COMPACT = "prism.compact"; @@ -278,6 +279,8 @@ public class PrismSettings implements Observer "Constrain to fair adversaries when model checking MDPs." }, { BOOLEAN_TYPE, PRISM_FIX_DEADLOCKS, "Automatically fix deadlocks", "4.0.3", new Boolean(true), "", "Automatically fix deadlocks, where necessary, when constructing probabilistic models." }, + { BOOLEAN_TYPE, PRISM_SORT_STATES, "Sort reachable states", "4.4", new Boolean(true), "", + "Sort the list of reachable states when constructing probabilistic models." }, { 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." }, { DOUBLE_TYPE, PRISM_SUM_ROUND_OFF, "Probability sum threshold", "2.1", new Double(1.0E-5), "0.0,",