/*
 * 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_D4 {

    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 eventoprotocol1 = "";

    public CreatorCondition_D4(LinkedList<Instance> i, LinkedList<Protocols> p) {

        this.instance = i;
        this.prot = p;

        nomecanal = new LinkedList<>();
        nomecanal.add(p.get(0).getCanal().getName().replace(".", "_"));
        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(0).getProtocol().indexOf("(");
        pr2 = p.get(0).getProtocol().lastIndexOf(")");
        eventoprotocol1 = p.get(0).getProtocol().substring(pr1 + 1, pr2);


    }

    public String implementationCondiction_D4() {

        guardanomeProcessoProt_Imp = creatNamePcsp.CreatorProt_Name();
        pegarProtRIO = creatNamePcsp.CreatorProt_RIO();
        //Finding a valid protocol implementation
        //D.4 : I/O confluence for first component
        //D.4.1 : It is divergence-free
        condiction = condiction + "--D.4 : I/O confluence for first component";
        condiction = condiction + "\n";
        condiction = condiction + "--D.4.1 It is divergence-free\n";
        condiction = condiction + "\n\n";
        condiction = condiction + "assert " + guardanomeProcessoProt_Imp.get(0)
                + " :[divergence free [FD]]";
        condiction = condiction + "\n\n";

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

        condiction = condiction + "--D.4.2 It is refined by the projection on the channel \n";
        condiction = condiction + "\n";
        condiction = condiction + "assert "
                + guardanomeProcessoProt_Imp.get(0) + " [F= PROT_IMP_def("
                + instance.get(0).getName() + ","
                + eventoprotocol1 + ")";

        condiction = condiction + "\n\n";

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

        condiction = condiction + "--D.4.3 It is a refinement of the projection on the channel \n";
        condiction = condiction + "\n";
        condiction = condiction + "assert PROT_IMP_def("
                + instance.get(0).getName() + "," + eventoprotocol1
                + ") [FD= " + guardanomeProcessoProt_Imp.get(0);

        condiction = condiction + "\n\n";

        //D.4.4 : It is a port-protocol (communication protocol)
        //D.4.4.1 : inputs
        //D.4.4.2 : outputs
        condiction = condiction + "--D.4.4 It is a port-protocol (communication protocol) \n";

        condiction = condiction + "\n\n";

        condiction = condiction + "--D.4.4.1 \n";
        condiction = condiction + "assert not Test(subseteq(inputs_PROT_IMP("
                + instance.get(0).getName()
                + "," + eventoprotocol1 + "),{|"
                + eventoprotocol1
                + "|})) [T= ERROR";
        condiction = condiction + "\n\n";
        condiction = condiction + "--D.4.4.2 \n";
        //assert not Test(subseteq(outputs_PROT_IMP(Controller,write.1), {| write |})) [T= ERROR
        condiction = condiction + "assert not Test(subseteq(outputs_PROT_IMP("
                + instance.get(0).getName()
                + "," + eventoprotocol1 + "),{|"
                + eventoprotocol1
                + "|})) [T= ERROR";
        condiction = condiction + "\n\n";

        //D.4.5 : The renamed version is I/O Confluent

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


        //Condition D.4.5: The renamed version is I/O Confluent

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

        return condiction;
    }
}