/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package CSP_ANALYSE;

import CSP_CREATOR.CreatorContract;
import CSP_CREATOR.CreatorInstance;
import LOGIC.Contract;
import LOGIC.Instance;
import LOGIC.ObjectList;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.InputStreamReader;
import java.util.ArrayList;
import javax.swing.JOptionPane;

/**
 *
 * @author forall
 */
public class AnalyseFDR {

    private Contract contract;
    private ArrayList<FDRResult> resultadoFDR;
    private ArrayList<FDRResult> strongOutputDChannel;
    private CreatorContract creatC;
    private CreatorInstance creatI;
    private String strongOchannel = "";
    private ReadFileCSP readF;
    private ReturnMensageFDR mensagemFdr;

    public AnalyseFDR(Contract c, ObjectList l) {
        contract = c;
        resultadoFDR = new ArrayList<>();
        strongOutputDChannel = new ArrayList<>();
        creatC = new CreatorContract(c, l);
        readF = new ReadFileCSP(c);
        mensagemFdr = new ReturnMensageFDR(c);
    }

    public ArrayList<FDRResult> takeResultIOProcess() {

        readF.saidaFDR();
        // vai ler o arquivo saidaFDR.log verificando as condições de IOProcess
        File pegarSaida = new File("fdrLog/"+contract.getName()+"_saida_"+readF.getTemp()+".log");
        if (!pegarSaida.exists()) {
            System.exit(-1);
        }
        try {

            BufferedReader pegarResultado = new BufferedReader(new FileReader(pegarSaida));
            String line = "";
            while ((line = pegarResultado.readLine()) != null) {

                if (line == null) {
                    FDRResult retorno = new FDRResult();
                    retorno.setMensagem("O arquivo CSP está com erro");
                    retorno.setResultado(false);
                    resultadoFDR.add(retorno);

                } else if (line.equals("Checking Test(inter(inputs(" + contract.getName() + "),outputs(" + contract.getName() + ")) == {}) [T= ERROR")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        resultadoFDR.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("Contract's Channels are I/O Channel");
                            retorno.setResultado(true);
                            resultadoFDR.add(retorno);
                        } else {

                            retorno.setMensagem("Contract's Channels aren't I/O Channel");
                            retorno.setResultado(false);
                            resultadoFDR.add(retorno);
                        }
                    }

                } else if (line.equals("Checking HideAll(" + contract.getName() + ") :[divergence free [FD]]")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        resultadoFDR.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("The Contract's behavior has Infinite Traces");
                            retorno.setResultado(true);
                            resultadoFDR.add(retorno);
                        } else {

                            retorno.setMensagem("The Contract's behavior doesn't have Infinite Traces");
                            retorno.setResultado(false);
                            resultadoFDR.add(retorno);
                        }
                    }
                } else if (line.equals("Checking " + contract.getName() + " :[divergence free [FD]]")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        resultadoFDR.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("The Contract's behavior is Divergence Free");
                            retorno.setResultado(true);
                            resultadoFDR.add(retorno);

                        } else {

                            retorno.setMensagem("The Contract's behavior isn't Divergence Free");
                            retorno.setResultado(false);
                            resultadoFDR.add(retorno);
                        }
                    }
                } else if (line.equals("Checking LHS_InputDet(" + contract.getName() + ") [F= RHS_InputDet(" + contract.getName() + ")")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        resultadoFDR.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("The Contract's behavior is input Deterministic");
                            retorno.setResultado(true);
                            resultadoFDR.add(retorno);
                        } else {

                            retorno.setMensagem("The Contract's behavior isn't input Deterministic");
                            retorno.setResultado(false);
                            resultadoFDR.add(retorno);
                        }
                    }
                } else if (line.equals("Checking LHS_OutputDec_A(" + contract.getName() + ") [F= RHS_OutputDec_A(" + contract.getName() + ")")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult r = new FDRResult();
                        r.setMensagem("O arquivo CSP está com erro");
                        r.setResultado(false);
                        strongOutputDChannel.add(r);
                    } else {

                        FDRResult r = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            r.setMensagem("The Contract's behavior is output decisive");
                            r.setResultado(true);
                            strongOutputDChannel.add(r);
                        } else {

                            r.setMensagem("The Contract's behavior isn't output decisive");
                            r.setResultado(false);
                            strongOutputDChannel.add(r);
                        }
                    }

                } else if (line.contains("Checking LHS_OutputDec_B(")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult r = new FDRResult();
                        r.setMensagem("O arquivo CSP está com erro");
                        r.setResultado(false);
                        strongOutputDChannel.add(r);
                    } else {
                        FDRResult r = new FDRResult();

                        if (line.equals("true") || line.equals("xtrue")) {

                            r.setMensagem("The Contract is output decisive in channels");
                            r.setResultado(true);
                            strongOutputDChannel.add(r);

                        } else {

                            r.setMensagem("The Contract NOT is output decisive in channels");
                            r.setResultado(false);
                            strongOutputDChannel.add(r);
                        }
                    }
                }
            }


        } catch (Exception e) {
            e.printStackTrace();
            JOptionPane.showMessageDialog(null, "error occurred in checking IO / Process");
        }
        resultadoFDR.add(StrongOutputIsTrue());
        //returnMensagefdr();
        resultadoFDR.add(mensagemFdr.returnMensagefdr());
       
        return resultadoFDR;

    }

    public FDRResult StrongOutputIsTrue() {
        FDRResult retorno = new FDRResult();
        for (int i = 0; i < strongOutputDChannel.size(); i++) {
            if ((!strongOutputDChannel.get(i).getResultado())) {
                retorno.setMensagem("The Contract is NOT output decisive");
                retorno.setResultado(false);
                //resultadoFDR.add(retorno);
            } else {
                retorno.setMensagem("The Contract is output decisive");
                retorno.setResultado(true);
                //resultadoFDR.add(retorno);
            }
        }

        //retorna o resultado do strongOutputDecisiviness
        return retorno;
    }
    
   
}