package de.prob2.ui.consoles.b;

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

import com.google.inject.Inject;

import de.prob.animator.command.EvaluationCommand;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.ClassicalB;
import de.prob.animator.domainobjects.EvaluationException;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.scripting.ClassicalBFactory;
import de.prob.scripting.ModelTranslationError;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.FormalismType;
import de.prob.statespace.IAnimationChangeListener;
import de.prob.statespace.StateSpace;
import de.prob.statespace.Trace;
import de.prob2.ui.consoles.ConsoleInstruction;


public class BInterpreter implements IAnimationChangeListener {

	private static final Logger logger = LoggerFactory.getLogger(BInterpreter.class);
	private final StateSpace defaultSS;
	private String modelName;
	private Trace currentTrace;

	@Inject
	public BInterpreter(final ClassicalBFactory bfactory, final AnimationSelector animations) {
		StateSpace s = null;
		try {
			s = bfactory.create("MACHINE Empty END").load();
		} catch (ModelTranslationError e) {
			throw new RuntimeException("loading a model into ProB failed!");
		}
		defaultSS = s;
		animations.registerAnimationChangeListener(this);
	}

	public String eval(final ConsoleInstruction instruction) {
		String line = instruction.getInstruction();
		String res = "";
		try {
			IEvalElement parsed = parse(line);
			if (currentTrace == null) {
				EvaluationCommand cmd = parsed.getCommand(defaultSS.getRoot());
				defaultSS.execute(cmd);
				res = cmd.getValue().toString();
			} else {
				AbstractEvalResult result = currentTrace.evalCurrent(parsed);
				res = result.toString();
			}
		} catch (EvaluationException e) {
			res = "Not correct B syntax! ";
			logger.debug(res);
			return res;
		}
		return res;
	}

	public String result(AbstractEvalResult res) {
		return res.toString();
	}
	
	public IEvalElement parse(final String line) {
		if (currentTrace == null) {
			return new ClassicalB(line);
		}
		return currentTrace.getModel().parseFormula(line);
	}
		
	@Override
	public void traceChange(final Trace currentTrace, final boolean currentAnimationChanged) {
		if (currentAnimationChanged) {
			if (currentTrace == null) {
				modelName = null;
				notifyModelChange(modelName);
			} else if (currentTrace.getModel().getFormalismType() == FormalismType.B) {
				// ignore models that are not B models
				String modelName = currentTrace.getStateSpace().getMainComponent().toString();
				if (!modelName.equals(this.modelName)) {
					this.modelName = modelName;
					notifyModelChange(this.modelName);
				}
			}
			this.currentTrace = currentTrace;
		}
	}

	public void notifyModelChange(final String name) {
		//submit(WebUtils.wrap("cmd", "BConsole.modelChange", "modelloaded", name != null, "name", name == null ? "" : name));
		logger.trace("BConsole.modelChange\n modelloaded");
		String output = name == null ? "" : name;
		logger.trace(output);
	}

	@Override
	public void animatorStatus(final boolean busy) {
		if (busy) {
			//submit(WebUtils.wrap("cmd", "BConsole.disable"));
			logger.trace("BConsole.disable");
		} else {
			//submit(WebUtils.wrap("cmd", "BConsole.enable"));
			logger.trace("BConsole.enable");
		}
	}


}

@@ -1211,34 +1211,20 @@
 %0A%09%09%09
-throw new RuntimeException
+logger.error
 (%22lo
@@ -1255,16 +1255,19 @@
 failed!%22
+, e
 );%0A%09%09%7D%0A%09
@@ -1828,75 +1828,92 @@
 %0A%09%09%09
-res = %22Not correct B syntax! %22;%0A%09%09%09logger.debug(res);%0A%09%09%09return res
+logger.info(%22B evaluation failed%22, e);%0A%09%09%09return %22Invalid syntax: %22 + e.getMessage()
 ;%0A%09%09

Improve error reporting in B interpreter