Newer
Older
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
*
* ludovic.apvrille AT enst.fr
*
* This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
*
* This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info".
*
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited
* liability.
*
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
* that may mean that it is complicated to manipulate, and that also
* therefore means that it is reserved for developers and experienced
* professionals having in-depth computer knowledge. Users are therefore
* encouraged to load and test the software's suitability as regards their
* requirements in conditions enabling the security of their systems and/or
* data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security.
*
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms.
*/
package ui;
import myutil.TraceManager;
import tepe.*;
import ui.avatarpd.*;
import java.util.ListIterator;
import java.util.Vector;
* Class AvatarRequirementPanelTranslator
* Creation: 17/02/2011
* @author Ludovic APVRILLE
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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
public class AvatarRequirementPanelTranslator {
protected Vector checkingErrors, warnings;
protected CorrespondanceTGElement listE; // usual list
public AvatarRequirementPanelTranslator() {
}
public void reinit() {
checkingErrors = new Vector();
warnings = new Vector();
listE = new CorrespondanceTGElement();
}
public Vector getErrors() {
return checkingErrors;
}
public Vector getWarnings() {
return warnings;
}
public CorrespondanceTGElement getCorrespondanceTGElement() {
return listE;
}
public TEPE generateTEPESpecification(AvatarPDPanel _apdp) {
TEPE tepe = new TEPE(_apdp.getName(), _apdp);
TraceManager.addDev("Creating new TEPE named " + tepe.getName());
reinit();
makeComponents(tepe, _apdp);
makeLinksBetweenComponents(tepe, _apdp);
listE.makeTEPEIDs();
TraceManager.addDev(tepe.toString());
return tepe;
}
public void makeComponents(TEPE _tepe, AvatarPDPanel _apdp) {
TGComponent tgc;
ListIterator iterator = _apdp.getComponentList().listIterator();
while(iterator.hasNext()) {
tgc = (TGComponent)(iterator.next());
// Alias
if (tgc instanceof AvatarPDAlias) {
TEPEAliasComponent tepealiasc = new TEPEAliasComponent("Alias", tgc);
tepealiasc.setValue(tgc.getValue());
_tepe.add(tepealiasc);
listE.addCor(tepealiasc, tgc);
// Attributes
} else if (tgc instanceof AvatarPDAttribute) {
TEPEAttributeComponent tepeattributec = new TEPEAttributeComponent("Attribute", tgc, "No__Block");
tepeattributec.setValue(tgc.getValue());
_tepe.add(tepeattributec);
listE.addCor(tepeattributec, tgc);
// Setting of Attributes
} else if (tgc instanceof AvatarPDAttributeSetting) {
TEPESettingComponent tepesettingc = new TEPESettingComponent("Attribute setting", tgc);
tepesettingc.setValue(tgc.getValue());
_tepe.add(tepesettingc);
listE.addCor(tepesettingc, tgc);
// Block
} else if (tgc instanceof AvatarPDBlock) {
Vector<AvatarPDAttribute> va = ((AvatarPDBlock)tgc).getAllAvatarPDAttribute();
for(AvatarPDAttribute attr: va) {
TEPEAttributeComponent tepeattributec = new TEPEAttributeComponent("Attribute", attr, attr.getFather().getValue());
tepeattributec.setValue(attr.getValue());
_tepe.add(tepeattributec);
listE.addCor(tepeattributec, attr);
}
Vector<AvatarPDSignal> vs = ((AvatarPDBlock)tgc).getAllAvatarPDSignal();
for(AvatarPDSignal sig: vs) {
TEPESignalComponent tepesignalc = new TEPESignalComponent("Signal", sig, sig.getFather().getValue());
tepesignalc.setValue(sig.getValue());
_tepe.add(tepesignalc);
listE.addCor(tepesignalc, sig);
}
// Equations
} else if (tgc instanceof AvatarPDBoolEq) {
TEPEEquationComponent tepeequationc = new TEPEEquationComponent("Equation", tgc);
tepeequationc.setValue(tgc.getValue());
_tepe.add(tepeequationc);
listE.addCor(tepeequationc, tgc);
// Logical constraint
} else if (tgc instanceof AvatarPDLogicalConstraint) {
AvatarPDLogicalConstraint apdlc = (AvatarPDLogicalConstraint)tgc;
TEPELogicalConstraintComponent tepelogicalc;
if (apdlc.getValue().compareTo(AvatarPDLogicalConstraint.STEREOTYPES[0]) ==0) {
// no sequence
tepelogicalc = new TEPELogicalConstraintComponent("Logical constraint", tgc, TEPELogicalConstraintComponent.NO_SEQUENCE);
} else {
// Sequence
tepelogicalc = new TEPELogicalConstraintComponent("Logical sequence", tgc, TEPELogicalConstraintComponent.SEQUENCE);
}
tepelogicalc.setValue(tgc.getValue());
_tepe.add(tepelogicalc);
listE.addCor(tepelogicalc, tgc);
// Property
} else if (tgc instanceof AvatarPDProperty) {
AvatarPDProperty apdp = (AvatarPDProperty)tgc;
int type = 0;
if (apdp.isLiveness()) {
type = TEPEPropertyComponent.LIVENESS;
} else if (apdp.isNotLiveness()) {
type = TEPEPropertyComponent.NON_LIVENESS;
} else if (apdp.isRechability()) {
type = TEPEPropertyComponent.REACHABILITY;
} else if (apdp.isNotRechability()) {
type = TEPEPropertyComponent.NON_REACHABILITY;
} else if (apdp.isSafety()) {
type = TEPEPropertyComponent.SAFETY;
} else if (apdp.isNotSafety()) {
type = TEPEPropertyComponent.NON_SAFETY;
}
TEPEPropertyComponent tepepropertyc = new TEPEPropertyComponent("Property", tgc, type);
tepepropertyc.setValue(tgc.getValue());
_tepe.add(tepepropertyc);
listE.addCor(tepepropertyc, tgc);
// Operators between properties
} else if (tgc instanceof AvatarPDPropertyRelation) {
AvatarPDPropertyRelation apdpr = (AvatarPDPropertyRelation)tgc;
int type = 0;
if (apdpr.isOr()) {
type = TEPEPropertyOperatorComponent.OR;
} else if (apdpr.isAnd()) {
type = TEPEPropertyOperatorComponent.AND;
} else if (apdpr.isImply()) {
type = TEPEPropertyOperatorComponent.IMPLY;
} else if (apdpr.isEquivalent()) {
type = TEPEPropertyOperatorComponent.EQUIVALENT;
}
TEPEPropertyOperatorComponent tepepropertyoperatorc = new TEPEPropertyOperatorComponent("Property operator", tgc, type);
tepepropertyoperatorc.setValue(tgc.getValue());
_tepe.add(tepepropertyoperatorc);
listE.addCor(tepepropertyoperatorc, tgc);
// Signal
} else if (tgc instanceof AvatarPDSignal) {
TEPESignalComponent tepesignalc = new TEPESignalComponent("Signal", tgc, tgc.getFather().getValue());
tepesignalc.setValue(tgc.getValue());
_tepe.add(tepesignalc);
listE.addCor(tepesignalc, tgc);
// Temporal constraint
} else if (tgc instanceof AvatarPDTemporalConstraint) {
TEPETimeConstraintComponent tepetimeconstraintc = new TEPETimeConstraintComponent("Time Constraint", tgc);
tepetimeconstraintc.setValue(tgc.getValue());
_tepe.add(tepetimeconstraintc);
listE.addCor(tepetimeconstraintc, tgc);
}
}
}
public void makeLinksBetweenComponents(TEPE _tepe, AvatarPDPanel _apdp) {
TGComponent tgc, tgc1, tgc2;
ListIterator iterator = _apdp.getComponentList().listIterator();
TEPEComponent element1, element2;
while(iterator.hasNext()) {
tgc = (TGComponent)(iterator.next());
if (tgc instanceof AvatarPDAttributeConnector) {
AvatarPDAttributeConnector apdaco = (AvatarPDAttributeConnector)tgc;
tgc1 = _apdp.getComponentToWhichBelongs(apdaco.getTGConnectingPointP1());
tgc2 = _apdp.getComponentToWhichBelongs(apdaco.getTGConnectingPointP2());
if ((tgc1 == null) || (tgc2 == null)) {
TraceManager.addDev("Tgcs null in Avatar translation");
} else {
element1 = (TEPEComponent)(listE.getObject(tgc1));
element2 = (TEPEComponent)(listE.getObject(tgc2));
if ((element1 != null) && (element2 != null)) {
//TraceManager.addDev("Adding output / input");
element1.addOutAttributeComponent(element2);
element2.addInAttributeComponent(element1);
}
}
} else if (tgc instanceof AvatarPDPropertyConnector) {
AvatarPDPropertyConnector apdpco = (AvatarPDPropertyConnector)tgc;
tgc1 = _apdp.getComponentToWhichBelongs(apdpco.getTGConnectingPointP1());
tgc2 = _apdp.getComponentToWhichBelongs(apdpco.getTGConnectingPointP2());
if ((tgc1 == null) || (tgc2 == null)) {
TraceManager.addDev("Tgcs null in Avatar translation");
} else {
element1 = (TEPEComponent)(listE.getObject(tgc1));
element2 = (TEPEComponent)(listE.getObject(tgc2));
if ((element1 != null) && (element2 != null)) {
//TraceManager.addDev("Adding output / input");
element1.addOutPropertyComponent(element2);
// Must know whether it is negated, or not
if (!(tgc2 instanceof AvatarPDPropertyRelation)) {
element2.addInPropertyComponent(element1);
if (apdpco.isNegated()) {
} else {
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
}
}
}
}
} else if (tgc instanceof AvatarPDSignalConnector) {
AvatarPDSignalConnector apdsco = (AvatarPDSignalConnector)tgc;
tgc1 = _apdp.getComponentToWhichBelongs(apdsco.getTGConnectingPointP1());
tgc2 = _apdp.getComponentToWhichBelongs(apdsco.getTGConnectingPointP2());
if ((tgc1 == null) || (tgc2 == null)) {
TraceManager.addDev("Tgcs null in Avatar translation");
} else {
element1 = (TEPEComponent)(listE.getObject(tgc1));
element2 = (TEPEComponent)(listE.getObject(tgc2));
if ((element1 != null) && (element2 != null)) {
element1.addOutSignalComponent(element2);
// Must know whether it is negated, or not
if (apdsco.getTGConnectingPointP2() instanceof AvatarPDForbiddenSignalConnectingPoint) {
element2.addInNegatedSignalComponent(element1);
} else {
// Must enforce order of connectors
if ((tgc2 instanceof AvatarPDLogicalConstraint) || (tgc2 instanceof AvatarPDTemporalConstraint)) {
// Must enforce order of connectors
// Done afterwards
} else {
element2.addInSignalComponent(element1);
}
}
}
}
}
}
// Enforcing order in AvatarPDLogicalConstraint
iterator = _apdp.getComponentList().listIterator();
TGConnector tgco;
while(iterator.hasNext()) {
tgc = (TGComponent)(iterator.next());
if (tgc instanceof AvatarPDLogicalConstraint) {
for(int i=2; i<8; i++) {
tgco = _apdp.getConnectorConnectedTo(tgc.getTGConnectingPointAtIndex(i));
if (tgco != null) {
AvatarPDSignalConnector apdsco = (AvatarPDSignalConnector)tgco;
tgc1 = _apdp.getComponentToWhichBelongs(apdsco.getTGConnectingPointP1());
element1 = (TEPEComponent)(listE.getObject(tgc1));
element2 = (TEPEComponent)(listE.getObject(tgc));
if ((element1 != null) && (element2 != null)) {
element2.addInSignalComponent(element1);
}
}
}
} else if (tgc instanceof AvatarPDTemporalConstraint) {
for(int i=2; i<4; i++) {
tgco = _apdp.getConnectorConnectedTo(tgc.getTGConnectingPointAtIndex(i));
if (tgco != null) {
AvatarPDSignalConnector apdsco = (AvatarPDSignalConnector)tgco;
tgc1 = _apdp.getComponentToWhichBelongs(apdsco.getTGConnectingPointP1());
element1 = (TEPEComponent)(listE.getObject(tgc1));
element2 = (TEPEComponent)(listE.getObject(tgc));
if ((element1 != null) && (element2 != null)) {
element2.addInSignalComponent(element1);
}
}
}
} else if (tgc instanceof AvatarPDPropertyRelation) {
for(int i=0; i<8; i++) {
tgco = _apdp.getConnectorConnectedTo(tgc.getTGConnectingPointAtIndex(i));
if (tgco != null) {
AvatarPDPropertyConnector apdpco = (AvatarPDPropertyConnector)tgco;
tgc1 = _apdp.getComponentToWhichBelongs(apdpco.getTGConnectingPointP1());
element1 = (TEPEComponent)(listE.getObject(tgc1));
element2 = (TEPEComponent)(listE.getObject(tgc));
if ((element1 != null) && (element2 != null)) {
element2.addInPropertyComponent(element1);
if (apdpco.isNegated()) {
} else {