Refactor timeout: conversion in PrismUtils, now additionally supports days (d) and weeks (w) for long-term model checking

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

prism/src/prism/PrismCL.java

@@ -31,7 +31,6 @@ import java.io.FileNotFoundException;
 import java.net.UnknownHostException;
 import java.util.ArrayList;
 import java.util.List;
-import java.util.regex.Pattern;
 
 import parser.Values;
 import parser.ast.Expression;
@@ -917,6 +916,20 @@ public class PrismCL implements PrismModelListener
 		techLog.close();
 	}
 
+	/** Set a timeout, exit program if timeout is reached */
+	private void setTimeout(final int timeout)
+	{
+		common.Timeout.setTimeout(timeout, new Runnable() {
+			@Override
+			public void run()
+			{
+				mainLog.println("\nError: Timeout (after " + timeout + " seconds).");
+				mainLog.flush();
+				System.exit(1);
+			}
+		});
+	}
+
 	// PrismModelListener methods
 
 	@Override
@@ -978,33 +991,17 @@ public class PrismCL implements PrismModelListener
 					i++;
 					// ignore - this is dealt with before java is launched
 				}
+				// timeout
 				else if (sw.equals("timeout")) {
 					if (i < args.length - 1) {
-						String timeoutSpec = args[++i];
-						int multiplier = 1;
-						if (timeoutSpec.endsWith("s")) {
-							timeoutSpec = timeoutSpec.substring(0, timeoutSpec.length()-1);
-						} else if (timeoutSpec.endsWith("m")) {
-							timeoutSpec = timeoutSpec.substring(0, timeoutSpec.length()-1);
-							multiplier = 60;
-						} else if (timeoutSpec.endsWith("h")) {
-							timeoutSpec = timeoutSpec.substring(0, timeoutSpec.length()-1);
-							multiplier = 60*60;
+						int timeout = PrismUtils.convertTimeStringtoSeconds(args[++i]);
+						if (timeout < 0) {
+							errorAndExit("Negative timeout value \"" + timeout + "\" for -" + sw + " switch");
 						}
-						try {
-							final int timeout = Integer.parseInt(timeoutSpec) * multiplier;
-							common.Timeout.setTimeout(timeout, new Runnable() {
-								@Override
-								public void run()
-								{
-									mainLog.println("\nError: Timeout (after " + timeout + " seconds).");
-									mainLog.flush();
-									System.exit(1);
-								}
-							});
-						} catch (NumberFormatException e) {
-							errorAndExit("Illegal timeout value '" + timeoutSpec + "' for -" + sw + " switch");
+						if (timeout > 0) {
+							setTimeout(timeout);
 						}
+						// timeout == 0 -> no timeout
 					} else {
 						errorAndExit("Missing timeout value for -" + sw + " switch");
 					}

prism/src/prism/PrismUtils.java

@@ -320,6 +320,42 @@ public class PrismUtils
 		}
 	}
 
+	/**
+	 * Convert a string representing an amount of time (e.g. 5s, 5m, 5h, 5d, 5w) to the value
+	 * in seconds.
+	 * If the unit is omitted, we assume it is seconds.
+	 */
+	public static int convertTimeStringtoSeconds(String time) throws PrismException
+	{
+		Pattern p = Pattern.compile("([0-9]+)([smhdw]?)");
+		Matcher m = p.matcher(time);
+		if (!m.matches()) {
+			throw new PrismException("Invalid time value \"" + time + "\"");
+		}
+		int value;
+		try {
+			value = Integer.parseInt(m.group(1));
+		} catch (NumberFormatException e) {
+			throw new PrismException("Invalid time value \"" + time + "\"");
+		}
+		switch (m.group(2)) {
+		case "":
+		case "s":  // seconds
+			return value;
+		case "m":  // minutes
+			return value * 60;
+		case "h":  // hours
+			return value * (60 * 60);
+		case "d":  // days
+			return value * (24 * 60 * 60);
+		case "w":  // weeks
+			return value * (7 * 24 * 60 * 60);
+		default:
+			// Shouldn't happen
+			throw new PrismException("Invalid time value \"" + time + "\"");
+		}
+	}
+
 	/**
 	 * Convert a number of bytes to a string representing the amount of memory (e.g. 125k, 50m, 4g).
 	 */