1
2
3
4
5
6
7
8
9
10
11
12
13
14
15 package org.overturetool.traces;
16
17
18
19
20
21 import jp.co.csk.vdm.toolbox.VDM.*;
22 import java.util.*;
23 import org.overturetool.ast.imp.*;
24 import org.overturetool.ast.itf.*;
25
26 import org.overturetool.traces.API.*;
27 import org.overturetool.traces.*;
28 import org.overturetool.traces.io.*;
29 import org.overturetool.traces.toolbox.*;
30 import org.overturetool.traces.astspec.oml2vpp.*;
31
32
33
34 @SuppressWarnings("unchecked")
35 public class DEF {
36
37
38
39 public static class Name implements Record {
40
41 public String clnm;
42
43 public String tnm;
44
45
46 public Name () {}
47
48
49 public Name (String p1, String p2) {
50
51 clnm = p1;
52 tnm = p2;
53 }
54
55
56 public Object clone () {
57 return new Name(clnm, tnm);
58 }
59
60
61 public String toString () {
62 return "mk_DEF`Name(" + UTIL.toString(clnm) + "," + UTIL.toString(tnm) + ")";
63 }
64
65
66 public boolean equals (Object obj) {
67 if (!(obj instanceof Name))
68 return false;
69 else {
70
71 Name temp = (Name) obj;
72 return UTIL.equals(clnm, temp.clnm) && UTIL.equals(tnm, temp.tnm);
73 }
74 }
75
76
77 public int hashCode () {
78 return (clnm == null ? 0 : clnm.hashCode()) + (tnm == null ? 0 : tnm.hashCode());
79 }
80
81 }
82
83 ;
84
85
86 static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
87
88
89
90 private HashMap valm = new HashMap();
91
92
93
94 private HashMap inherit = new HashMap();
95
96
97
98 private HashMap recdefs = new HashMap();
99
100
101
102 private RTERR errorLog = null;
103
104
105
106
107 private void vdm_init_DEF () throws CGException {
108 try {
109
110 valm = new HashMap();
111 inherit = new HashMap();
112 recdefs = new HashMap();
113 }
114 catch (Exception e){
115
116 e.printStackTrace(System.out);
117 System.out.println(e.getMessage());
118 }
119 }
120
121
122
123
124 public DEF () throws CGException {
125 vdm_init_DEF();
126 }
127
128
129
130
131 public DEF (final IOmlSpecifications spec, final RTERR errLog) throws CGException {
132
133 vdm_init_DEF();
134 {
135
136 errorLog = (RTERR) UTIL.clone(errLog);
137 ExpandSpec((IOmlSpecifications) spec);
138 }
139 }
140
141
142
143
144 public void ExpandSpec (final IOmlSpecifications spec) throws CGException {
145
146 Vector sq_2 = null;
147 sq_2 = spec.getClassList();
148 IOmlClass cl = null;
149 for (Iterator enm_30 = sq_2.iterator(); enm_30.hasNext(); ) {
150
151 IOmlClass elem_3 = (IOmlClass) enm_30.next();
152 cl = (IOmlClass) elem_3;
153 {
154
155 String id = null;
156 id = cl.getIdentifier();
157 Vector supers = null;
158 Boolean cond_10 = null;
159 cond_10 = cl.hasInheritanceClause();
160 if (cond_10.booleanValue()) {
161
162 IOmlInheritanceClause obj_11 = null;
163 obj_11 = (IOmlInheritanceClause) cl.getInheritanceClause();
164 supers = obj_11.getIdentifierList();
165 }
166 else
167 supers = new Vector();
168 Vector body = null;
169 body = cl.getClassBody();
170 {
171
172 valm.put(id, ExpandValueMap(body));
173 HashMap rhs_17 = new HashMap();
174 HashMap modmap_18 = new HashMap();
175 modmap_18 = ExpandRecTypeDefs(id, body);
176 rhs_17 = new HashMap(recdefs);
177 rhs_17.putAll(modmap_18);
178 recdefs = (HashMap) UTIL.clone(rhs_17);
179 HashSet rhs_23 = new HashSet();
180 HashSet set_25 = new HashSet();
181 Enumeration enm_26 = supers.elements();
182 while ( enm_26.hasMoreElements())
183 set_25.add(enm_26.nextElement());
184 rhs_23 = set_25;
185 inherit.put(id, rhs_23);
186 }
187 }
188 }
189 }
190
191
192
193
194 private HashMap ExpandValueMap (final Vector body_ul) throws CGException {
195
196 HashMap v_um = new HashMap();
197 {
198
199 IOmlDefinitionBlock body = null;
200 for (Iterator enm_21 = body_ul.iterator(); enm_21.hasNext(); ) {
201
202 IOmlDefinitionBlock elem_3 = (IOmlDefinitionBlock) enm_21.next();
203 body = (IOmlDefinitionBlock) elem_3;
204 if (new Boolean(body instanceof OmlValueDefinitions).booleanValue()) {
205
206 HashMap rhs_15 = new HashMap();
207 HashMap modmap_16 = new HashMap();
208 modmap_16 = ExpandValueDef((IOmlValueDefinitions) body);
209 rhs_15 = new HashMap(v_um);
210 rhs_15.putAll(modmap_16);
211 v_um = (HashMap) UTIL.clone(rhs_15);
212 }
213 else {
214 if (new Boolean(body instanceof OmlInstanceVariableDefinitions).booleanValue()) {
215
216 HashMap rhs_10 = new HashMap();
217 HashMap modmap_11 = new HashMap();
218 modmap_11 = ExpandInstVarDef((IOmlInstanceVariableDefinitions) body);
219 rhs_10 = new HashMap(v_um);
220 rhs_10.putAll(modmap_11);
221 v_um = (HashMap) UTIL.clone(rhs_10);
222 }
223 }
224 }
225 }
226 return v_um;
227 }
228
229
230
231
232 private HashMap ExpandValueDef (final IOmlValueDefinitions body) throws CGException {
233
234 HashMap v_um = new HashMap();
235 {
236
237 Vector sq_2 = null;
238 sq_2 = body.getValueList();
239 IOmlValueDefinition vdef = null;
240 for (Iterator enm_23 = sq_2.iterator(); enm_23.hasNext(); ) {
241
242 IOmlValueDefinition elem_3 = (IOmlValueDefinition) enm_23.next();
243 vdef = (IOmlValueDefinition) elem_3;
244 {
245
246 IOmlValueShape shape = null;
247 shape = (IOmlValueShape) vdef.getShape();
248 IOmlPattern pat = null;
249 pat = (IOmlPattern) shape.getPattern();
250 IOmlExpression tmpVal_9 = null;
251 tmpVal_9 = (IOmlExpression) shape.getExpression();
252 IOmlExpression expr = null;
253 expr = (IOmlExpression) tmpVal_9;
254 if (new Boolean(pat instanceof OmlPatternIdentifier).booleanValue()) {
255
256 HashMap rhs_16 = new HashMap();
257 HashMap modmap_17 = new HashMap();
258 modmap_17 = MatchPatId2Expr((IOmlPatternIdentifier) pat, (IOmlExpression) expr);
259 rhs_16 = new HashMap(v_um);
260 rhs_16.putAll(modmap_17);
261 v_um = (HashMap) UTIL.clone(rhs_16);
262 }
263 else
264 errorLog.ReportInternalError(pat, UTIL.ConvertToString(RTERR.ONLY_uID_uSUPPORTED), new Boolean(false));
265 }
266 }
267 }
268 return v_um;
269 }
270
271
272
273
274 private HashMap ExpandInstVarDef (final IOmlInstanceVariableDefinitions body) throws CGException {
275
276 HashMap v_um = new HashMap();
277 {
278
279 Vector sq_2 = null;
280 sq_2 = body.getVariablesList();
281 IOmlInstanceVariableShape instdef = null;
282 for (Iterator enm_23 = sq_2.iterator(); enm_23.hasNext(); ) {
283
284 IOmlInstanceVariableShape elem_3 = (IOmlInstanceVariableShape) enm_23.next();
285 instdef = (IOmlInstanceVariableShape) elem_3;
286 if (new Boolean(!new Boolean(instdef instanceof OmlInstanceVariableInvariant).booleanValue()).booleanValue()) {
287
288 OmlInstanceVariable instdef2 = (OmlInstanceVariable) instdef;
289 IOmlAssignmentDefinition idef = null;
290 idef = (IOmlAssignmentDefinition) instdef2.getAssignmentDefinition();
291 String id = null;
292 id = idef.getIdentifier();
293 IOmlExpression tmpVal_13 = null;
294 Boolean cond_15 = null;
295 cond_15 = idef.hasExpression();
296 if (cond_15.booleanValue())
297 tmpVal_13 = (IOmlExpression) idef.getExpression();
298 else
299 tmpVal_13 = null;
300 IOmlExpression expr = null;
301 expr = (IOmlExpression) tmpVal_13;
302 if (new Boolean(!UTIL.equals(expr, null)).booleanValue())
303 v_um.put(id, expr);
304 }
305 }
306 }
307 return v_um;
308 }
309
310
311
312
313 private HashMap ExpandRecTypeDefs (final String clnm, final Vector body_ul) throws CGException {
314
315 HashMap r_um = new HashMap();
316 {
317
318 IOmlDefinitionBlock body = null;
319 for (Iterator enm_16 = body_ul.iterator(); enm_16.hasNext(); ) {
320
321 IOmlDefinitionBlock elem_4 = (IOmlDefinitionBlock) enm_16.next();
322 body = (IOmlDefinitionBlock) elem_4;
323 if (new Boolean(body instanceof OmlTypeDefinitions).booleanValue()) {
324
325 HashMap rhs_9 = new HashMap();
326 HashMap modmap_10 = new HashMap();
327 modmap_10 = ExpandTypeDefs(clnm, (IOmlTypeDefinitions) body);
328 rhs_9 = new HashMap(r_um);
329 rhs_9.putAll(modmap_10);
330 r_um = (HashMap) UTIL.clone(rhs_9);
331 }
332 }
333 }
334 return r_um;
335 }
336
337
338
339
340 private HashMap ExpandTypeDefs (final String clnm, final IOmlTypeDefinitions body) throws CGException {
341
342 HashMap r_um = new HashMap();
343 {
344
345 Vector sq_3 = null;
346 sq_3 = body.getTypeList();
347 IOmlTypeDefinition tdef = null;
348 for (Iterator enm_18 = sq_3.iterator(); enm_18.hasNext(); ) {
349
350 IOmlTypeDefinition elem_4 = (IOmlTypeDefinition) enm_18.next();
351 tdef = (IOmlTypeDefinition) elem_4;
352 {
353
354 IOmlTypeShape shape = null;
355 shape = (IOmlTypeShape) tdef.getShape();
356 if (new Boolean(shape instanceof OmlComplexType).booleanValue()) {
357
358 HashMap rhs_11 = new HashMap();
359 HashMap modmap_12 = new HashMap();
360 modmap_12 = ExpandComplexTypeDef(clnm, (IOmlComplexType) shape);
361 rhs_11 = new HashMap(r_um);
362 rhs_11.putAll(modmap_12);
363 r_um = (HashMap) UTIL.clone(rhs_11);
364 }
365 }
366 }
367 }
368 return r_um;
369 }
370
371
372
373
374 private HashMap ExpandComplexTypeDef (final String clnm, final IOmlComplexType shape) throws CGException {
375
376 String id = null;
377 id = shape.getIdentifier();
378 Vector f_ul = null;
379 f_ul = shape.getFieldList();
380 HashMap rexpr_6 = new HashMap();
381 Name tmpVar1_7 = null;
382 tmpVar1_7 = new Name(clnm, id);
383 HashMap tmpVar2_10 = new HashMap();
384 HashMap res_m_11 = new HashMap();
385 {
386
387 HashSet e_set_18 = new HashSet();
388 HashSet riseq_20 = new HashSet();
389 int max_21 = f_ul.size();
390 for (int i_22 = 1; i_22 <= max_21; i_22++)
391 riseq_20.add(new Long(i_22));
392 e_set_18 = riseq_20;
393 Long i = null;
394 {
395 for (Iterator enm_24 = e_set_18.iterator(); enm_24.hasNext(); ) {
396
397 Long elem_23 = UTIL.NumberToLong(enm_24.next());
398 i = elem_23;
399 String md_12 = null;
400 IOmlField obj_13 = null;
401 if ((1 <= i.intValue()) && (i.intValue() <= f_ul.size()))
402 obj_13 = (IOmlField) f_ul.get(i.intValue() - 1);
403 else
404 UTIL.RunTime("Run-Time Error:Illegal index");
405 md_12 = obj_13.getIdentifier();
406 res_m_11.put(md_12, i);
407 }
408 }
409 }
410 tmpVar2_10 = res_m_11;
411 rexpr_6 = new HashMap();
412 rexpr_6.put(tmpVar1_7, tmpVar2_10);
413 return rexpr_6;
414 }
415
416
417
418
419 public IOmlExpression LookUp (final String clnm, final String defnm) throws CGException {
420
421 Boolean cond_3 = null;
422 cond_3 = new Boolean(valm.containsKey(clnm));
423 if (cond_3.booleanValue()) {
424
425 HashMap vm = (HashMap) valm.get(clnm);
426 Boolean cond_14 = null;
427 cond_14 = new Boolean(vm.containsKey(defnm));
428 if (cond_14.booleanValue())
429 return (IOmlExpression) (IOmlExpression) vm.get(defnm);
430 else {
431
432 Boolean cond_21 = null;
433 cond_21 = new Boolean(inherit.containsKey(clnm));
434 if (cond_21.booleanValue()) {
435
436 HashSet supers = (HashSet) inherit.get(clnm);
437 {
438
439 {
440
441 String sup = null;
442 for (Iterator enm_46 = supers.iterator(); enm_46.hasNext(); ) {
443
444 String elem_29 = UTIL.ConvertToString(enm_46.next());
445 sup = elem_29;
446 {
447
448 Boolean cond_32 = null;
449 Boolean var1_33 = null;
450 var1_33 = new Boolean(valm.containsKey(sup));
451 {
452 if ((cond_32 = var1_33).booleanValue()) {
453
454 Boolean var2_36 = null;
455 var2_36 = new Boolean(((HashMap) valm.get(sup)).containsKey(defnm));
456 cond_32 = var2_36;
457 }
458 }
459 if (cond_32.booleanValue())
460 return (IOmlExpression) (IOmlExpression) ((HashMap) valm.get(sup)).get(defnm);
461 }
462 }
463 }
464 errorLog.ReportInternalError(null, UTIL.ConvertToString(RTERR.INTERNAL_uERROR), new Boolean(true));
465 }
466 }
467 else {
468 errorLog.ReportInternalError(null, UTIL.ConvertToString(RTERR.INTERNAL_uERROR), new Boolean(true));
469 }
470 }
471 }
472 else
473 errorLog.ReportInternalError(null, UTIL.ConvertToString(RTERR.INTERNAL_uERROR), new Boolean(true));
474 return (IOmlExpression) new OmlName(null, new String("Dummy"));
475 }
476
477
478
479
480 public SEM.VAL LookUpRecSel (final SEM.REC recval, final String selid, final IOmlFieldSelect expr) throws CGException {
481
482 Name tag = null;
483 tag = (recval).tag;
484 Boolean cond_7 = null;
485 cond_7 = new Boolean(recdefs.containsKey(tag));
486 if (cond_7.booleanValue()) {
487
488 HashMap sel_um = (HashMap) recdefs.get(tag);
489 Boolean cond_19 = null;
490 cond_19 = new Boolean(sel_um.containsKey(selid));
491 if (cond_19.booleanValue()) {
492
493 Long num = UTIL.NumberToLong(sel_um.get(selid));
494 SEM.VAL rexpr_31 = null;
495 Vector tmp_l_32 = null;
496 tmp_l_32 = (recval).v;
497 if ((1 <= num.intValue()) && (num.intValue() <= tmp_l_32.size()))
498 rexpr_31 = (SEM.VAL) tmp_l_32.get(num.intValue() - 1);
499 else
500 UTIL.RunTime("Run-Time Error:Illegal index");
501 return (SEM.VAL) rexpr_31;
502 }
503 else {
504
505 errorLog.ReportError(expr, UTIL.ConvertToString(RTERR.RECORD_uFIELD_uID_uUNKNOWN));
506 SEM.NUM rexpr_25 = null;
507 rexpr_25 = new SEM.NUM(UTIL.NumberToReal(new Long(1)));
508 return (SEM.VAL) rexpr_25;
509 }
510 }
511 else {
512
513 errorLog.ReportError(expr, UTIL.ConvertToString(RTERR.RECORD_uFIELD_uID_uUNKNOWN));
514 SEM.NUM rexpr_13 = null;
515 rexpr_13 = new SEM.NUM(UTIL.NumberToReal(new Long(1)));
516 return (SEM.VAL) rexpr_13;
517 }
518 }
519
520
521
522
523 public SEM.REC UpdateRecVal (final SEM.REC recval, final String selid, final SEM.VAL val, final IOmlExpression expr) throws CGException {
524
525 Name tag = null;
526 tag = (recval).tag;
527 Boolean cond_8 = null;
528 cond_8 = new Boolean(recdefs.containsKey(tag));
529 if (cond_8.booleanValue()) {
530
531 HashMap sel_um = (HashMap) recdefs.get(tag);
532 Boolean cond_23 = null;
533 cond_23 = new Boolean(sel_um.containsKey(selid));
534 if (cond_23.booleanValue()) {
535
536 Long num = UTIL.NumberToLong(sel_um.get(selid));
537 SEM.REC rexpr_38 = null;
538 SEM.REC tmpRE_40 = (SEM.REC) UTIL.clone(recval);
539 Vector val_42 = null;
540 Vector seqmap_45 = null;
541 seqmap_45 = (recval).v;
542 HashMap modmap_43 = new HashMap();
543 modmap_43 = new HashMap();
544 modmap_43.put(num, val);
545 val_42 = (Vector) UTIL.clone(seqmap_45);
546 for (Iterator enm_52 = modmap_43.keySet().iterator(); enm_52.hasNext(); ) {
547
548 Object dom_53 = enm_52.next();
549 Long edom_49 = UTIL.NumberToLong(dom_53);
550 SEM.VAL erng_50 = (SEM.VAL) modmap_43.get(dom_53);
551 if (edom_49.intValue() > val_42.size() || edom_49.intValue() < 1)
552 UTIL.RunTime("Run-Time Error:Illegal index in sequence modifier");
553 else
554 val_42.set(edom_49.intValue() - 1, erng_50);
555 }
556 ((SEM.REC) tmpRE_40).v = val_42;
557 rexpr_38 = tmpRE_40;
558 return rexpr_38;
559 }
560 else {
561
562 errorLog.ReportError(expr, UTIL.ConvertToString(RTERR.RECORD_uFIELD_uID_uUNKNOWN));
563 SEM.REC rexpr_29 = null;
564 Name tmpVar_30 = null;
565 tmpVar_30 = new Name(new String(""), new String(""));
566 rexpr_29 = new SEM.REC(tmpVar_30, new Vector());
567 return rexpr_29;
568 }
569 }
570 else {
571
572 errorLog.ReportError(expr, UTIL.ConvertToString(RTERR.RECORD_uFIELD_uID_uUNKNOWN));
573 SEM.REC rexpr_14 = null;
574 Name tmpVar_15 = null;
575 tmpVar_15 = new Name(new String(""), new String(""));
576 rexpr_14 = new SEM.REC(tmpVar_15, new Vector());
577 return rexpr_14;
578 }
579 }
580
581
582
583
584 static private HashMap MatchPatId2Expr (final IOmlPatternIdentifier patid, final IOmlExpression expr) throws CGException {
585
586 HashMap varRes_3 = new HashMap();
587 {
588
589 String id = null;
590 id = patid.getIdentifier();
591 varRes_3 = new HashMap();
592 varRes_3.put(id, expr);
593 }
594 return varRes_3;
595 }
596
597
598 }
599 ;