diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 6e70d7fc..248a0a76 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -66,6 +66,7 @@ public class PrismCL private boolean simpath = false; private ModelType typeOverride = null; private boolean explicitbuildtest = false; + private boolean nobuild = false; // property info private int propertyToCheck = -1; @@ -267,10 +268,13 @@ public class PrismCL // decide if model construction is necessary boolean doBuild = true; - // e.g. no need if using approximate (simulation-based) model checking + // if explicitly disabled... + if (nobuild) + doBuild = false; + // no need if using approximate (simulation-based) model checking... if (simulate) doBuild = false; - // e.g. no need for PTA model checking (when not using digital clocks) + // no need for PTA model checking (when not using digital clocks)... else if (modulesFile.getModelType() == ModelType.PTA && !prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD).equals("Digital clocks")) doBuild = false; @@ -1081,6 +1085,10 @@ public class PrismCL errorAndExit("No file specified for -" + sw + " switch"); } } + // disable model construction + else if (sw.equals("nobuild")) { + nobuild = true; + } // set scc computation algorithm else if (sw.equals("sccmethod") || sw.equals("bsccmethod")) { if (i < args.length - 1) { @@ -1778,6 +1786,7 @@ public class PrismCL mainLog.println("-exporttransient ........ Export transient probabilities to a file"); mainLog.println("-exportprism ............ Export final PRISM model to a file"); mainLog.println("-exportprismconst ....... Export final PRISM model with expanded constants to a file"); + mainLog.println("-nobuild ....................... Skip model construction (just parse/export)"); mainLog.println(); mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine"); mainLog.println("-sparse (or -s) ................ Use the Sparse engine");