New default for CUDD max memory (1GB) and more flexible usage of that setting: allow memory in format 125k, 50m, 4g, etc.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10028 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/Prism.java

@@ -461,9 +461,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		settings.set(PrismSettings.PRISM_MAX_ITERS, i);
 	}
 
-	public void setCUDDMaxMem(int i) throws PrismException
+	public void setCUDDMaxMem(String s) throws PrismException
 	{
-		settings.set(PrismSettings.PRISM_CUDD_MAX_MEM, i);
+		settings.set(PrismSettings.PRISM_CUDD_MAX_MEM, s);
 	}
 
 	public void setCUDDEpsilon(double d) throws PrismException
@@ -821,9 +821,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		return settings.getBoolean(PrismSettings.PRISM_COMPACT);
 	}
 
-	public long getCUDDMaxMem()
+	public String getCUDDMaxMem()
 	{
-		return settings.getInteger(PrismSettings.PRISM_CUDD_MAX_MEM);
+		return settings.getString(PrismSettings.PRISM_CUDD_MAX_MEM);
 	}
 
 	public double getCUDDEpsilon()
@@ -971,7 +971,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	{
 		if (cuddStarted) {
 			JDD.SetCUDDEpsilon(settings.getDouble(PrismSettings.PRISM_CUDD_EPSILON));
-			JDD.SetCUDDMaxMem(settings.getInteger(PrismSettings.PRISM_CUDD_MAX_MEM));
+			try {
+				long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(getCUDDMaxMem());
+				JDD.SetCUDDMaxMem(cuddMaxMem);
+			} catch (PrismException e) {
+				// Fail silently if memory string is invalid 
+			}
 		}
 	}
 
@@ -1289,7 +1294,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		}
 
 		// initialise cudd/jdd
-		JDD.InitialiseCUDD(getCUDDMaxMem(), getCUDDEpsilon());
+		long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(getCUDDMaxMem());
+		JDD.InitialiseCUDD(cuddMaxMem, getCUDDEpsilon());
 		cuddStarted = true;
 		JDD.SetOutputStream(techLog.getFilePointer());
 

prism/src/prism/PrismSettings.java

@@ -289,8 +289,8 @@ public class PrismSettings implements Observer
 																			"Number of MTBDD levels descended for hybrid engine data structures block division with GS/SOR." },
 			{ INTEGER_TYPE,		PRISM_SOR_MAX_MEM,						"Hybrid GS memory (KB)",				"2.1",			new Integer(1024),															"0,",																						
 																			"Maximum memory usage for hybrid engine data structures block division with GS/SOR (KB)." },
-			{ INTEGER_TYPE,		PRISM_CUDD_MAX_MEM,						"CUDD max. memory (KB)",				"2.1",			new Integer(409600),														"0,",																						
-																			"Maximum memory available to CUDD (underlying BDD/MTBDD library) in KB (Note: Restart PRISM after changing this.)" },
+			{ STRING_TYPE,		PRISM_CUDD_MAX_MEM,						"CUDD max. memory (KB)",				"4.2.1",			new String("1g"),														"",																						
+																			"Maximum memory available to CUDD (underlying BDD/MTBDD library), e.g. 125k, 50m, 4g. Note: Restart PRISM after changing this." },
 			{ DOUBLE_TYPE,		PRISM_CUDD_EPSILON,						"CUDD epsilon",							"2.1",			new Double(1.0E-15),														"0.0,",																						
 																			"Epsilon value used by CUDD (underlying BDD/MTBDD library) for terminal cache comparisons." },
 			// ADVERSARIES/COUNTEREXAMPLES:
@@ -1215,14 +1215,7 @@ public class PrismSettings implements Observer
 		// CUDD settings
 		else if (sw.equals("cuddmaxmem")) {
 			if (i < args.length - 1) {
-				try {
-					j = Integer.parseInt(args[++i]);
-					if (j < 0)
-						throw new NumberFormatException();
-					set(PRISM_CUDD_MAX_MEM, j);
-				} catch (NumberFormatException e) {
-					throw new PrismException("Invalid value for -" + sw + " switch");
-				}
+				set(PRISM_CUDD_MAX_MEM, args[++i]);
 			} else {
 				throw new PrismException("No value specified for -" + sw + " switch");
 			}
@@ -1587,7 +1580,7 @@ public class PrismSettings implements Observer
 		mainLog.println("-sbmax <n> ..................... Set memory limit (KB) (for hybrid engine) [default: 1024]");
 		mainLog.println("-gsl <n> (or sorl <n>) ......... Set number of levels for hybrid GS/SOR [default: -1]");
 		mainLog.println("-gsmax <n> (or sormax <n>) ..... Set memory limit (KB) for hybrid GS/SOR [default: 1024]");
-		mainLog.println("-cuddmaxmem <n> ................ Set max memory for CUDD package (KB) [default: 200x1024]");
+		mainLog.println("-cuddmaxmem <n> ................ Set max memory for CUDD package, e.g. 125k, 50m, 4g [default: 1g]");
 		mainLog.println("-cuddepsilon <x> ............... Set epsilon value for CUDD package [default: 1e-15]");
 		mainLog.println();
 		mainLog.println("PARAMETRIC MODEL CHECKING OPTIONS:");

prism/src/prism/PrismUtils.java

@@ -29,6 +29,8 @@ package prism;
 import java.text.DecimalFormat;
 import java.util.List;
 import java.util.Locale;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
 /**
  * Various general-purpose utility methods in Java
@@ -283,6 +285,37 @@ public class PrismUtils
 		}
 		return firstCycle;
 	}
+
+	/**
+	 * Convert a string representing an amount of memory (e.g. 125k, 50m, 4g) to the value in KB.
+	 * If the letter prefix is omitted, we assume it is "k" (i.e. KB).
+	 */
+	public static long convertMemoryStringtoKB(String mem) throws PrismException
+	{
+		Pattern p = Pattern.compile("([0-9]+)([kmg]?)");
+		Matcher m = p.matcher(mem);
+		if (!m.matches()) {
+			throw new PrismException("Invalid amount of memory \"" + mem + "\"");
+		}
+		long num;
+		try {
+			num = Long.parseLong(m.group(1));
+		} catch (NumberFormatException e) {
+			throw new PrismException("Invalid amount of memory \"" + mem + "\"");
+		}
+		switch (m.group(2)) {
+		case "":
+		case "k":
+			return num;
+		case "m":
+			return num * 1024;
+		case "g":
+			return num * (1024 * 1024);
+		default:
+			// Shouldn't happen
+			throw new PrismException("Invalid amount of memory \"" + mem + "\"");
+		}
+	}
 }
 
 //------------------------------------------------------------------------------