diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 71eb58aed..c9ea33298 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -194,12 +194,22 @@ public static class CuddOutOfMemoryException extends RuntimeException { public static JDDNode MINUS_INFINITY; // wrapper methods for dd - + + /** + * Set the default output stream for DD (native) code. + * This mainly used for printing diagnostic/error messages. + * @param fp C++ file pointer (e.g., to stdout or a file), cast to a long. + */ public static void SetOutputStream(long fp) { DD_SetOutputStream(fp); } - + + /** + * Get the default output stream for DD (native) code. + * This mainly used for printing diagnostic/error messages. + * It is a C++ file pointer (e.g., to stdout or a file), cast to a long. + */ public static long GetOutputStream() { return DD_GetOutputStream(); @@ -1484,7 +1494,7 @@ public static void PrintMinterms(PrismLog log, JDDNode dd) * * @param log the output log * @param dd the MTBDD - * @param name an optional description to be printed ({@code null} for none) + * @param description an optional description to be printed ({@code null} for none) */ public static void PrintMinterms(PrismLog log, JDDNode dd, String description) { diff --git a/prism/src/jdd/JDDLibrary.java b/prism/src/jdd/JDDLibrary.java new file mode 100644 index 000000000..c97c3e85c --- /dev/null +++ b/prism/src/jdd/JDDLibrary.java @@ -0,0 +1,86 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package jdd; + +import prism.*; + +/** + * A {@code PrismLibrary} wrapper around native code in the JDD library. + */ +public class JDDLibrary implements PrismLibrary +{ + /** Has CUDD been initialised? */ + private static boolean cuddInitialised = false; + + @Override + public void initialise(Prism prism) throws PrismException + { + long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(prism.getCUDDMaxMem()); + JDD.InitialiseCUDD(cuddMaxMem, prism.getCUDDEpsilon()); + cuddInitialised = true; + } + + @Override + public void setMainLog(PrismLog mainLog) throws PrismException + { + // If possible, we ensure that the log is using native code + // and pass the (file/stdout) pointer to JDD. + // This is mainly so that diagnostic/error messages from the + // DD native code end up in the same place as the rest of the log output. + if (mainLog instanceof PrismFileLog) { + ((PrismFileLog) mainLog).useNative(); + } + long fp = mainLog.getFilePointer(); + if (fp > 0) { + JDD.SetOutputStream(fp); + } + } + + @Override + public void notifySettings(PrismSettings settings) + { + if (cuddInitialised) { + JDD.SetCUDDEpsilon(settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON)); + try { + long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(settings.getString(PrismSettings.PRISM_CUDD_MAX_MEM)); + JDD.SetCUDDMaxMem(cuddMaxMem); + } catch (PrismException e) { + // Fail silently if memory string is invalid + } + jdd.SanityJDD.enabled = settings.getBoolean(PrismSettings.PRISM_JDD_SANITY_CHECKS); + } + } + + @Override + public void closeDown(boolean check) + { + if (cuddInitialised) { + JDD.CloseDownCUDD(check); + cuddInitialised = false; + } + } +} diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index b7fa1022b..bfc39220b 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -30,12 +30,14 @@ import java.io.File; import java.io.FileInputStream; import java.io.FileNotFoundException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; import java.util.ArrayList; import java.util.List; import java.util.regex.Pattern; import common.iterable.Range; -import dv.DoubleVector; import explicit.CTMC; import explicit.CTMCModelChecker; import explicit.ConstructModel; @@ -46,17 +48,15 @@ import explicit.FastAdaptiveUniformisation; import explicit.FastAdaptiveUniformisationModelChecker; import explicit.ModelModelGenerator; -import hybrid.PrismHybrid; import io.UMBImporter; import io.ExplicitModelImporter; import io.ModelExportOptions; import io.ModelExportTask; import io.ModelExportFormat; import jdd.JDD; +import jdd.JDDLibrary; import jdd.JDDNode; import jdd.JDDVars; -import mtbdd.PrismMTBDD; -import odd.ODDUtils; import param.ParamMode; import param.ParamModelChecker; import parser.PrismParser; @@ -74,7 +74,6 @@ import simulator.ModulesFileModelGenerator; import simulator.SimulatorEngine; import simulator.method.SimulationMethod; -import sparse.PrismSparse; import strat.Strategy; import strat.StrategyExportOptions; import strat.StrategyExportOptions.StrategyExportType; @@ -224,6 +223,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Parsers/translators/model checkers/simulators/etc. //------------------------------------------------------------------------------ + private final List libraries = new ArrayList<>(); private static PrismParser thePrismParser = null; private static boolean prismParserInUse = false; private SimulatorEngine theSimulator = null; @@ -241,6 +241,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener // State //------------------------------------------------------------------------------ + /** + * Working directory for resolving files (null = current working directory). + * Since this is used by native shared libraries, and to ease access from other code, it is static. + */ + private static Path workingDirectory = null; + public enum ModelSource { PRISM_MODEL, MODEL_GENERATOR, EXPLICIT_FILES, BUILT_MODEL; public String description() @@ -369,9 +375,6 @@ public class ModelDetails private String[] paramLowerBounds; private String[] paramUpperBounds; - // Has the CUDD library been initialised yet? - private boolean cuddStarted = false; - // Info about automatic engine switching private int engineOld = -1; private boolean engineSwitched = false; @@ -431,18 +434,73 @@ public void loadUserSettingsFile(File settingsFile) } } + // Working directory + + /** + * Set the working directory, with respect to which filenames for reading/writing + * will be resolved. If set to null, the existing current working directory is used. + * If set, this should be called before {@link #initialise()} so that it is + * passed to any other libraries that are initialised. + * + * @param dirname Name of working directory (null = current working directory) + */ + public static void setWorkingDirectory(String dirname) throws PrismException + { + if (dirname == null) { + workingDirectory = null; + return; + } + Path wd = Paths.get(dirname); + if (!Files.isDirectory(wd)) { + throw new PrismException("Working directory \"" + dirname + "\" is not a directory"); + } + if (!Files.isReadable(wd)) { + throw new PrismException("Working directory \"" + dirname + "\" is not readable"); + } + if (!Files.isWritable(wd)) { + throw new PrismException("Working directory \"" + dirname + "\" is not writeable"); + } + workingDirectory = wd; + } + + /** + * Get the working directory, with respect to which filenames for reading/writing + * will be resolved. If set to null, the existing current working directory is used. + */ + public static Path getWorkingDirectory() + { + return workingDirectory; + } + + /** + * Resolve a filename. If relative, it will be resolved with respect to + * {@link #getWorkingDirectory()} (or the current working directory if that is null). + */ + public static File resolveFile(String filename) + { + return resolveFile(new File(filename)); + } + + /** + * Resolve a filename. If relative, it will be resolved with respect to + * {@link #getWorkingDirectory()} (or the current working directory if that is null). + */ + public static File resolveFile(File file) + { + return workingDirectory == null ? file : workingDirectory.resolve(file.toPath()).toFile(); + } + // Set methods /** * Set the PrismLog where messages and model checking output will be sent. */ - public void setMainLog(PrismLog l) + public void setMainLog(PrismLog mainLog) throws PrismException { - // store new log - mainLog = l; - // pass to other components - JDD.SetOutputStream(mainLog.getFilePointer()); - PrismNative.setMainLog(mainLog); + super.setLog(mainLog); + for (PrismLibrary lib : libraries) { + lib.setMainLog(mainLog); + } } // Set methods for main prism settings @@ -1090,17 +1148,9 @@ public static String getEngineString(int engine) */ public void notifySettings(PrismSettings settings) { - if (cuddStarted) { - JDD.SetCUDDEpsilon(settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON)); - try { - long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(getCUDDMaxMem()); - JDD.SetCUDDMaxMem(cuddMaxMem); - } catch (PrismException e) { - // Fail silently if memory string is invalid - } + for (PrismLibrary lib : libraries) { + lib.notifySettings(settings); } - jdd.SanityJDD.enabled = settings.getBoolean(PrismSettings.PRISM_JDD_SANITY_CHECKS); - PrismNative.SetExportIterations(settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)); } //------------------------------------------------------------------------------ @@ -1243,15 +1293,31 @@ public void initialise() throws PrismException } mainLog.print("Memory limits: cudd=" + getCUDDMaxMem()); mainLog.println(", java(heap)=" + PrismUtils.convertBytesToMemoryString(Runtime.getRuntime().maxMemory())); + } - // initialise cudd/jdd - long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(getCUDDMaxMem()); - JDD.InitialiseCUDD(cuddMaxMem, getCUDDEpsilon()); - cuddStarted = true; - JDD.SetOutputStream(mainLog.getFilePointer()); + /** + * Ensure that the native libraries are loaded and initialised, + * and that any relevant settings are passed to them. + */ + public void useNative() throws PrismException + { + // Add/initialise libraries for native code, if not already done + if (libraries.stream().noneMatch(JDDLibrary.class::isInstance)) { + addLibrary(new JDDLibrary()); + } + if (libraries.stream().noneMatch(PrismNativeLibrary.class::isInstance)) { + addLibrary(new PrismNativeLibrary()); + } + } - // initialise libraries/engines - PrismNative.initialise(this, mainLog); + /** + * Initialise a freshy created {@link PrismLibrary} and add to the list of libraries. + */ + private void addLibrary(PrismLibrary lib) throws PrismException + { + lib.initialise(this); + lib.setMainLog(mainLog); + libraries.add(lib); } /** @@ -4211,13 +4277,10 @@ public void closeDown(boolean check) // Clear any built model(s) clearBuiltModel(); // Close down libraries/engines - PrismNative.closeDown(); ParamModelChecker.closeDown(); - // Close down CUDD/JDD - if (cuddStarted) { - JDD.CloseDownCUDD(check); - // reset CUDD status - cuddStarted = false; + int numLibs = libraries.size(); + for (int i = numLibs - 1; i >= 0; i--) { + libraries.get(i).closeDown(check); } } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index d2042e208..d4ec8e564 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1117,10 +1117,7 @@ else if (sw.equals("version")) { // set working directory else if (sw.equals("dir")) { if (i < args.length - 1) { - String workingDir = args[++i]; - if (PrismNative.setWorkingDirectory(workingDir) != 0) { - errorAndExit("Could not change working directory to " + workingDir); - } + Prism.setWorkingDirectory(args[++i]); } else { errorAndExit("No property specified for -" + sw + " switch"); } diff --git a/prism/src/prism/PrismFileLog.java b/prism/src/prism/PrismFileLog.java index 13ad70169..2b0c0e2ce 100644 --- a/prism/src/prism/PrismFileLog.java +++ b/prism/src/prism/PrismFileLog.java @@ -40,6 +40,8 @@ public class PrismFileLog extends PrismPrintStreamLog protected String filename; /** Are we writing to stdout? */ protected boolean stdout; + /** Are we using native code to write to the file? */ + protected boolean nativeCode; /** * Create a {@link PrismLog} which will write to {@code filename}, overwriting any previous contents. @@ -61,7 +63,7 @@ public PrismFileLog(String filename) throws PrismException */ public PrismFileLog(String filename, boolean append) throws PrismException { - this(filename, append, true); + this(filename, append, false); } /** @@ -87,6 +89,7 @@ private void createLogStream(String filename, boolean append, boolean nativeCode { this.filename = filename; this.stdout = "stdout".equals(filename); + this.nativeCode = nativeCode; try { if (nativeCode) { setPrintStream(new PrismFileLogNative(filename, append)); @@ -102,6 +105,20 @@ private void createLogStream(String filename, boolean append, boolean nativeCode } } + /** + * Ensure the log is using native code to write to the file. + * If this is currently not the case, this method will {@code close()} + * the current log and open a new equivalent one using native code. + * Throw a PRISM exception if there is a problem opening the file for writing. + */ + public void useNative() throws PrismException + { + if (!nativeCode) { + close(); + createLogStream(filename, true, true); + } + } + /** * Get the filename (or "stdout" if writing to standard output) **/ @@ -110,6 +127,14 @@ public String getFileName() return stdout ? "stdout" : filename; } + /** + * Is this log using native code to write to the file? + */ + public boolean isNative() + { + return nativeCode; + } + // Methods for PrismLog @Override @@ -161,6 +186,19 @@ public static PrismFileLog create(String filename, boolean append) throws PrismE return new PrismFileLog(filename, append); } + /** + * Create a {@link PrismLog} which will write to {@code filename}, appending to an existing file if requested. + * If {@code filename} is "stdout", then output will be written to standard output. + * Throw a PRISM exception if there is a problem opening the file for writing. + * @param filename Filename of log file + * @param append Append to the existing file? + * @param nativeCode Use native code to write to the file? + */ + public static PrismFileLog create(String filename, boolean append, boolean nativeCode) throws PrismException + { + return new PrismFileLog(filename, append, nativeCode); + } + /** * Create a {@link PrismLog} which will write to standard output. */ diff --git a/prism/src/prism/PrismLibrary.java b/prism/src/prism/PrismLibrary.java new file mode 100644 index 000000000..5dd340e68 --- /dev/null +++ b/prism/src/prism/PrismLibrary.java @@ -0,0 +1,59 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +/** + * Interface for libraries that can be loaded and used by PRISM. + * Currently, this is mainly used to provide a clean way for + * native code to be detached from the main Prism class. + */ +public interface PrismLibrary +{ + /** + * Initialise the library. + * @param prism The main Prism object + */ + void initialise(Prism prism) throws PrismException; + + /** + * Set the main log for the library to use. + * @param mainLog The log + */ + void setMainLog(PrismLog mainLog) throws PrismException; + + /** + * Notify the library of changes to PRISM settings. + * @param settings The new settings + */ + void notifySettings(PrismSettings settings); + + /** + * Close down the library, tidying up any resources. + * @param check Do additional checks to make sure close down was clean? + */ + void closeDown(boolean check); +} diff --git a/prism/src/prism/PrismNG.java b/prism/src/prism/PrismNG.java index c91b7c587..72b6cc5bf 100644 --- a/prism/src/prism/PrismNG.java +++ b/prism/src/prism/PrismNG.java @@ -64,8 +64,10 @@ public class PrismNG public synchronized static void nailMain(NGContext context) throws InterruptedException { currentNailGunContext = context; - if (PrismNative.setWorkingDirectory(context.getWorkingDirectory()) != 0) { - System.err.println("Nailgun: Can not change working directory to " + context.getWorkingDirectory()); + try { + Prism.setWorkingDirectory(context.getWorkingDirectory()); + } catch (PrismException ex) { + System.err.println("Nailgun: " + ex.getMessage()); System.exit(1); } diff --git a/prism/src/prism/PrismNative.java b/prism/src/prism/PrismNative.java index 92696daae..2e796c697 100644 --- a/prism/src/prism/PrismNative.java +++ b/prism/src/prism/PrismNative.java @@ -45,14 +45,13 @@ public class PrismNative System.exit(1); } } - + // Initialise/close down methods - public static void initialise(Prism prism, PrismLog mainLog) + public static void initialise(Prism prism) { setPrism(prism); setCUDDManager(); - setMainLog(mainLog); } public static void closeDown() diff --git a/prism/src/prism/PrismNativeComponent.java b/prism/src/prism/PrismNativeComponent.java new file mode 100644 index 000000000..63157ef1b --- /dev/null +++ b/prism/src/prism/PrismNativeComponent.java @@ -0,0 +1,44 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +/** + * Base class for {@link PrismComponent}s that use native code. + */ +public class PrismNativeComponent extends PrismComponent +{ + /* Reference to the parent Prism instance. */ + protected Prism prism; + + public PrismNativeComponent(Prism prism) throws PrismException + { + super(prism); + this.prism = prism; + // Make sure PRISM is set up to use native code. + prism.useNative(); + } +} diff --git a/prism/src/prism/PrismNativeLibrary.java b/prism/src/prism/PrismNativeLibrary.java new file mode 100644 index 000000000..17b332f59 --- /dev/null +++ b/prism/src/prism/PrismNativeLibrary.java @@ -0,0 +1,63 @@ +//============================================================================== +// +// Copyright (c) 2026- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.nio.file.Path; + +/** + * A {@code PrismLibrary} wrapper around native code in the "prism" shared library. + */ +public class PrismNativeLibrary implements PrismLibrary +{ + @Override + public void initialise(Prism prism) throws PrismException + { + Path workingDirectory = Prism.getWorkingDirectory(); + if (workingDirectory != null) { + PrismNative.setWorkingDirectory(workingDirectory.toString()); + } + PrismNative.initialise(prism); + } + + @Override + public void setMainLog(PrismLog mainLog) throws PrismException + { + PrismNative.setMainLog(mainLog); + } + + @Override + public void notifySettings(PrismSettings settings) + { + PrismNative.SetExportIterations(settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)); + } + + @Override + public void closeDown(boolean check) + { + PrismNative.closeDown(); + } +} diff --git a/prism/src/symbolic/build/ExplicitFiles2MTBDD.java b/prism/src/symbolic/build/ExplicitFiles2MTBDD.java index 3a925b122..0ca89ade6 100644 --- a/prism/src/symbolic/build/ExplicitFiles2MTBDD.java +++ b/prism/src/symbolic/build/ExplicitFiles2MTBDD.java @@ -38,16 +38,7 @@ import parser.Values; import parser.VarList; import parser.ast.DeclarationType; -import prism.Evaluator; -import prism.ModelInfo; -import prism.ModelType; -import prism.Prism; -import prism.PrismException; -import prism.PrismLog; -import prism.PrismNotSupportedException; -import prism.PrismSettings; -import prism.ProgressDisplay; -import prism.RewardInfo; +import prism.*; import symbolic.model.Model; import symbolic.model.ModelSymbolic; import symbolic.model.ModelVariablesDD; @@ -58,12 +49,8 @@ /** * Class to convert explicit-state file storage of a model to symbolic representation. */ -public class ExplicitFiles2MTBDD +public class ExplicitFiles2MTBDD extends PrismNativeComponent { - // Prism stuff - private Prism prism; - private PrismLog mainLog; - // Importer / files to read in from private ExplicitModelImporter importer; @@ -112,10 +99,9 @@ public class ExplicitFiles2MTBDD private ProgressDisplay progress; private int transitionsImported; - public ExplicitFiles2MTBDD(Prism prism) + public ExplicitFiles2MTBDD(Prism prism) throws PrismException { - this.prism = prism; - mainLog = prism.getMainLog(); + super(prism); } /** @@ -290,7 +276,7 @@ private void allocateDDVars() throws PrismException modelVariables = new ModelVariablesDD(); - modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); + modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); // create arrays/etc. first diff --git a/prism/src/symbolic/build/ExplicitModel2MTBDD.java b/prism/src/symbolic/build/ExplicitModel2MTBDD.java index 23fd22401..bc93c61eb 100644 --- a/prism/src/symbolic/build/ExplicitModel2MTBDD.java +++ b/prism/src/symbolic/build/ExplicitModel2MTBDD.java @@ -32,13 +32,7 @@ import parser.*; import parser.ast.*; import explicit.*; -import prism.ModelType; -import prism.Prism; -import prism.PrismException; -import prism.PrismLangException; -import prism.PrismLog; -import prism.PrismSettings; -import prism.ProgressDisplay; +import prism.*; import symbolic.model.ModelVariablesDD; import symbolic.model.ProbModel; import symbolic.model.StochModel; @@ -46,14 +40,8 @@ /** * Class to convert explicit-state representation of a model to a symbolic one. */ -public class ExplicitModel2MTBDD +public class ExplicitModel2MTBDD extends PrismNativeComponent { - // prism - private Prism prism; - - // logs - private PrismLog mainLog; // main log - // Explicit-state model private explicit.Model modelExpl; @@ -96,10 +84,9 @@ public class ExplicitModel2MTBDD // constructor - public ExplicitModel2MTBDD(Prism prism) + public ExplicitModel2MTBDD(Prism prism) throws PrismException { - this.prism = prism; - mainLog = prism.getMainLog(); + super(prism); } // Build model @@ -249,7 +236,7 @@ private void allocateDDVars() modelVariables = new ModelVariablesDD(); - modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); + modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); // create arrays/etc. first diff --git a/prism/src/symbolic/build/ModelGenerator2MTBDD.java b/prism/src/symbolic/build/ModelGenerator2MTBDD.java index 10c4b8e43..c42cc0108 100644 --- a/prism/src/symbolic/build/ModelGenerator2MTBDD.java +++ b/prism/src/symbolic/build/ModelGenerator2MTBDD.java @@ -38,15 +38,7 @@ import parser.ast.DeclarationClock; import parser.ast.DeclarationIntUnbounded; import parser.ast.DeclarationType; -import prism.ModelGenerator; -import prism.ModelType; -import prism.Prism; -import prism.PrismException; -import prism.PrismLangException; -import prism.PrismLog; -import prism.PrismNotSupportedException; -import prism.PrismSettings; -import prism.RewardGenerator; +import prism.*; import symbolic.model.Model; import symbolic.model.ModelSymbolic; import symbolic.model.ModelVariablesDD; @@ -57,12 +49,8 @@ /** * Class to construct a symbolic representation from a ModelGenerator object. */ -public class ModelGenerator2MTBDD +public class ModelGenerator2MTBDD extends PrismNativeComponent { - // Prism stuff - private Prism prism; - private PrismLog mainLog; - // Source model generators private ModelGenerator modelGen; private RewardGenerator rewardGen; @@ -102,10 +90,9 @@ public class ModelGenerator2MTBDD private int maxNumChoices = 0; - public ModelGenerator2MTBDD(Prism prism) + public ModelGenerator2MTBDD(Prism prism) throws PrismException { - this.prism = prism; - mainLog = prism.getMainLog(); + super(prism); } /** @@ -228,7 +215,7 @@ private void allocateDDVars() throws PrismException JDDNode vr, vc; int i, j, n; - modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); + modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); // create arrays/etc. first diff --git a/prism/src/symbolic/build/Modules2MTBDD.java b/prism/src/symbolic/build/Modules2MTBDD.java index 6a8399501..934d3edd6 100644 --- a/prism/src/symbolic/build/Modules2MTBDD.java +++ b/prism/src/symbolic/build/Modules2MTBDD.java @@ -45,17 +45,11 @@ // class to translate a modules description file into an MTBDD model -public class Modules2MTBDD +public class Modules2MTBDD extends PrismNativeComponent { - // Prism object - private Prism prism; - // StateModelChecker for expression -> MTBDD conversion private StateModelChecker expr2mtbdd; - // logs - private PrismLog mainLog; // main log - // ModulesFile object to store syntax tree from parser private ModulesFile modulesFile; @@ -232,13 +226,12 @@ public SystemDDs(int n) // constructor - public Modules2MTBDD(Prism p, ModulesFile mf) + public Modules2MTBDD(Prism prism, ModulesFile mf) throws PrismException { - prism = p; - mainLog = p.getMainLog(); + super(prism); modulesFile = mf; // get symmetry reduction info - String s = prism.getSettings().getString(PrismSettings.PRISM_SYMM_RED_PARAMS); + String s = settings.getString(PrismSettings.PRISM_SYMM_RED_PARAMS); doSymmetry = !(s == null || s == ""); } @@ -482,7 +475,7 @@ private void allocateDDVars() case 1: // ordering: (a ... a) (s ... s) (l ... l) (r c ... r c) - modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); + modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); // create arrays/etc. first @@ -538,7 +531,7 @@ private void allocateDDVars() // create a gap in the dd variables // this allows to prepend additional row/col vars, e.g. for constructing // a product model when doing LTL model checking - modelVariables.preallocateExtraStateVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_STATE_VARS)); + modelVariables.preallocateExtraStateVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_STATE_VARS)); // allocate dd variables for module variables (i.e. rows/cols) @@ -562,7 +555,7 @@ private void allocateDDVars() case 2: // ordering: (a ... a) (l ... l) (s r c ... r c) (s r c ... r c) ... - modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); + modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS)); // create arrays/etc. first @@ -2216,7 +2209,7 @@ private void doSymmetry(ModelSymbolic model) throws PrismException String ss[]; // parse symmetry reduction parameters - ss = prism.getSettings().getString(PrismSettings.PRISM_SYMM_RED_PARAMS).split(" "); + ss = settings.getString(PrismSettings.PRISM_SYMM_RED_PARAMS).split(" "); if (ss.length != 2) throw new PrismException ("Invalid parameters for symmetry reduction"); try { numModulesBeforeSymm = Integer.parseInt(ss[0].trim()); diff --git a/prism/src/symbolic/comp/MultiObjModelChecker.java b/prism/src/symbolic/comp/MultiObjModelChecker.java index 1532714c0..58d7c9a41 100644 --- a/prism/src/symbolic/comp/MultiObjModelChecker.java +++ b/prism/src/symbolic/comp/MultiObjModelChecker.java @@ -42,21 +42,7 @@ import mtbdd.PrismMTBDD; import parser.ast.Expression; import parser.ast.RelOp; -import prism.MultiObjUtils; -import prism.NativeIntArray; -import prism.OpRelOpBound; -import prism.Operator; -import prism.OpsAndBoundsList; -import prism.Point; -import prism.Prism; -import prism.PrismComponent; -import prism.PrismException; -import prism.PrismNative; -import prism.PrismNotSupportedException; -import prism.PrismSettings; -import prism.PrismUtils; -import prism.Tile; -import prism.TileList; +import prism.*; import sparse.NDSparseMatrix; import sparse.PrismSparse; import acceptance.AcceptanceRabin; @@ -68,18 +54,16 @@ /** * Multi-objective model checking functionality */ -public class MultiObjModelChecker extends PrismComponent +public class MultiObjModelChecker extends PrismNativeComponent { - protected Prism prism; protected boolean verbose; /** * Create a new MultiObjModelChecker, inherit basic state from parent (unless null). */ - public MultiObjModelChecker(PrismComponent parent, Prism prism) throws PrismException + public MultiObjModelChecker(Prism prism) throws PrismException { - super(parent); - this.prism = prism; + super(prism); this.verbose = settings.getBoolean(PrismSettings.PRISM_VERBOSE); } diff --git a/prism/src/symbolic/comp/NondetModelChecker.java b/prism/src/symbolic/comp/NondetModelChecker.java index 434a791e9..bdb361f23 100644 --- a/prism/src/symbolic/comp/NondetModelChecker.java +++ b/prism/src/symbolic/comp/NondetModelChecker.java @@ -572,7 +572,7 @@ protected StateValues checkExpressionMultiObjective(List exprs, JDDN // For LTL/multi-obj model checking routines mcLtl = new LTLModelChecker(prism); - mcMo = new MultiObjModelChecker(prism, prism); + mcMo = new MultiObjModelChecker(prism); // Product is initially just the original model (we build it recursively) modelProduct = model; @@ -925,8 +925,7 @@ protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolea // and whether we want to use the corresponding algorithms boolean useSimplePathAlgo = expr.isSimplePathFormula(); - if (useSimplePathAlgo && - prism.getSettings().getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA) && + if (useSimplePathAlgo && settings.getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA) && LTLModelChecker.isSupportedLTLFormula(model.getModelType(), expr)) { // If PRISM_PATH_VIA_AUTOMATA is true, we want to use the LTL engine // whenever possible @@ -1553,10 +1552,10 @@ protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards da = mcLtl.constructDFAForCosafetyRewardLTL(this, model, expr, labelDDs); // If required, export DA - if (prism.getSettings().getExportPropAut()) { - mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); - da.print(out, prism.getSettings().getExportPropAutType()); + if (settings.getExportPropAut()) { + mainLog.println("Exporting DA to file \"" + settings.getExportPropAutFilename() + "\"..."); + PrintStream out = PrismUtils.newPrintStream(settings.getExportPropAutFilename()); + da.print(out, settings.getExportPropAutType()); out.close(); //da.printDot(new java.io.PrintStream("da.dot")); } diff --git a/prism/src/symbolic/comp/ProbModelChecker.java b/prism/src/symbolic/comp/ProbModelChecker.java index fa2d642eb..1ad4b763d 100644 --- a/prism/src/symbolic/comp/ProbModelChecker.java +++ b/prism/src/symbolic/comp/ProbModelChecker.java @@ -495,8 +495,7 @@ protected StateValues checkProbPathFormula(Expression expr, boolean qual, JDDNod // and whether we want to use the corresponding algorithms boolean useSimplePathAlgo = expr.isSimplePathFormula(); - if (useSimplePathAlgo && - prism.getSettings().getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA) && + if (useSimplePathAlgo && settings.getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA) && LTLModelChecker.isSupportedLTLFormula(model.getModelType(), expr)) { // If PRISM_PATH_VIA_AUTOMATA is true, we want to use the LTL engine // whenever possible @@ -1019,10 +1018,10 @@ protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards DA da = mcLtl.constructDFAForCosafetyRewardLTL(this, model, expr, labelDDs); // If required, export DA - if (prism.getSettings().getExportPropAut()) { - mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); - da.print(out, prism.getSettings().getExportPropAutType()); + if (settings.getExportPropAut()) { + mainLog.println("Exporting DA to file \"" + settings.getExportPropAutFilename() + "\"..."); + PrintStream out = PrismUtils.newPrintStream(settings.getExportPropAutFilename()); + da.print(out, settings.getExportPropAutType()); out.close(); //da.printDot(new java.io.PrintStream("da.dot")); } diff --git a/prism/src/symbolic/comp/StateModelChecker.java b/prism/src/symbolic/comp/StateModelChecker.java index 2f1ea907e..2a1a8b125 100644 --- a/prism/src/symbolic/comp/StateModelChecker.java +++ b/prism/src/symbolic/comp/StateModelChecker.java @@ -46,18 +46,8 @@ import parser.ast.ExpressionFilter.FilterOperator; import parser.type.*; import parser.visitor.ReplaceLabels; -import prism.Accuracy; +import prism.*; import prism.Filter; -import prism.ModelType; -import prism.Prism; -import prism.PrismComponent; -import prism.PrismException; -import prism.PrismLangException; -import prism.PrismLog; -import prism.PrismNotSupportedException; -import prism.PrismSettings; -import prism.PrismUtils; -import prism.Result; import symbolic.model.ModelSymbolic; import symbolic.model.NondetModel; import symbolic.states.StateListMTBDD; @@ -70,11 +60,8 @@ // Base class for model checkers - does state-based evaluations (no temporal/probabilistic) -public class StateModelChecker extends PrismComponent implements ModelChecker +public class StateModelChecker extends PrismNativeComponent implements ModelChecker { - // PRISM stuff - protected Prism prism; - // Properties file protected PropertiesFile propertiesFile; @@ -119,11 +106,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker public StateModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismException { - // Initialise PrismComponent - super(prism); - // Initialise - this.prism = prism; + super(prism); model = m; propertiesFile = pf; constantValues = new Values(); @@ -147,7 +131,7 @@ public StateModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismEx // Store locally and/or pass onto engines engine = prism.getEngine(); termCritParam = prism.getTermCritParam(); - doIntervalIteration = prism.getSettings().getBoolean(PrismSettings.PRISM_INTERVAL_ITER); + doIntervalIteration = settings.getBoolean(PrismSettings.PRISM_INTERVAL_ITER); verbose = prism.getVerbose(); storeVector = prism.getStoreVector(); genStrat = prism.getGenStrat(); @@ -163,11 +147,8 @@ public StateModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismEx */ public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException { - // Initialise PrismComponent - super(prism); - // Initialise - this.prism = prism; + super(prism); this.varList = varList; this.allDDRowVars = allDDRowVars; this.varDDRowVars = varDDRowVars; diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index f43546c44..fb30fdffa 100644 --- a/prism/src/userinterface/GUIPrism.java +++ b/prism/src/userinterface/GUIPrism.java @@ -436,15 +436,15 @@ public String[] processCLArgs(String args[]) } else if (sw.equals("dir")) { if (i < args.length - 1) { String workingDir = args[++i]; - // set working dir natively for PRISM stuff - if (PrismNative.setWorkingDirectory(workingDir) != 0) { - System.err.println("Error: Could not change working directory to " + workingDir); + // set working dir for PRISM + try { + Prism.setWorkingDirectory(workingDir); + } catch (PrismException ex) { + System.err.println("Error: " + ex.getMessage()); System.exit(1); } // also store locally to initialise file chooser chooserDir = workingDir; - // NB: we avoid setting system property "user.dir" - // since this may break loading of shared libraries etc. } else { System.err.println("Error: No value specified for -" + sw + " switch"); System.exit(1); @@ -518,8 +518,12 @@ public void exit() } }*/ - if (doExit) + if (doExit) { + if (prism != null) { + prism.closeDown(true); + } System.exit(0); + } } //ACCESS METHODS