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

import LOGIC.Instance;
import LOGIC.Protocols;
import java.util.LinkedList;

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

    private String condiction = "";
    private LinkedList<Protocols> prot;
    private LinkedList<Instance> instance;
    private LinkedList<String> guardanomeProcessoProt_Imp;
    private LinkedList<String> pegarProtRIO;
    private CreatorNamesOfProcessCSP creatNamePcsp;
     private LinkedList<String> nomecanal;
     private String eventoprotocol2 = "";
    public CreatorCondition_D5(LinkedList<Instance> i, LinkedList<Protocols> p) {

        this.instance = i;
        this.prot = p;
        nomecanal = new LinkedList<>();
        nomecanal.add(p.get(1).getCanal().getName().replace(".", "_"));
        guardanomeProcessoProt_Imp = new LinkedList<>();
        pegarProtRIO = new LinkedList<>();
        creatNamePcsp = new CreatorNamesOfProcessCSP(i, p);
          //pegando o nome do evento que passei por paramentro no protocolo 
        int pr1, pr2;

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

    // 4  e 5 são a mesma coisa, cada um para um componente
    public String implementationCondiction_D5() {

        guardanomeProcessoProt_Imp = creatNamePcsp.CreatorProt_Name();

        pegarProtRIO = creatNamePcsp.CreatorProt_RIO();

        //Finding a valid protocol implementation
        //D.5 : I/O confluence for second component
        //D.5.1 : It is divergence-free
        condiction = condiction + "--D.5 : I/O confluence for second component \n";
        condiction = condiction + "--D.5.1 \n";
        condiction = condiction + "\n\n";
        condiction = condiction + "assert " + guardanomeProcessoProt_Imp.get(1)
                + " :[divergence free [FD]]";
        condiction = condiction + "\n\n";

        //D.5.2 : It is refined by the projection on the channel

        condiction = condiction + "--D.5.2 \n";

        //
        condiction = condiction + "\n";
        condiction = condiction + "assert " + guardanomeProcessoProt_Imp.get(1)
                + " [F= PROT_IMP_def("
                + instance.get(1).getName() + ","
                + eventoprotocol2 + ")";
        condiction = condiction + "\n\n";

        //D.5.3 : It is a refinement of the projection on the channel

        condiction = condiction + "--D.5.3 \n";
        //

        condiction = condiction + "\n";
        condiction = condiction + "assert PROT_IMP_def(" + instance.get(1).getName() + 
                "," + eventoprotocol2
                + ") [FD= " + guardanomeProcessoProt_Imp.get(1);
        condiction = condiction + "\n\n";

        //D.5.4 : It is a port-protocol (communication protocol)
        //D.5.4.1 : inputs
        //D.5.4.2 : outputs
        condiction = condiction + "--D.5.4 \n";

        condiction = condiction + "\n\n";

        condiction = condiction + "--D.5.4.1 \n";
        condiction = condiction + "assert not Test(subseteq(inputs_PROT_IMP("
                + instance.get(1).getName()
                + "," + eventoprotocol2
                + "),{|" + eventoprotocol2
                + "|})) [T= ERROR";

        condiction = condiction + "\n\n";
        condiction = condiction + "--D.5.4.2 \n";
        condiction = condiction + "assert not Test(subseteq(outputs_PROT_IMP("
                + instance.get(1).getName()
                + "," + eventoprotocol2 + "),{|"
                + eventoprotocol2
                + "|})) [T= ERROR";

        condiction = condiction + "\n\n";

        condiction = condiction + "--D.5.5 : The renamed version is I/O Confluent";
        condiction = condiction + "\n\n";

        condiction = condiction + "assert InBufferProt("
                + pegarProtRIO.get(1)
                + ", " + eventoprotocol2
                + ") :[deterministic [F]]";
        condiction = condiction + "\n\n";


        return condiction;
    }
}