/*
 * This file has been developed at the University of Munich, Chair for Programming & Software Engineering.
 * 
 * This file is licensed under the Eclipse Public License (EPL) 1.0
 * 
 */
package eu.uml4soa.utbm.vnserver;

import java.util.List;
import java.util.Set;

import net.miowb.model.mio.ModalIOAutomaton;
import net.miowb.model.mio.State;
import net.miowb.model.mio.Transition;
import net.miowb.operations.refinement.MioStrictObservationalRefinement;
import net.miowb.operations.refinement.MioStrongRefinement;
import net.miowb.operations.refinement.MioWeakRefinement;
import net.miowb.workbench.helpers.AutomatonUtils;
import net.miowb.workbench.operations.IMioRefinementOperation;
import net.miowb.workbench.operations.model.RefinementRelation;
import net.miowb.workbench.operations.model.SingleActionPath;
import net.miowb.workbench.operations.model.StatePair;
import net.miowb.workbench.operations.result.RefinementResult;

import org.eclipse.emf.common.util.EList;
import org.eclipse.uml2.uml.Activity;
import org.eclipse.uml2.uml.Behavior;
import org.eclipse.uml2.uml.Class;
import org.eclipse.uml2.uml.Element;
import org.eclipse.uml2.uml.Model;
import org.eclipse.uml2.uml.ProtocolStateMachine;

import eu.mdd4soa.smm.exception.TransformationException;
import eu.mdd4soa.smm.statik.Participant;
import eu.mdd4soa.trans.uml2smm.transform.BehaviourConverter;
import eu.mdd4soa.trans.uml2smm.transform.StaticConverter;
import eu.uml4soa.utbm.u2m.SemanticsException;
import eu.uml4soa.utbm.u2m.model.CAutomaton;
import eu.uml4soa.utbm.u2m.semantics.OrchestrationSemanticsFunction;
import eu.uml4soa.utbm.u2m.semantics.ProtocolSemanticsFunction;

public class ServerRefinementChecker extends AbstractChecker {

	public ServerRefinementChecker(String theory, String fileName) {
		super(theory, fileName);
	}

	public boolean check() {

		Model model= loadModel();

		// LEFT: PROTOCOL
		ProtocolStateMachine psm1= getPSM(model, getLeftName());

		// RIGHT: ORCHESTRATION
		org.eclipse.uml2.uml.Class participant= getParticipant(model, getRightName());

		if (psm1 == null || participant == null) {
			setResult("Could not find the state machine or the participant in EMF model.");
			return false;
		}

		ProtocolSemanticsFunction f= new ProtocolSemanticsFunction(psm1);
		try {
			f.calculateSemantics();
		} catch (SemanticsException e1) {
			setResult("Problem finding semantics for PSM: " + e1.getMessage());
			return false;
		}
		ModalIOAutomaton protocol= f.getSemantics();

		EList<Behavior> ownedBehaviors= participant.getOwnedBehaviors();
		if (ownedBehaviors == null || ownedBehaviors.size() != 1 || (! (ownedBehaviors.get(0) instanceof Activity))) {
			setResult("Could not find participant behaviour in EMF model.");
			return false;
		}

		ModalIOAutomaton orch= null;

		try {
			Activity b= (Activity) ownedBehaviors.get(0);
			orch= calcSem(b);
		} catch (Exception e) {
			setResult("Problem finding semantics for activity: " + e.getMessage());
			return false;
		}

		IMioRefinementOperation checker= null;
		if (getTheory().equals(ServerClientConstants.THEORY_SO))
			checker= new MioStrictObservationalRefinement();
		if (getTheory().equals(ServerClientConstants.THEORY_WEAK))
			checker= new MioWeakRefinement();
		if (getTheory().equals(ServerClientConstants.THEORY_STRONG))
			checker= new MioStrongRefinement();

		if (getTheory().equals(ServerClientConstants.THEORY_STRONG) || getTheory().equals(ServerClientConstants.THEORY_WEAK)) {
			// hiding
			AutomatonUtils.hideEquals(orch, protocol);
		}


		RefinementResult result= checker.checkRefinement(protocol, orch);
		if (result.isOkay()) {
			// All is well.
			return true;
		} else {
			// All is NOT well.
			List<RefinementRelation> negativeResults= result.getNegativeResults();
			if (negativeResults == null || negativeResults.isEmpty()) {
				setResult("No result from checker.");
				return false;
			}
			RefinementRelation refinementRelation= negativeResults.get(0);

			StatePair pairWithoutProvided= refinementRelation.getPairWithoutProvided();
			State protState= pairWithoutProvided.getS1();
			State implState= pairWithoutProvided.getS2();
			Transition transition= null; // pairWithoutProvided.getProblematicPath().getRelevantTransition();

			Set<Transition> flattenedTransitions= refinementRelation.getFlattenedTransitions();
			for (Transition transition2 : flattenedTransitions) {
				if (transition2.getFrom().equals(protState))
					transition= transition2;
			}

			List<SingleActionPath> requiredWithoutProvided= refinementRelation.getRequiredWithoutProvided();
			for (SingleActionPath singleActionPath : requiredWithoutProvided) {
				transition= singleActionPath.getRelevantTransition();
			}
			System.out.println(requiredWithoutProvided);

			String whichAutomaton= "LEFT";
			String actionLabel= "UNKNOWN";
			if (transition != null) {

				// not so sure here...

				// if (transition.getFrom().equals(protState))
				// whichAutomaton= "LEFT";
				// else
				// whichAutomaton= "RIGHT";
				actionLabel= transition.getAction().getLabel();
			}

			setResult(ServerClientConstants.ERROR_REFINEMENT + ServerClientConstants.SEPARATOR + whichAutomaton + ServerClientConstants.SEPARATOR
					+ protState.getLabel() + ServerClientConstants.SEPARATOR + implState.getLabel() + ServerClientConstants.SEPARATOR + actionLabel);
			System.out.println(getResult());
			return false;
		}

	}

	private ModalIOAutomaton calcSem(Activity behaviour) throws TransformationException, SemanticsException {

		Element owner= behaviour.getOwner();
		if (! (owner instanceof org.eclipse.uml2.uml.Class))
			throw new TransformationException("Owner of behaviour is not a class.");


		Participant ismParticipant= StaticConverter.convert((Class) owner);
		eu.mdd4soa.smm.behaviour.ServiceActivity sa= BehaviourConverter.convert(ismParticipant, behaviour);


		CAutomaton transform= OrchestrationSemanticsFunction.transform(sa);
		return transform.toEMF();
	}

}
