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

import CREATOR_CONDICTIONS_RULES.CreatorNamesOfProcessCSP;
import CREATOR_CONDICTIONS_RULES.CreatorProtocol;
import LOGIC.Barra;
import LOGIC.Contract;
import LOGIC.Instance;
import LOGIC.Protocols;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.util.ArrayList;
import java.util.LinkedList;
import javax.swing.JOptionPane;

/**
 *
 * @author sarah
 */
public class AnalyseRuleCommunication {

    private ArrayList<FDRResult> rule1;//i/oconfluente c1
    private ArrayList<FDRResult> rule2;//i/oconfluente c2
    private ArrayList<FDRResult> rule3;//protocolo compatível c1
    private ArrayList<FDRResult> rule4;//protocolo compatível c2
    private ArrayList<FDRResult> rule5;//have infinite traces
    private ArrayList<FDRResult> ruleResult;
    private LinkedList<Instance> instance;
    private String pegarErro = "";
    private Contract c;
    private ReadFileCSP rdf;
    private ReturnMensageFDR mensagemF;
    private LinkedList<Protocols> prot;
    private CreatorNamesOfProcessCSP creatName;
    private LinkedList<String> colocaprot;
    private LinkedList<String> colocaprot_RIO;
    private LinkedList<String> colocaDual_prot_RIO;
    private String eventoprotocol1 = "";
    private String eventoprotocol2 = "";
    private Barra barra;
    public AnalyseRuleCommunication(LinkedList<Instance> i, LinkedList<Protocols> p) {
        instance = i;
        rule1 = new ArrayList<FDRResult>();
        rule2 = new ArrayList<FDRResult>();
        rule3 = new ArrayList<FDRResult>();
        rule4 = new ArrayList<FDRResult>();
        rule5 = new ArrayList<FDRResult>();
        ruleResult = new ArrayList<FDRResult>();
        c = new Contract();
        c.setName("RuleCommunicationOf" + i.get(0).getName() + "_" + i.get(1).getName());
        rdf = new ReadFileCSP(c);
        mensagemF = new ReturnMensageFDR(c);
        prot = p;
        creatName = new CreatorNamesOfProcessCSP(i, p);
        colocaprot = new LinkedList<>();
        colocaprot_RIO = new LinkedList<>();
        colocaDual_prot_RIO = new LinkedList<>();

        barra = new Barra();
        barra.criarBarra(5);
        //pegando o nome do evento que passei por paramentro no protocolo 
        int pr1, pr2, pr3, pr4;

        pr1 = p.get(0).getProtocol().indexOf("(");
        pr2 = p.get(0).getProtocol().lastIndexOf(")");
        eventoprotocol1 = p.get(0).getProtocol().substring(pr1 + 1, pr2);

        pr3 = p.get(1).getProtocol().indexOf("(");
        pr4 = p.get(1).getProtocol().lastIndexOf(")");
        eventoprotocol2 = p.get(1).getProtocol().substring(pr3 + 1, pr4);
    }

    public ArrayList<FDRResult> resultRule() {

        colocaprot = creatName.CreatorProt_Name();
        colocaprot_RIO = creatName.CreatorProt_RIO();
        colocaDual_prot_RIO = creatName.CreatorDual_Prot_RIO();

        rdf.saidaFDR();
        // vai ler o arquivo saidaFDR.log verificando as condições de IOProcess
        File pegarSaida = new File("fdrLog/" + c.getName() + "_saida_" + rdf.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);
                    ruleResult.add(retorno);
                    //Checking Cell0\{|rd0|} [T= Cell0
                } else if (line.equals("Checking " + instance.get(0).getName()
                        + " \\ {|" + eventoprotocol1
                        + "|} [T= " + instance.get(0).getName())) {


                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("channel is in the alphabet of contract");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("NOT");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }
                } else if (line.equals("Checking STOP [T= RUN(inter(events("
                        + instance.get(0).getName() + "),events("
                        + instance.get(1).getName() + ")))")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("The Alphabets are disjont");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("The Alphabets aren't disjont");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }
                } else if (line.equals("Checking " + colocaprot.get(0)
                        + " :[divergence free [FD]]")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }
                } else if (line.equals("Checking " + colocaprot.get(0)
                        + " [F= PROT_IMP_def("
                        + instance.get(0).getName() + ","
                        + eventoprotocol1 + ")")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }

                } else if (line.equals("Checking PROT_IMP_def("
                        + instance.get(0).getName() + ","
                        + eventoprotocol1
                        + ") [FD= " + colocaprot.get(0))) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(subseteq(inputs_PROT_IMP("
                        + instance.get(0).getName()
                        + "," + eventoprotocol1 + "),{|"
                        + eventoprotocol1
                        + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(subseteq(outputs_PROT_IMP("
                        + instance.get(0).getName()
                        + "," + eventoprotocol1 + "),{|"
                        + eventoprotocol1
                        + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }
                } else if (line.equals("Checking InBufferProt(" + colocaprot_RIO.get(0) + ","
                        + eventoprotocol1 + ") :[deterministic [F]]")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule1.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule1.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule1.add(retorno);
                        }
                    }

                    barra.aumentar(line);
                      // verifcando I/O confluente para componente 2         
                    //componente 2


                    //Checking Cell1\{|rd1|} [T= Cell1
                } else if (line.equals("Checking " + instance.get(1).getName()
                        + " \\ {|" + prot.get(1).getCanal().getName()
                        + "|} [T= " + instance.get(1).getName())) {


                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule2.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("channel is in the alphabet of contract");
                            retorno.setResultado(true);
                            rule2.add(retorno);
                        } else {

                            retorno.setMensagem("NOT");
                            retorno.setResultado(false);
                            rule2.add(retorno);
                        }
                    }

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

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule2.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule2.add(retorno);
                        }
                    }


                } else if (line.equals("Checking " + colocaprot.get(1)
                        + " [F= PROT_IMP_def("
                        + instance.get(1).getName() + ","
                        + prot.get(1).getCanal().getName() + ")")) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule2.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule2.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule2.add(retorno);
                        }
                    }

                } else if (line.equals("Checking PROT_IMP_def("
                        + instance.get(1).getName() + ","
                        + prot.get(1).getCanal().getName()
                        + ") [FD= " + colocaprot.get(1))) {
                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule2.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule2.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule2.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(subseteq(inputs_PROT_IMP("
                        + instance.get(1).getName()
                        + "," + prot.get(1).getCanal().getName()
                        + "),{|" + prot.get(1).getCanal().getName()
                        + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule2.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule2.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule2.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(subseteq(outputs_PROT_IMP("
                        + instance.get(1).getName()
                        + "," + prot.get(1).getCanal().getName() + "),{|"
                        + prot.get(1).getCanal().getName()
                        + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule2.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule2.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule2.add(retorno);
                        }
                    }
                } else if (line.equals("Checking InBufferProt(" + colocaprot_RIO.get(1)
                        + "," + eventoprotocol2 + ") :[deterministic [F]]")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule2.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule2.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule2.add(retorno);
                        }
                    }

                    barra.aumentar(line);


//outro conjunto de verificações                    
//D.6: Protocols are Strong Compatible 
//componente 1

                } else if (line.equals("Checking "
                        + colocaprot_RIO.get(0)
                        + " :[deadlock free [FD]]")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }

                } else if (line.equals("Checking Test(subseteq(inputs("
                        + colocaprot_RIO.get(0) + "), {| "
                        + eventoprotocol1 + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(subseteq(outputs("
                        + colocaprot_RIO.get(0) + "), {|"
                        + eventoprotocol2 + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }




                } else if (line.equals("Checking Test(inputs("
                        + colocaprot_RIO.get(0) + ") == outputs("
                        + colocaDual_prot_RIO.get(0) + ")) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(outputs("
                        + colocaprot_RIO.get(0) + ") == inputs("
                        + colocaDual_prot_RIO.get(0) + ")) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaDual_prot_RIO.get(0)
                        + " [T= " + colocaprot_RIO.get(0))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaprot_RIO.get(0)
                        + " [T= " + colocaDual_prot_RIO.get(0))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }

                } else if (line.equals("Checking "
                        + colocaDual_prot_RIO.get(0)
                        + " [F= " + colocaprot_RIO.get(1))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaprot_RIO.get(1)
                        + " [F= " + colocaDual_prot_RIO.get(0))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule3.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule3.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule3.add(retorno);
                        }
                    }

                    barra.aumentar(line);
                    
                     } else if (line.equals("Checking "
                        + colocaprot_RIO.get(1)
                        + " :[deadlock free [FD]]")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(subseteq(inputs("
                        + colocaprot_RIO.get(1) + "), {| "
                        + prot.get(1).getCanal().getName() + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }

                } else if (line.equals("Checking Test(subseteq(outputs("
                        + colocaprot_RIO.get(1) + "), {| "
                        + prot.get(0).getCanal().getName() + "|})) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(inputs("
                        + colocaprot_RIO.get(1) + ") == outputs("
                        + colocaDual_prot_RIO.get(1) + ")) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }
                } else if (line.equals("Checking Test(outputs("
                        + colocaprot_RIO.get(1) + ") == inputs("
                        + colocaDual_prot_RIO.get(1) + ")) [T= ERROR")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaDual_prot_RIO.get(1)
                        + " [T= " + colocaprot_RIO.get(1))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaprot_RIO.get(1)
                        + " [T= " + colocaDual_prot_RIO.get(1))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaDual_prot_RIO.get(1)
                        + " [F= " + colocaprot_RIO.get(0))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaprot_RIO.get(0)
                        + " [F= " + colocaDual_prot_RIO.get(1))) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule4.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule4.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule4.add(retorno);
                        }
                    }

                    barra.aumentar(line);


// outro conjunto de verificações
                    // Protocols have finite output property
                } else if (line.equals("Checking "
                        + colocaprot_RIO.get(0) + "\\outputs("
                        + colocaprot_RIO.get(0) + ") :[divergence free [FD]]")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule5.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule5.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule5.add(retorno);
                        }
                    }
                } else if (line.equals("Checking "
                        + colocaprot_RIO.get(1)
                        + "\\outputs(" + colocaprot_RIO.get(1)
                        + ") :[divergence free [FD]]")) {

                    line = pegarResultado.readLine();
                    if (line == null) {
                        FDRResult retorno = new FDRResult();
                        retorno.setMensagem("O arquivo CSP está com erro");
                        retorno.setResultado(false);
                        rule5.add(retorno);
                    } else {
                        FDRResult retorno = new FDRResult();
                        if (line.equals("true") || line.equals("xtrue")) {

                            retorno.setMensagem("YES");
                            retorno.setResultado(true);
                            rule5.add(retorno);
                        } else {

                            retorno.setMensagem("NO");
                            retorno.setResultado(false);
                            rule5.add(retorno);
                        }
                    }

                }
                barra.aumentar(line);
            }

        } catch (Exception e) {
            e.printStackTrace();
            JOptionPane.showMessageDialog(null, "error occurred in verifying the composition");
        }


        ruleResult.add(pegaSaídaR1(rule1));
        ruleResult.add(pegaSaídaR2(rule2));
        ruleResult.add(pegaSaídaR3(rule3));
        ruleResult.add(pegaSaídaR4(rule4));
        ruleResult.add(pegaSaídaR5(rule5));
        ruleResult.add(mensagemF.returnMensagefdr());

        for (int i = 0; i < ruleResult.size(); i++) {
            System.out.println(ruleResult.get(i).getMensagem());
            System.out.println(ruleResult.get(i).getResultado());
        }
        
        barra.finalizar();
        
        return ruleResult;
        
    }

    //I/O confluence
    private FDRResult pegaSaídaR1(ArrayList<FDRResult> r) {

        FDRResult result = new FDRResult();
        if (r.size() == 0) {
            result.setResultado(false);
            result.setMensagem("O arquivo CSP está com erro");
            return result;

        } else {
            for (int i = 0; i < r.size(); i++) {
                if (r.get(i).getResultado() == false) {
                    result.setMensagem("The protocol implementation on "
                            + eventoprotocol1
                            + "\n of the " + instance.get(0).getName()
                            + " is not a valid I/O Confluent");
                    result.setResultado(false);
                    return result;
                }
            }
        }
        result.setMensagem("The protocol implementation on "
                + eventoprotocol1
                + "\n of the " + instance.get(0).getName()
                + " is a valid I/O Confluent");
        result.setResultado(true);
        return result;
    }

    private FDRResult pegaSaídaR2(ArrayList<FDRResult> r) {

        FDRResult result = new FDRResult();
        if (r.size() == 0) {
            result.setResultado(false);
            result.setMensagem("O arquivo CSP está com erro");
            return result;

        } else {
            for (int i = 0; i < r.size(); i++) {
                if (r.get(i).getResultado() == false) {
                    result.setMensagem("The protocol implementation on "
                            + eventoprotocol2
                            + "\n of the " + instance.get(1).getName()
                            + " is not a valid I/O Confluent");
                    result.setResultado(false);
                    return result;
                }
            }
        }

        result.setMensagem("The protocol implementation on "
                + eventoprotocol2
                + "\n of the " + instance.get(1).getName()
                + " is a valid I/O Confluent");
        result.setResultado(true);
        return result;
    }

    private FDRResult pegaSaídaR3(ArrayList<FDRResult> r) {

        FDRResult result = new FDRResult();
        if (r.size() == 0) {
            result.setResultado(false);
            result.setMensagem("O arquivo CSP está com erro");
            return result;

        } else {
            for (int i = 0; i < r.size(); i++) {
                if (r.get(i).getResultado() == false) {
                    result.setMensagem("Protocols of "
                            + instance.get(0).getName()
                            + "\n aren't strongly compatible in "
                            + eventoprotocol1);
                    result.setResultado(false);
                    return result;
                }
            }
        }

        result.setMensagem("Protocols of "
                + instance.get(0).getName()
                + "\n are strongly compatible in "
                + eventoprotocol1);
        result.setResultado(true);
        return result;
    }

    private FDRResult pegaSaídaR4(ArrayList<FDRResult> r) {

        FDRResult result = new FDRResult();
        if (r.size() == 0) {
            result.setResultado(false);
            result.setMensagem("O arquivo CSP está com erro");
            return result;

        } else {
            for (int i = 0; i < r.size(); i++) {
                if (r.get(i).getResultado() == false) {
                    result.setMensagem("Protocols of "
                            + instance.get(1).getName()
                            + "\n aren't strongly compatible in "
                            + eventoprotocol2);
                    result.setResultado(false);
                    return result;
                }
            }
        }

        result.setMensagem("Protocols of "
                + instance.get(1).getName()
                + " are strongly compatible in "
                + eventoprotocol2);
        result.setResultado(true);
        return result;
    }

    private FDRResult pegaSaídaR5(ArrayList<FDRResult> r) {

        FDRResult result = new FDRResult();
        if (r.size() == 0) {
            result.setResultado(false);
            result.setMensagem("O arquivo CSP está com erro");
            return result;

        } else {
            for (int i = 0; i < r.size(); i++) {
                if (r.get(i).getResultado() == false) {
                    result.setMensagem("Protocols don't have finite output property");
                    result.setResultado(false);
                    return result;
                }
            }
        }

        result.setMensagem("Protocols have finite output property");
        result.setResultado(true);
        return result;
    }
}
/*
        System.out.println("Analyse\n\n\n");
        System.out.println("Checking " + instance.get(0).getName() + 
                        "\\{|" + instance.get(0).getChannel().get(0).getName() +
                        "|} [T= " + instance.get(0));
        System.out.println("\n\n"); 
        System.out.println("Checking STOP [T= RUN(inter(events(" + 
                       instance.get(0).getName() + "),events(" + 
                       instance.get(1).getName() + ")))");
        System.out.println("\n\n");
        System.out.println("Checking" + colocaprot.get(0)+ 
                       " :[divergence free [FD]]");
        System.out.println("\n\n");
        System.out.println("Checking" + colocaprot.get(0)+ " [F= PROT_IMP_def("
                + instance.get(0).getName() + "," + prot.get(0).getCanal().getName() + ")");
        System.out.println("\n\n");
        System.out.println("Checking PROT_IMP_def(" + instance.get(0).getName() + "," 
                       + prot.get(0).getCanal().getName()
                        + ") [FD= " + colocaprot.get(0));
        System.out.println("\n\n");
        System.out.println("Checking PROT_IMP_def(" + instance.get(0).getName() + "," 
                       + prot.get(0).getCanal().getName()
                        + ") [FD= " + colocaprot.get(0));
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(inputs_PROT_IMP(" + 
                       instance.get(0).getName() 
                + ","+prot.get(0).getCanal().getName() + "),{|" + 
                       prot.get(0).getCanal().getName()
                + "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(inputs_PROT_IMP(" + 
                       instance.get(0).getName() 
                + ","+prot.get(0).getCanal().getName() + "),{|" + 
                       prot.get(0).getCanal().getName()
                + "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(outputs_PROT_IMP(" 
                       + instance.get(0).getName() 
                + ","+prot.get(0).getCanal().getName() + "),{|" + 
                       prot.get(0).getCanal().getName()
                + "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(outputs_PROT_IMP(" 
                       + instance.get(0).getName() 
                + ","+prot.get(0).getCanal().getName() + "),{|" + 
                       prot.get(0).getCanal().getName()
                + "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(0) + ", " + 
                   prot.get(0).getCanal().getName() + ") :[deterministic [F]]");
        System.out.println("\n\n");
        System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(0) + ", " + 
                   prot.get(0).getCanal().getName() + ") :[deterministic [F]]");
        System.out.println("\n\n");
        System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(0) + ", " + 
                   prot.get(0).getCanal().getName() + ") :[deterministic [F]]");
        System.out.println("\n\n");
        System.out.println("Checking" + colocaprot.get(1)+ " [F= PROT_IMP_def("
                + instance.get(1).getName() + "," + prot.get(1).getCanal().getName() + ")");
        System.out.println("\n\n");
        System.out.println("Checking PROT_IMP_def(" + instance.get(1).getName() + "," 
                       + prot.get(1).getCanal().getName()
                        + ") [FD= " + colocaprot.get(1));
        System.out.println("\n\n");
        System.out.println("Checking PROT_IMP_def(" + instance.get(1).getName() + "," 
                       + prot.get(1).getCanal().getName()
                        + ") [FD= " + colocaprot.get(1));
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(inputs_PROT_IMP(" + 
                       instance.get(1).getName() 
                + ","+prot.get(1).getCanal().getName() + "),{|" + 
                       prot.get(1).getCanal().getName()
                + "|})) [T= ERROR"); 
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(outputs_PROT_IMP(" 
                       + instance.get(1).getName() 
                + ","+prot.get(1).getCanal().getName() + "),{|" + 
                       prot.get(1).getCanal().getName()
                + "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(1) + ", " + 
                   prot.get(1).getCanal().getName() + ") :[deterministic [F]]");
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(0) + " :[deadlock free [FD]]");
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(1) + " :[deadlock free [FD]]");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(inputs("+ 
                  colocaprot_RIO.get(0) + "),{|" + prot.get(0).getCanal().getName() +
                   "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(outputs("+ 
                  colocaprot_RIO.get(0) + "),{|" + prot.get(1).getCanal().getName() +
                   "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(inputs("+ 
                  colocaprot_RIO.get(1) + "),{|" + prot.get(1).getCanal().getName() +
                   "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(inputs("+ 
                  colocaprot_RIO.get(1) + "),{|" + prot.get(1).getCanal().getName() +
                   "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(subseteq(outputs("+ 
                  colocaprot_RIO.get(1) + "),{|" + prot.get(0).getCanal().getName() +
                   "|})) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(inputs("+ 
                  colocaprot_RIO.get(0) + " == outputs(" + colocaDual_prot_RIO.get(0)
                   + ")) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(inputs("+ 
                  colocaprot_RIO.get(0) + " == outputs(" + colocaDual_prot_RIO.get(0)
                   + ")) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(inputs("+ 
                  colocaprot_RIO.get(0) + " == outputs(" + colocaDual_prot_RIO.get(0)
                   + ")) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(outputs("+ 
                  colocaprot_RIO.get(1) + " == inputs(" + colocaDual_prot_RIO.get(1)
                   + ")) [T= ERROR");
        System.out.println("\n\n");
        System.out.println("Checking Test(outputs("+ 
                  colocaprot_RIO.get(1) + " == inputs(" + colocaDual_prot_RIO.get(1)
                   + ")) [T= ERROR");
        System.out.println("\n\n"); 
        System.out.println("Checking "+ 
                  colocaDual_prot_RIO.get(0) + " [T= " + colocaprot_RIO.get(0));
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(0) + " [T= " + colocaDual_prot_RIO.get(0));
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(0) + " [T= " + colocaDual_prot_RIO.get(0));
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(0) + " [T= " + colocaDual_prot_RIO.get(0));
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaDual_prot_RIO.get(0) + " [F= " + colocaprot_RIO.get(1));
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(1) + " [T= " + colocaDual_prot_RIO.get(0));
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(0) + "\\outputs(" + colocaprot_RIO.get(0) +
                 " :[divergence free [FD]]");
        System.out.println("\n\n");
        System.out.println("Checking "+ 
                  colocaprot_RIO.get(1) + "\\outputs(" + colocaprot_RIO.get(1) +
                 " :[divergence free [FD]]");
         
         */