Cleaner separation of native code

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)
 	{

prism/src/jdd/JDDLibrary.java

@@ -0,0 +1,86 @@
+//==============================================================================
+//
+//	Copyright (c) 2026-
+//	Authors:
+//	* Dave Parker <david.parker@cs.ox.ac.uk> (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;
+        }
+    }
+}

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<PrismLibrary> 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);
 		}
 	}
 

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");
 					}