package de.prob2.ui.consoles.b;

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.exception.CliError;
import de.prob.exception.ProBError;
import de.prob.statespace.StateSpace;
import de.prob2.ui.consoles.ConsoleExecResult;
import de.prob2.ui.consoles.ConsoleExecResultType;
import de.prob2.ui.consoles.ConsoleInstruction;
import de.prob2.ui.consoles.Executable;
import de.prob2.ui.prob2fx.CurrentTrace;
import de.prob2.ui.project.MachineLoader;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.util.Collections;

public class BInterpreter implements Executable {

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

	@Inject
	public BInterpreter(final MachineLoader machineLoader, final CurrentTrace currentTrace) {
		defaultSS = machineLoader.getEmptyStateSpace(Collections.emptyMap());
		this.currentTrace = currentTrace;
	}

	@Override
	public ConsoleExecResult exec(final ConsoleInstruction instruction) {
		String line = instruction.getInstruction();
		AbstractEvalResult res;
		try {
			if ("clear".equals(instruction.getInstruction())) {
				return new ConsoleExecResult("clear","", ConsoleExecResultType.PASSED);
			}
			if (currentTrace.exists()) {
				res = currentTrace.get().evalCurrent(currentTrace.getModel().parseFormula(line));
			} else {
				EvaluationCommand cmd = new ClassicalB(line).getCommand(defaultSS.getRoot());
				defaultSS.execute(cmd);
				res = cmd.getValue();
			}
		} catch (CliError | EvaluationException | ProBError e) {
			logger.info("B evaluation failed", e);
			return new ConsoleExecResult("", "Invalid syntax: " + e.getMessage(), ConsoleExecResultType.ERROR);
		}
		// noinspection ObjectToString
		return new ConsoleExecResult("", res.toString(), ConsoleExecResultType.PASSED);
	}
}

@@ -37,84 +37,65 @@
 ort 
-com.google.inject.Inject;%0Aimport de.prob.animator.command.EvaluationCommand;
+java.util.Collections;%0A%0Aimport com.google.inject.Inject;%0A
 %0Aimp
@@ -153,58 +153,8 @@
 lt;%0A
-import de.prob.animator.domainobjects.ClassicalB;%0A
 impo
@@ -204,24 +204,77 @@
 nException;%0A
+import de.prob.animator.domainobjects.FormulaExpand;%0A
 import de.pr
@@ -362,20 +362,16 @@
 ace.
-StateSp
+Tr
 ace;%0A
+%0A
 impo
@@ -631,24 +631,25 @@
 hineLoader;%0A
+%0A
 import org.s
@@ -698,39 +698,8 @@
 y;%0A%0A
-import java.util.Collections;%0A%0A
 publ
@@ -847,58 +847,62 @@
 nal 
-StateSpace defaultSS;%0A%09private CurrentTrace curren
+CurrentTrace currentTrace;%0A%09private final Trace defaul
 tTra
@@ -1012,20 +1012,74 @@
 %7B%0A%09%09
-defaultSS = 
+this.currentTrace = currentTrace;%0A%09%09this.defaultTrace = new Trace(
 mach
@@ -1134,44 +1134,9 @@
 p())
-;%0A%09%09this.currentTrace = currentTrace
+)
 ;%0A%09%7D
@@ -1223,89 +1223,8 @@
 ) %7B%0A
-%09%09String line = instruction.getInstruction();%0A%09%09AbstractEvalResult res;%0A%09%09try %7B%0A%09
 %09%09if
@@ -1269,25 +1269,24 @@
 ction())) %7B%0A
-%09
 %09%09%09return ne
@@ -1354,18 +1354,41 @@
 ;%0A%09%09
-%09%7D%0A%09%09%09if (
+%7D%0A%09%09try %7B%0A%09%09%09final Trace trace = 
 curr
@@ -1408,21 +1408,10 @@
 ts()
-) %7B%0A%09%09%09%09res =
+ ?
  cur
@@ -1429,29 +1429,72 @@
 et()
-.evalCurrent(c
+ : defaultTrace;%0A%09%09%09AbstractEvalResult res = trace.evalC
 urrent
-T
+(t
 race
@@ -1522,168 +1522,178 @@
 ula(
-line));%0A%09%09%09%7D else %7B%0A%09%09%09%09EvaluationCommand cmd = new ClassicalB(line).getCommand(defaultSS.getRoot());%0A%09%09%09%09defaultSS.execute(cmd);%0A%09%09%09%09res = cmd.getValue();%0A%09%09%09%7D
+instruction.getInstruction(), FormulaExpand.expand));%0A%09%09%09// noinspection ObjectToString%0A%09%09%09return new ConsoleExecResult(%22%22, res.toString(), ConsoleExecResultType.PASSED);
 %0A%09%09%7D
@@ -1831,42 +1831,32 @@
 %22, %22
-Invalid syntax: %22 + e.getMessage()
+Evaluation failed: %22 + e
 , Co
@@ -1891,123 +1891,8 @@
 %09%09%7D%0A
-%09%09// noinspection ObjectToString%0A%09%09return new ConsoleExecResult(%22%22, res.toString(), ConsoleExecResultType.PASSED);%0A
 %09%7D%0A%7D

Disable evaluation result truncation in BInterpreter (PROB2UI-141)