From aeb9102cfcacd3722cf0a0befbd79d4ad9296004 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 12 Feb 2026 08:37:03 +0000 Subject: [PATCH 1/4] PRISM GUI closes Prism down properly, like PrismCL. --- prism/src/userinterface/GUIPrism.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index f43546c444..d80cf85f50 100644 --- a/prism/src/userinterface/GUIPrism.java +++ b/prism/src/userinterface/GUIPrism.java @@ -518,8 +518,12 @@ public void exit() } }*/ - if (doExit) + if (doExit) { + if (prism != null) { + prism.closeDown(true); + } System.exit(0); + } } //ACCESS METHODS From 117f52bd4992b8ae84558c7d6158cdca9eadfedb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 12 Feb 2026 07:19:38 +0000 Subject: [PATCH 2/4] Clean up interface to native code, especially in prism.Prism. Calls to JDD.xx() and PrismNative.xx() are pushed into separate libraries. Currently those libraries are always created but will later be optional. Prism also also now stores a (static) workingDirectory, as set by the -dir switch or when running PRISM in Nailgun mode. There are methods to resolve filenames with respect to this. Currently unused. In fact, setting the working directory currently only works via the native call to change cwd. --- prism/src/jdd/JDD.java | 16 +++- prism/src/jdd/JDDLibrary.java | 82 ++++++++++++++++ prism/src/prism/Prism.java | 122 ++++++++++++++++-------- prism/src/prism/PrismCL.java | 5 +- prism/src/prism/PrismLibrary.java | 59 ++++++++++++ prism/src/prism/PrismNG.java | 6 +- prism/src/prism/PrismNative.java | 5 +- prism/src/prism/PrismNativeLibrary.java | 63 ++++++++++++ prism/src/userinterface/GUIPrism.java | 10 +- 9 files changed, 313 insertions(+), 55 deletions(-) create mode 100644 prism/src/jdd/JDDLibrary.java create mode 100644 prism/src/prism/PrismLibrary.java create mode 100644 prism/src/prism/PrismNativeLibrary.java diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 71eb58aed7..c9ea33298d 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 0000000000..949705fa9c --- /dev/null +++ b/prism/src/jdd/JDDLibrary.java @@ -0,0 +1,82 @@ +//============================================================================== +// +// 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, 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. + 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 b7fa1022bf..f6125fc2dd 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)); } //------------------------------------------------------------------------------ @@ -1244,14 +1294,13 @@ 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()); - - // initialise libraries/engines - PrismNative.initialise(this, mainLog); + // Add/initialise components/libraries + libraries.add(new JDDLibrary()); + libraries.add(new PrismNativeLibrary()); + for (PrismLibrary lib : libraries) { + lib.initialise(this); + } + setMainLog(mainLog); } /** @@ -4211,13 +4260,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 d2042e2081..d4ec8e5640 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/PrismLibrary.java b/prism/src/prism/PrismLibrary.java new file mode 100644 index 0000000000..5dd340e68b --- /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 c91b7c587e..72b6cc5bf4 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 92696daae0..2e796c697a 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/PrismNativeLibrary.java b/prism/src/prism/PrismNativeLibrary.java new file mode 100644 index 0000000000..17b332f595 --- /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/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index d80cf85f50..fb30fdffa8 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); From 17806bdcb1f236509997f50aebc400e3ee3fa9ae Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 15 Feb 2026 16:22:13 +0000 Subject: [PATCH 3/4] Components using native code trigger use of native code for log writing. PrismFileLog now defaults to using non-native code, i.e., PrintStreams, but can be switched cleanly to a native implementation using useNative(). Code using native libraries (mainly symbolic engines) implement new interface PrismNativeComponent, which triggers the switch on creation. --- prism/src/jdd/JDDLibrary.java | 6 ++- prism/src/prism/PrismFileLog.java | 40 +++++++++++++++++- prism/src/prism/PrismNativeComponent.java | 42 +++++++++++++++++++ .../symbolic/build/ExplicitFiles2MTBDD.java | 24 +++-------- .../symbolic/build/ExplicitModel2MTBDD.java | 23 +++------- .../symbolic/build/ModelGenerator2MTBDD.java | 23 +++------- prism/src/symbolic/build/Modules2MTBDD.java | 23 ++++------ .../symbolic/comp/MultiObjModelChecker.java | 24 ++--------- .../src/symbolic/comp/NondetModelChecker.java | 13 +++--- prism/src/symbolic/comp/ProbModelChecker.java | 11 +++-- .../src/symbolic/comp/StateModelChecker.java | 29 +++---------- 11 files changed, 129 insertions(+), 129 deletions(-) create mode 100644 prism/src/prism/PrismNativeComponent.java diff --git a/prism/src/jdd/JDDLibrary.java b/prism/src/jdd/JDDLibrary.java index 949705fa9c..c97c3e85cd 100644 --- a/prism/src/jdd/JDDLibrary.java +++ b/prism/src/jdd/JDDLibrary.java @@ -47,9 +47,13 @@ public void initialise(Prism prism) throws PrismException @Override public void setMainLog(PrismLog mainLog) throws PrismException { - // If possible, pass the (file/stdout) pointer to JDD. + // 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); diff --git a/prism/src/prism/PrismFileLog.java b/prism/src/prism/PrismFileLog.java index 13ad70169a..2b0c0e2ce6 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/PrismNativeComponent.java b/prism/src/prism/PrismNativeComponent.java new file mode 100644 index 0000000000..71fa7e8166 --- /dev/null +++ b/prism/src/prism/PrismNativeComponent.java @@ -0,0 +1,42 @@ +//============================================================================== +// +// 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; + } +} diff --git a/prism/src/symbolic/build/ExplicitFiles2MTBDD.java b/prism/src/symbolic/build/ExplicitFiles2MTBDD.java index 3a925b1224..0ca89ade6e 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 23fd224010..bc93c61ebd 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 10c4b8e43d..c42cc01081 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 6a8399501d..934d3edd66 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 1532714c08..58d7c9a412 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 434a791e91..bdb361f23d 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 fa2d642eb6..1ad4b763df 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 2f1ea907eb..2a1a8b125a 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; From e2b6f506f533bf2fd88e2dcd250af3591a70fe11 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 15 Feb 2026 16:42:47 +0000 Subject: [PATCH 4/4] Native code in Prism only loaded/initialised on demand. Native shared libraries can be absent when using the explicit engine. --- prism/src/prism/Prism.java | 29 ++++++++++++++++++----- prism/src/prism/PrismNativeComponent.java | 2 ++ 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index f6125fc2dd..bfc39220b6 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1293,14 +1293,31 @@ public void initialise() throws PrismException } mainLog.print("Memory limits: cudd=" + getCUDDMaxMem()); mainLog.println(", java(heap)=" + PrismUtils.convertBytesToMemoryString(Runtime.getRuntime().maxMemory())); + } - // Add/initialise components/libraries - libraries.add(new JDDLibrary()); - libraries.add(new PrismNativeLibrary()); - for (PrismLibrary lib : libraries) { - lib.initialise(this); + /** + * 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()); } - setMainLog(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); } /** diff --git a/prism/src/prism/PrismNativeComponent.java b/prism/src/prism/PrismNativeComponent.java index 71fa7e8166..63157ef1b9 100644 --- a/prism/src/prism/PrismNativeComponent.java +++ b/prism/src/prism/PrismNativeComponent.java @@ -38,5 +38,7 @@ public PrismNativeComponent(Prism prism) throws PrismException { super(prism); this.prism = prism; + // Make sure PRISM is set up to use native code. + prism.useNative(); } }