/*
 * 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;
    
    public CreatorCondition_D5(LinkedList<Instance> i, LinkedList<Protocols> p){
    
        this.instance = i;
        this.prot = p;
        
        guardanomeProcessoProt_Imp = new LinkedList<>();
        pegarProtRIO = new LinkedList<>();
        creatNamePcsp = new CreatorNamesOfProcessCSP(i, p);
    }
    
    
    // 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() + "," + 
                prot.get(1).getCanal().getName() + ")";
        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() + "," + prot.get(1).getCanal().getName()
                + ") [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() 
                + ","+prot.get(1).getCanal().getName() +
                "),{|" + prot.get(1).getCanal().getName()
                + "|})) [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() 
                + ","+prot.get(1).getCanal().getName() + "),{|" 
                + prot.get(1).getCanal().getName()
                + "|})) [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) + 
                ", " + prot.get(1).getCanal().getName() + 
                ") :[deterministic [F]]";
        condiction = condiction + "\n\n";


        return condiction;
    }
}