package de.prob2.ui.verifications.ltl.formula;

import java.util.ArrayList;

import javax.inject.Inject;
import com.google.inject.Injector;

import de.be4.classicalb.core.parser.ClassicalBParser;
import de.prob.animator.command.EvaluationCommand;
import de.prob.animator.domainobjects.LTL;
import de.prob.ltl.parser.LtlParser;
import de.prob.ltl.parser.pattern.PatternManager;
import de.prob.statespace.State;
import de.prob2.ui.prob2fx.CurrentTrace;
import de.prob2.ui.project.machines.Machine;
import de.prob2.ui.verifications.ltl.LTLMarker;
import de.prob2.ui.verifications.ltl.LTLParseListener;
import de.prob2.ui.verifications.ltl.LTLResultHandler;
import de.prob2.ui.verifications.ltl.LTLView;
import de.prob2.ui.verifications.ltl.LTLResultHandler.Checked;

public class LTLFormulaChecker {
				
	private final CurrentTrace currentTrace;
	
	private final Injector injector;
	
	private final LTLResultHandler resultHandler;
	
	@Inject
	private LTLFormulaChecker(final CurrentTrace currentTrace, final Injector injector, final LTLResultHandler resultHandler) {
		this.currentTrace = currentTrace;
		this.injector = injector;
		this.resultHandler = resultHandler;
	}
	
	public void checkMachine(Machine machine, PatternManager patternManager) {
		ArrayList<Boolean> success = new ArrayList<>();
		success.add(true);
		machine.getFormulas().forEach(item-> {
			Checked result = this.checkFormula(item, patternManager);
			if(result == Checked.FAIL || result == Checked.EXCEPTION) {
				machine.setCheckedFailed();
				success.set(0, false);
			}
		});
		if(success.get(0)) {
			machine.setCheckedSuccessful();
		}
	}
	
	public Checked checkFormula(LTLFormulaItem item, PatternManager patternManager) {
		LTL formula = null;
		Object result = null;
		State stateid = currentTrace.getCurrentState();
		LtlParser parser = new LtlParser(item.getFormula());
		LTLParseListener parseListener = new LTLParseListener();
		parser.removeErrorListeners();
		parser.addErrorListener(parseListener);
		parser.addWarningListener(parseListener);
		parser.setPatternManager(patternManager);
		parser.parse();
		if(parseListener.getErrorMarkers().size() > 0) {
			StringBuilder msg = new StringBuilder();
			for(LTLMarker error : parseListener.getErrorMarkers()) {
				msg.append(error.getMsg()+"\n");
			}
			result = new LTLParseError(msg.toString());
		} else {
			formula = new LTL(item.getFormula(), new ClassicalBParser(), parser);
			EvaluationCommand lcc = formula.getCommand(stateid);
			currentTrace.getStateSpace().execute(lcc);
			result = lcc.getValue();
		}
		Checked checked = resultHandler.handleFormulaResult(item, result, stateid);
		injector.getInstance(LTLView.class).refreshFormula();
		return checked;
	}
		
}

@@ -1701,54 +1701,8 @@
 ) %7B%0A
-%09%09LTL formula = null;%0A%09%09Object result = null;%0A
 %09%09St
@@ -1808,243 +1808,419 @@
 ;%0A%09%09
-LTLParseListener parseListener = new LTLParseListener();%0A%09%09parser.removeErrorListeners();%0A%09%09parser.addErrorListener(parseListener);%0A%09%09parser.addWarningListener(
+parser.setPatternManager(patternManager);%0A%09%09Checked checked = resultHandler.handleFormulaResult(item, getResult(parser, item), stateid);%0A%09%09injector.getInstance(LTLView.class).refreshFormula();%0A%09%09return checked;%0A%09%7D%0A%09%0A%09private Object getResult(LtlParser 
 parse
-Listener);%0A%09%09parser.setPatternManager(patternManager);%0A%09%09parser.parse(
+r, LTLFormulaItem item) %7B%0A%09%09Object result = null;%0A%09%09State stateid = currentTrace.getCurrentState();%0A%09%09LTLParseListener parseListener = parseFormula(parser
 );%0A%09
@@ -2476,16 +2476,20 @@
 se %7B%0A%09%09%09
+LTL 
 formula 
@@ -2690,156 +2690,305 @@
 %7D%0A%09%09
-Checked checked = resultHandler.handleFormulaResult(item, result, stateid);%0A%09%09injector.getInstance(LTLView.class).refreshFormula();%0A%09%09return checked
+return result;%0A%09%7D%0A%09%0A%09private LTLParseListener parseFormula(LtlParser parser) %7B%0A%09%09LTLParseListener parseListener = new LTLParseListener();%0A%09%09parser.removeErrorListeners();%0A%09%09parser.addErrorListener(parseListener);%0A%09%09parser.addWarningListener(parseListener);%0A%09%09parser.parse();%0A%09%09return parseListener
 ;%0A%09%7D

Refactor LTLFormulaChecker