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

    private String condiction = "";
    private LinkedList<Protocols> prot;
    private LinkedList<Instance> instance;
    private CreatorNamesOfProcessCSP creatNamePcsp;
    private LinkedList<String> pegarProtRIO;
    private CreatorNamesOfProcessCSP creatorNameProcessCsp;
    private LinkedList<String> pegarDualProtRIO;
    //private LinkedList<String> pegarDualProt;
    private LinkedList<String> nomecanal;
    private String eventoprotocol1 = "";
    private String eventoprotocol2 = "";
    private String canal1 = "";
    private String canal2 = "";

    public CreatorCondition_D6(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(".", "_"));

        creatNamePcsp = new CreatorNamesOfProcessCSP(i, p);
        pegarProtRIO = new LinkedList<>();
        creatorNameProcessCsp = new CreatorNamesOfProcessCSP(i, p);

        //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);


        pegarProtRIO = creatorNameProcessCsp.CreatorProt_RIO();

        pegarDualProtRIO = creatorNameProcessCsp.CreatorDual_Prot_RIO();
        //pegando o nome do canal 
        int can1, can2, can3, can4;

        can1 = p.get(0).getProtocol().indexOf("(");
        can2 = p.get(0).getProtocol().lastIndexOf(".");
        canal1 = p.get(0).getProtocol().substring(can1 + 1, can2);

        can3 = p.get(1).getProtocol().indexOf("(");
        can4 = p.get(1).getProtocol().lastIndexOf(".");
        canal2 = p.get(1).getProtocol().substring(can3 + 1, can4);
    }

    public String implementationCondition_D6_1() {



        condiction = condiction + "---- D.6: Protocols are Strong Compatible";
        condiction = condiction + "\n";

        condiction = condiction + "assert " + pegarProtRIO.get(0)
                + " :[deadlock free [FD]]";
        condiction = condiction + "\n\n";


        condiction = condiction + "----	 * D.6.2: Protocols are communication protocols";
        condiction = condiction + "\n";

        condiction = condiction + "assert not Test(subseteq(inputs("
                + pegarProtRIO.get(0) + "), {| "
                + canal1 + "|})) [T= ERROR";
        condiction = condiction + "\n";

        condiction = condiction + "assert not Test(subseteq(outputs("
                + pegarProtRIO.get(0) + "), {|"
                + canal2 + "|})) [T= ERROR";
        condiction = condiction + "\n";



        condiction = condiction + "assert not Test(inputs("
                + pegarProtRIO.get(0) + ") == outputs("
                + pegarDualProtRIO.get(0) + ")) [T= ERROR";
        condiction = condiction + "\n\n";



        condiction = condiction + "assert not Test(outputs("
                + pegarProtRIO.get(0) + ") == inputs("
                + pegarDualProtRIO.get(0) + ")) [T= ERROR";
        condiction = condiction + "\n\n";


        condiction = condiction + "assert " + pegarDualProtRIO.get(0)
                + " [T= " + pegarProtRIO.get(0);
        condiction = condiction + "\n\n";

        condiction = condiction + "assert " + pegarProtRIO.get(0)
                + " [T= " + pegarDualProtRIO.get(0);
        condiction = condiction + "\n\n";

        condiction = condiction + "\n\n";

        condiction = condiction + "assert " + pegarDualProtRIO.get(0)
                + " [F= " + pegarProtRIO.get(1);
        condiction = condiction + "\n\n";

        condiction = condiction + "\n\n";

        condiction = condiction + "assert " + pegarProtRIO.get(1)
                + " [F= " + pegarDualProtRIO.get(0);
        condiction = condiction + "\n\n";


        return condiction;



    }

    public String implementationCondition_D6_2() {


        condiction = condiction + "assert " + pegarProtRIO.get(1)
                + " :[deadlock free [FD]]";
        condiction = condiction + "\n\n";

        condiction = condiction + "assert not Test(subseteq(inputs("
                + pegarProtRIO.get(1) + "), {| "
                + canal2 + "|})) [T= ERROR";
        condiction = condiction + "\n";


        condiction = condiction + "assert not Test(subseteq(outputs("
                + pegarProtRIO.get(1) + "), {| "
                + canal1 + "|})) [T= ERROR";
        condiction = condiction + "\n";

        condiction = condiction + "assert not Test(inputs("
                + pegarProtRIO.get(1) + ") == outputs("
                + pegarDualProtRIO.get(1) + ")) [T= ERROR";
        condiction = condiction + "\n";

        condiction = condiction + "assert not Test(outputs("
                + pegarProtRIO.get(1) + ") == inputs("
                + pegarDualProtRIO.get(1) + ")) [T= ERROR";
        condiction = condiction + "\n";

        condiction = condiction + "assert " + pegarDualProtRIO.get(1)
                + " [T= " + pegarProtRIO.get(1);
        condiction = condiction + "\n\n";

        condiction = condiction + "assert " + pegarProtRIO.get(1)
                + " [T= " + pegarDualProtRIO.get(1);
        condiction = condiction + "\n\n";

        condiction = condiction + "\n\n";

        condiction = condiction + "assert " + pegarDualProtRIO.get(1)
                + " [F= " + pegarProtRIO.get(0);
        condiction = condiction + "\n\n";

        condiction = condiction + "\n\n";

        condiction = condiction + "assert " + pegarProtRIO.get(0)
                + " [F= " + pegarDualProtRIO.get(1);
        condiction = condiction + "\n\n";


        return condiction;

    }
}