First try at a timeout mechanism (undocumented at the moment) for command-line PrismCL.

-timeout 5      5 seconds
-timeout 5s     5 seconds
-timeout 1m     1 minute
-timeout 1h     1 hour


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

prism/src/common/Timeout.java

@@ -0,0 +1,79 @@
+//==============================================================================
+//	
+//	Copyright (c) 2015-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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 common;
+
+/**
+ * Simple timeout mechanism.
+ * After the specified number of seconds have elapsed (measured by
+ * System.currentTimeMillis()), a Runnable is invoked.
+ * Checks once per second.
+ */
+public class Timeout implements Runnable
+{
+	/** The time after which the timeout is expired. */
+	private final long timeoutTime;
+	/** The Runnable to call after the timeout has expired. */
+	private final Runnable timeoutRunnable;
+
+	/**
+	 * Set a timeout.
+	 * Starts a (daemon) thread which checks if the timeout has elapsed.
+	 */
+	public static void setTimeout(int timeoutInSeconds, Runnable timeoutRunnable) {
+		Timeout t = new Timeout(timeoutInSeconds, timeoutRunnable);
+		Thread timeoutThread = new Thread(t);
+		// the thread should be a daemon thread, because otherwise
+		// the VM will not exit before the timeout is expired...
+		timeoutThread.setDaemon(true);
+		timeoutThread.start();
+	}
+
+	/**
+	 * Constructor.
+	 */
+	private Timeout(int timeoutInSeconds, Runnable timeoutRunnable)
+	{
+		timeoutTime = System.currentTimeMillis() + timeoutInSeconds*1000;
+		this.timeoutRunnable = timeoutRunnable;
+	}
+
+	@Override
+	public void run()
+	{
+		while (true) {
+			long current = System.currentTimeMillis();
+			if (current > timeoutTime) {
+				// Timeout is expired, run Runnable
+				timeoutRunnable.run();
+				return;
+			}
+			try {
+				Thread.sleep(1000);
+			} catch (InterruptedException e) {}
+		}
+	}
+}

prism/src/prism/PrismCL.java

@@ -31,6 +31,7 @@ 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;
@@ -977,6 +978,37 @@ public class PrismCL implements PrismModelListener
 					i++;
 					// ignore - this is dealt with before java is launched
 				}
+				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;
+						}
+						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");
+						}
+					} else {
+						errorAndExit("Missing timeout value for -" + sw + " switch");
+					}
+				}
 				// print version
 				else if (sw.equals("version")) {
 					printVersion();