/*
 * 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;
    
    public CreatorCondition_D4(LinkedList<Instance> i, LinkedList<Protocols> p){
    
        this.instance = i;
        this.prot = p;
        
        guardanomeProcessoProt_Imp = new LinkedList<>();
        pegarProtRIO = new LinkedList<>();
        creatNamePcsp = new CreatorNamesOfProcessCSP(i, p);
    }
    
    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() + "," + 
                prot.get(0).getCanal().getName() + ")";

        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() + "," + prot.get(0).getCanal().getName()
                + ") [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() 
                + ","+prot.get(0).getCanal().getName() + "),{|" + 
                prot.get(0).getCanal().getName()
                + "|})) [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() 
                + ","+prot.get(0).getCanal().getName() + "),{|" + 
                prot.get(0).getCanal().getName()
                + "|})) [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) + 
                ", " + prot.get(0).getCanal().getName() + ") :[deterministic [F]]";
        condiction = condiction + "\n\n";
       
        return condiction;
    }
}