Madiel de Souza Conserva Filho / bts

c4161db02119122d3b671aed432601cd64fd2566.svn-base 4.16 KB
edit raw blame history 
   1
   2
   3
   4
   5
   6
   7
   8
   9
  10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
  21
  22
  23
  24
  25
  26
  27
  28
  29
  30
  31
  32
  33
  34
  35
  36
  37
  38
  39
  40
  41
  42
  43
  44
  45
  46
  47
  48
  49
  50
  51
  52
  53
  54
  55
  56
  57
  58
  59
  60
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  93
  94
  95
  96
  97
  98
  99
 100
 101
 102
 103
 104
 105
 106
 107
 108
/*
 * 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;
    }
}