package dfatool.strategy.verification;

import java.io.IOException;
import java.io.UnsupportedEncodingException;
import java.util.ArrayList;
import java.util.List;

import dfatool.parser.ParseException;
import dfatool.strategy.graph.CommunicationGraph;
import dfatool.strategy.graph.Graph;
import dfatool.strategy.graph.TarjanAlgorithm;
import dfatool.strategy.graph.TarjanAlgorithm.Bridge;
import dfatool.strategy.verification.elements.EssentialComponent;
import dfatool.strategy.verification.elements.EssentialComponents;
import dfatool.strategy.verification.fdr2.FileGeneration;
import dfatool.strategy.verification.fdr2.RefinementChecker;

public class Decomposition {
	
	private List<Bridge> bridges;

	public void decompose() throws IOException, InterruptedException {
		findBridges();
		verifyConflictFreedom();
		generateEssentialComponentsAndUpdateGraph();
	}

	private void findBridges() {
		try {
			TarjanAlgorithm algo = new TarjanAlgorithm();
			bridges = algo.getBridges();
			System.out.println("Found bridges: "+bridges.size());
		} catch (UnsupportedEncodingException | ParseException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
	}
	
	public void generateDecompositionVerificationFiles(){
		try {
			List<Bridge> localBridges = new TarjanAlgorithm().getBridges();
			FileGeneration fg = new FileGeneration();
			fg.generateModel();
			for(Bridge b: localBridges){
				fg.generateConflictVerification(b.getFst().toString(), b.getSnd().toString());				
			}
		} catch (UnsupportedEncodingException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		} catch (ParseException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		
	}
	
	private void verifyConflictFreedom() throws IOException, InterruptedException {
		FileGeneration fg = new FileGeneration();
		RefinementChecker rc = new RefinementChecker();
		fg.generateModel();
		List<Bridge> temp = new ArrayList<Bridge>(bridges);
		for(Bridge b: bridges){
			fg.generateConflictVerification(b.getFst().toString(), b.getSnd().toString());
			String conflictFileName = fg.getConflictName(b.getFst().toString(), b.getSnd().toString());
			boolean succeeded = rc.checkFile(conflictFileName);
			if(!succeeded){
				System.out.println("Conflict verification didnt succeed for bridge: "+b.toString());
				temp.remove(b);
			}
				
		}
		bridges = temp;
	}

	private void generateEssentialComponentsAndUpdateGraph() {
		CommunicationGraph cg = CommunicationGraph.getInstance();
		Graph g = (Graph) cg.getGraph();
		g.removeEdges(bridges);
		EssentialComponents ecs = EssentialComponents.getInstance();
		List<EssentialComponent> cyclicEssentialComponents = new ArrayList<EssentialComponent>();
		int i = 0 ;
		for(EssentialComponent ec : g.getConnectedComponents()){
			if(ec.getComponentsList().size() > 1){
				ec.setName("EC"+ i);
				cyclicEssentialComponents.add(ec);
				i++;
			}
		}
		ecs.setEssentialComponents(cyclicEssentialComponents);
	}


	

}
