package de.prob.web;

import java.util.concurrent.Callable;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.concurrent.TimeUnit;
import java.util.concurrent.TimeoutException;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.exceptions.BParseException;
import de.prob.ProBException;
import de.prob.animator.command.RemoteEvaluateCommand;
import de.prob.animator.command.RemoteEvaluateCommand.EEvaluationStrategy;
import de.prob.animator.domainobjects.EvaluationResult;
import de.prob.statespace.StateSpace;

public class Evaluator {
	private static final int TIMEOUT = 3;
	private static final TimeUnit TIMEOUT_UNIT = TimeUnit.SECONDS;
	private static final String TIMEOUT_MESSAGE = "Could not complete calculation within the time constraints. ("
			+ TIMEOUT + " " + TIMEOUT_UNIT + ")";

	private final static Logger logger = LoggerFactory
			.getLogger(Evaluator.class);

	public final StateSpace space;
	private volatile boolean busy;

	public Evaluator(StateSpace space) {
		this.space = space;
	}

	public String eval(final String formula) throws BParseException {
		return exec(new RemoteEvaluateCommand(formula,
				EEvaluationStrategy.EXISTENTIAL), formula);
	}

	public String check(final String formula) throws BParseException {
		return exec(new RemoteEvaluateCommand(formula,
				EEvaluationStrategy.UNIVERSAL), formula);
	}

	public String exec(final RemoteEvaluateCommand command, final String formula)
			throws BParseException {
		ExecutorService executor = Executors.newSingleThreadExecutor();
		Future<String> future = executor.submit(new Callable<String>() {
			@Override
			public String call() throws Exception {
				try {
					space.execute(command);
					EvaluationResult first = command.getValue();
					return first.toString();
				} catch (ProBException e) {
					Throwable cause = e.getCause();
					if (cause != null)
						return "ERROR: " + cause.getMessage();
					return "ERROR: " + e.getMessage();
				}
			}
		});

		try {
			this.busy = true;
			String value = future.get(TIMEOUT, TIMEOUT_UNIT);
			logger.trace("Result {} ", value);
			return value;
		} catch (TimeoutException e) {
			space.sendInterrupt();
			logger.debug("Timeout while calculating '{}'.", formula);
			return TIMEOUT_MESSAGE;
		} catch (InterruptedException e) {
			logger.error("Interrupt Exception ", e);
			return "ERROR: " + e.getMessage();
		} catch (ExecutionException e) {
			Throwable cause = e.getCause();
			if (cause instanceof BException) {
				throw (BParseException) cause.getCause();
			}
			return "EXECUTION ERROR";
		} 
		
		finally {
			executor.shutdownNow();
			this.busy = false;
		}
	}

	public boolean isBusy() {
		return busy;
	}

}

@@ -1312,100 +1312,153 @@
 %7B%0A%09%09
-return exec(new RemoteEvaluateCommand(formula,%0A%09%09%09%09EEvaluationStrategy.EXISTENTIAL), formula
+EEvaluationStrategy strategy = EEvaluationStrategy.EXISTENTIAL;%0A%09%09return exec(new RemoteEvaluateCommand(formula, strategy), formula,%0A%09%09%09%09strategy
 );%0A%09
@@ -1528,16 +1528,80 @@
 ption %7B%0A
+%09%09EEvaluationStrategy strategy = EEvaluationStrategy.UNIVERSAL;%0A
 %09%09return
@@ -1644,52 +1644,41 @@
 ula,
-%0A%09%09%09%09EEvaluationStrategy.UNIVERSAL), formula
+ strategy), formula,%0A%09%09%09%09strategy
 );%0A%09
@@ -1736,17 +1736,20 @@
 command,
- 
+%0A%09%09%09
 final St
@@ -1760,16 +1760,52 @@
  formula
+, final EEvaluationStrategy strategy
 )%0A%09%09%09thr
@@ -2113,31 +2113,260 @@
 %09%09%09%09
-return first.toString()
+String p1 = ((strategy == EEvaluationStrategy.EXISTENTIAL) ? %22Existentially Quantified Predicate is %22%0A%09%09%09%09%09%09%09: %22Universially Quantified Predicate is %22)%0A%09%09%09%09%09%09%09+ first.value;%0A%0A%09%09%09%09%09return p1 + %22%5Cn%22 + first.explanation + %22%5Cn     %22%0A%09%09%09%09%09%09%09+ first.solution
 ;%0A%09%09
@@ -3157,12 +3157,9 @@
 %0A%09%09%7D
- %0A%09%09
+%0A
 %0A%09%09f

improved output