Madiel de Souza Conserva Filho / bts

Blame view

BRIC/.svn/pristine/e0/e001961308f2e4aa41f407040fc2ac12d66b351e.svn-base 4.68 KB
edit raw normal view history
eeb5cac08   Madiel de Souza Conserva Filho   first 
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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
 
  /*
   * 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;
      private LinkedList<String> nomecanal;
      private String eventoprotocol1 = "";
      private String canalprot = "";
  
      public CreatorCondition_D4(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(".", "_"));
          guardanomeProcessoProt_Imp = new LinkedList<>();
          pegarProtRIO = new LinkedList<>();
          creatNamePcsp = new CreatorNamesOfProcessCSP(i, p);
  
          //pegando o nome do evento que passei por paramentro no protocolo 
          int pr1, pr2;
  
          pr1 = p.get(0).getProtocol().indexOf("(");
          pr2 = p.get(0).getProtocol().lastIndexOf(")");
          eventoprotocol1 = p.get(0).getProtocol().substring(pr1 + 1, pr2);
          //pega apenas o canal
          int can1, can2;
          can1 = p.get(0).getProtocol().indexOf("(");
          can2 = p.get(0).getProtocol().lastIndexOf(".");
          canalprot = p.get(0).getProtocol().substring(can1 + 1, can2);
      }
  
      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 + "
  ";
          condiction = condiction + "--D.4.1 It is divergence-free
  ";
          condiction = condiction + "
  
  ";
          condiction = condiction + "assert " + guardanomeProcessoProt_Imp.get(0)
                  + " :[divergence free [FD]]";
          condiction = condiction + "
  
  ";
  
          //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 
  ";
          condiction = condiction + "
  ";
          condiction = condiction + "assert "
                  + guardanomeProcessoProt_Imp.get(0) + " [F= PROT_IMP_def("
                  + instance.get(0).getName() + ","
                  + eventoprotocol1 + ")";
  
          condiction = condiction + "
  
  ";
  
          //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 
  ";
          condiction = condiction + "
  ";
          condiction = condiction + "assert PROT_IMP_def("
                  + instance.get(0).getName() + "," + eventoprotocol1
                  + ") [FD= " + guardanomeProcessoProt_Imp.get(0);
  
          condiction = condiction + "
  
  ";
  
          //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) 
  ";
  
          condiction = condiction + "
  
  ";
  
          condiction = condiction + "--D.4.4.1 
  ";
          condiction = condiction + "assert not Test(subseteq(inputs_PROT_IMP("
                  + instance.get(0).getName()
                  + "," + eventoprotocol1 + "),{|"
                  + canalprot
                  + "|})) [T= ERROR";
          condiction = condiction + "
  
  ";
          condiction = condiction + "--D.4.4.2 
  ";
          //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()
                  + "," + eventoprotocol1 + "),{|"
                  + canalprot
                  + "|})) [T= ERROR";
          condiction = condiction + "
  
  ";
  
          //D.4.5 : The renamed version is I/O Confluent
  
          condiction = condiction + "--D.4.5 : The renamed version is I/O Confluent";
          condiction = condiction + "
  
  ";
          //     
  
  
          //Condition D.4.5: The renamed version is I/O Confluent
  
          condiction = condiction + "assert InBufferProt(" + pegarProtRIO.get(0)
                  + ", " + eventoprotocol1 + ") :[deterministic [F]]";
          condiction = condiction + "
  
  ";
  
          return condiction;
      }
  }