package edu.kit.iti.formal.pse.worthwhile.prover;

import java.util.HashSet;
import java.util.Set;

/**
 * Prover caller that implements a timeout after which the proving process should be aborted.
 * 
 * @author Leon Handreke
 */
public abstract class TimeoutProverCaller implements ProverCaller {

	/**
	 * time in milliseconds after which to return with an UNKNOWN result if no proof has been found.
	 */
	private int timeout;

	/**
	 * @return the timeout
	 */
	public final int getTimeout() {
		return timeout;
	}

	/**
	 * @param timeout
	 *                the timeout to set
	 */
	public final void setTimeout(final int timeout) {
		this.timeout = timeout;
	}

	/**
	 * The set of tasks to be run after a timeout occurs.
	 */
	private Set<Runnable> cleanupTasks = new HashSet<Runnable>();

	/**
	 * Add a cleanup task to be run after the timeout occurs.
	 * 
	 * @param cleanupTask
	 *                the cleanup task to add
	 */
	public final void addCleanupTask(final Runnable cleanupTask) {
		this.cleanupTasks.add(cleanupTask);
	}

	/**
	 * Run all scheduled cleanup tasks.
	 */
	private void runCleanupTasks() {
		for (Runnable task : this.cleanupTasks) {
			task.run();
		}
	}

	/**
	 * @param timeout
	 *                time in milliseconds after which to return with an UNKNOWN result if no proof has been found
	 */
	public TimeoutProverCaller(final int timeout) {
		this.timeout = timeout;
	}

	/**
	 * Schedule cleanup tasks after the given timeout.
	 */
	protected final void scheduleProverCallerTimeout() {
		// thread that kills the prover after timeout
		Thread killerThread = new Thread() {
			public void run() {
				try {
					Thread.sleep(TimeoutProverCaller.this.timeout);
				} catch (InterruptedException e) {
					TimeoutProverCaller.this.runCleanupTasks();
				} finally {
					TimeoutProverCaller.this.runCleanupTasks();
				}
			};
		};
		killerThread.start();
	}
}

@@ -990,24 +990,190 @@
 anupTask) %7B%0A
+%09%09// see runCleanupTasks for information on another thread that may tries to access cleanupTasks while we%0A%09%09// are modifying it%0A%09%09synchronized (this.cleanupTasks) %7B%0A%09
 %09%09this.clean
@@ -1198,16 +1198,20 @@
 pTask);%0A
+%09%09%7D%0A
 %09%7D%0A%0A%09/**
@@ -1287,16 +1287,259 @@
 sks() %7B%0A
+%09%09// runCleanupTasks is called from a thread, which is created in scheduleProverCallerTimeout, separate%0A%09%09// from the thread that created this and usually calls addCleanupTask, which modifies cleanupTasks%0A%09%09synchronized (this.cleanupTasks) %7B%0A%09
 %09%09for (R
@@ -1577,16 +1577,17 @@
 s) %7B%0A%09%09%09
+%09
 task.run
@@ -1590,16 +1590,21 @@
 .run();%0A
+%09%09%09%7D%0A
 %09%09%7D%0A%09%7D%0A%0A

Fix add/iterate access to cleanupTasks is not synchronized