/*
 * 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_D7 {
    
    private String condiction = "";
    private LinkedList<Protocols> prot;
    private LinkedList<Instance> instance;
    CreatorNamesOfProcessCSP creatNamePcsp;
    LinkedList<String> pegarProtRIO;
    
    public CreatorCondition_D7(LinkedList<Instance> i, LinkedList<Protocols> p){
    
        this.instance = i;
        this.prot = p;
        creatNamePcsp = new CreatorNamesOfProcessCSP(i, p);
        pegarProtRIO = new LinkedList<>();
    }
    
     public String implementationCondition_D7() {

        pegarProtRIO = creatNamePcsp.CreatorProt_RIO(); 
        
        condiction = condiction + "--D.7: Protocols have Finite Output Property \n\n";
        condiction = condiction + "--D.7.1";
        condiction = condiction + "\n\n";
        condiction = condiction + "assert " + pegarProtRIO.get(0) + " \\  outputs(" + 
                pegarProtRIO.get(0) + "):[divergence free [FD]]";
        condiction = condiction + "\n\n";
        condiction = condiction + "assert " + pegarProtRIO.get(1) + 
                " \\  outputs(" + pegarProtRIO.get(1) + "):[divergence free [FD]]";
        condiction = condiction + "\n\n";
        

        return condiction;
    }
}