001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: //
011: //
012:
013: /** @author Kristofer Johannisson */package de.uka.ilkd.key.ocl.gf;
014:
015: import java.io.BufferedOutputStream;
016: import java.io.FileNotFoundException;
017: import java.io.FileOutputStream;
018: import java.io.PrintStream;
019: import java.util.*;
020: import java.util.logging.Logger;
021:
022: import tudresden.ocl.check.OclTypeException;
023: import tudresden.ocl.check.types.Type;
024:
025: import com.togethersoft.openapi.rwi.*;
026:
027: import de.uka.ilkd.key.casetool.*;
028:
029: /** export UML/OCL type information to a file, for use in
030: * typechecking and with GF
031: */
032: public class ModelExporter {
033:
034: private static final String TOGETHER_UNIQUE_NAME_PREFIX = "<oiref:java#Class#";
035: private static final String TOGETHER_UNIQUE_NAME_POSTFIX = ":oiref>";
036:
037: /** key: package name "java::lang", val: string of class signatures */
038: private HashMap packClass;
039: /** key: package name "java::lang", val: string of association signatures */
040: private HashMap packAssoc;
041:
042: private HashMapOfClassifier model;
043:
044: /** Contains UMLOCLAssociation. Keeps track of which assocs have been added
045: * (necessary since otherwise
046: * we get the same assoc twice, in both directions) */
047: private Vector previousAssocs;
048:
049: private Logger logger;
050:
051: public ModelExporter(HashMapOfClassifier model) {
052: logger = Logger.getLogger("key.ocl.gf");
053: packClass = new HashMap();
054: packAssoc = new HashMap();
055: previousAssocs = new Vector();
056: this .model = model;
057: }
058:
059: /* @param s java-qualified class name e.g. java.lang.Object"
060: * @return ocl type name e.g. "java::lang::Object", qualify with
061: * "NOPACKAGE" as appropriate.
062: */
063: private String javaType2oclType(String s) {
064: if (s.indexOf(".") > 0) { // qualified name
065: return s.replaceAll("\\.", "::");
066: } else { // unqualified
067: if (s.equals("Integer") || s.equals("Real")
068: || s.equals("Boolean") || s.equals("String")) {
069: return s;
070: } else {
071: return "NOPACKAGE::" + s;
072: }
073: }
074: }
075:
076: /* @param name possibly package-qualified name, with dots
077: * e.g. "java.lang.Object"
078: * @return package in OCL notation, where dots are replaced with double
079: * colons (last part discarded), e.g. "java::lang"
080: */
081: private String name2package(String name) {
082: int lastDot = name.lastIndexOf(".");
083:
084: if (lastDot >= 0) {
085: String javaPack = name.substring(0, lastDot);
086: String result = javaPack.replaceAll("\\.", "::");
087: return result.equals("") ? "NOPACKAGE" : result;
088: } else { // no dot found
089: return "NOPACKAGE";
090: }
091: }
092:
093: private String qualifiedName(UMLOCLClassifier c) {
094: return javaType2oclType(c.getFullName());
095: }
096:
097: /** Convert a Type into a String representing an OCL type. This could
098: * entail qualifing and handling of array types
099: */
100: private String dresdenType2str(Type t) {
101: if (t instanceof UMLOCLClassifier) {
102: if (t.toString().endsWith("[]")) { // take care of broken array types
103: String shortname = t.toString().substring(0,
104: t.toString().length() - 2);
105: String ocltype;
106: try { // is the array element type a Java basic type?
107: ocltype = JavaOCLTypeMap.getBasicTypeFor(shortname)
108: .toString();
109: } catch (OclTypeException ote) {
110: // if not, it could still be one of the following:
111: if (shortname.equals("String")
112: || shortname.equals("Integer")
113: || shortname.equals("Real")
114: || shortname.equals("Boolean")) {
115: ocltype = shortname;
116: } else { // not a special class, qualify as usual:
117: ocltype = ((UMLOCLClassifier) t).getFullName();
118: ocltype = javaType2oclType(ocltype.substring(0,
119: ocltype.length() - 2));
120: }
121: }
122:
123: return "Sequence (" + ocltype + ")";
124: } else { // not an array type
125: return qualifiedName((UMLOCLClassifier) t);
126: }
127: } else { // this is probably a dresden Basic type
128: return t.toString();
129: }
130: }
131:
132: private String structFeature2str(UMLOCLStructuralFeature attr) {
133: if (classNotHandled(attr.getType().toString())) {
134: return "";
135: } else {
136: return attr.getName() + " : "
137: + dresdenType2str(attr.getType()) + ";\n";
138: }
139: }
140:
141: private boolean inhFromObject(UMLOCLFeature oper) {
142: String n = oper.getName();
143: Type r = oper.getType();
144: String rS;
145: if (r != null) {
146: rS = r.toString();
147: } else {
148: rS = "";
149: }
150:
151: return (n.equals("wait()") && r == null)
152: || (n.equals("wait(long)") && r == null)
153: || (n.equals("wait(long,int)") && r == null)
154: || (n.equals("getClass()") && r == null)
155: || (n.equals("toString()") && rS.equals("String"))
156: || (n.equals("equals(java.lang.Object)") && rS
157: .equals("Boolean"))
158: || (n.equals("hashCode()") && rS.equals("Integer"))
159: || (n.equals("notifyAll()") && r == null)
160: || (n.equals("finalize()") && r == null)
161: || (n.equals("clone()") && rS.equals("Object"))
162: || (n.equals("notify()") && r == null);
163: }
164:
165: /** operation names contain parameters, this method cleans up the name,
166: * i.e. it drops everything after (and including) the first '(' */
167: private String dropArguments(String operName) {
168: int x = operName.indexOf("(");
169: if (x != -1) {
170: return operName.substring(0, x);
171: } else {
172: return operName;
173: }
174:
175: }
176:
177: private String behavFeature2str(UMLOCLBehaviouralFeature oper) {
178: String result;
179: String name = dropArguments(oper.getName());
180:
181: Type[] args = oper.getParameters();
182: Type returns = oper.getType();
183:
184: // note that isQuery currently always returns true
185: if (oper.isQuery() && returns != null) {
186: result = "{query} ";
187: } else {
188: result = "";
189: }
190:
191: result += name + "(";
192: for (int i = 0; i < args.length; i++) {
193: if (i != 0) {
194: result += ", ";
195: }
196: if (classNotHandled(args[i].toString())) {
197: return "";
198: }
199: result += dresdenType2str(args[i]);
200: }
201: result += ")";
202:
203: if (returns != null) {
204: if (classNotHandled(returns.toString())) {
205: return "";
206: }
207: result += " : " + dresdenType2str(returns);
208: }
209:
210: result += ";\n";
211: return result;
212: }
213:
214: private String mult2str(Multiplicity mult) {
215: int min = mult.getMin();
216: int max = mult.getMax();
217:
218: if (min == 1 && max == 1) {
219: return "[1]";
220: } else {
221: String minS = "0"; // default in case of no match below
222: String maxS = "*"; // default in case of no match below
223:
224: if (min == 0) {
225: minS = "0";
226: } else if (min == 1) {
227: minS = "1";
228: }
229: if (max == 1) {
230: maxS = "1";
231: } else if (max == Multiplicity.INFINITE) {
232: maxS = "*";
233: }
234:
235: return "[" + minS + ".." + maxS + "]";
236: }
237: }
238:
239: // this really belongs in UMLOCLAssociations, but that is an interface
240: private boolean assocEqualsNoDirection(UMLOCLAssociation a1,
241: UMLOCLAssociation a2) {
242: return ((a1.getSource() == a2.getSource()
243: && a1.getSourceMultiplicity() == a2
244: .getSourceMultiplicity()
245: && a1.getSourceRole() == a2.getSourceRole()
246: && a1.getTarget() == a2.getTarget()
247: && a1.getTargetMultiplicity() == a2
248: .getTargetMultiplicity() && a1.getTargetRole() == a2
249: .getTargetRole()) || (a1.getSource() == a2.getTarget()
250: && a1.getSourceMultiplicity() == a2
251: .getTargetMultiplicity()
252: && a1.getSourceRole() == a2.getTargetRole()
253: && a1.getTarget() == a2.getSource()
254: && a1.getTargetMultiplicity() == a2
255: .getSourceMultiplicity() && a1.getTargetRole() == a2
256: .getSourceRole()));
257: }
258:
259: private boolean assocAlreadyDefined(UMLOCLAssociation assoc) {
260: Iterator i = previousAssocs.iterator();
261: UMLOCLAssociation a;
262:
263: while (i.hasNext()) {
264: a = (UMLOCLAssociation) i.next();
265: if (assocEqualsNoDirection(a, assoc)) {
266: return true;
267: }
268: }
269:
270: return false;
271: }
272:
273: private String getAssocQualifier(String sourceRole,
274: String targetClass, String role, String qualifier) {
275: //Added by Daniel
276: //Checks if this association is ordered or not
277: //as given by the "supplierQualifier"-property
278: RwiModel rwiModel = RwiModelAccess.getModel();
279: String result = "";
280: //"targetClass" needs to be UMLOCLClassifier::getFullName() !
281: String uniqueName = TOGETHER_UNIQUE_NAME_PREFIX + targetClass
282: + TOGETHER_UNIQUE_NAME_POSTFIX;
283: RwiElement elem = rwiModel.findElement(uniqueName);
284: if (elem != null) {
285: RwiNode node = (RwiNode) elem;
286: Enumeration memEnum = node.members();
287: while (memEnum.hasMoreElements()) {
288: RwiMember member = (RwiMember) memEnum.nextElement();
289: String supplierRoleProp = member.getProperty(role);
290: if (supplierRoleProp != null
291: && supplierRoleProp.equals(sourceRole)) {
292: result = member.getProperty(qualifier);
293: break;
294: }
295: }
296: }
297:
298: return result == null ? "" : result;
299: }
300:
301: private String assoc2str(UMLOCLAssociation assoc) {
302:
303: String sourceClass = assoc.getSource().getFullName();
304: String targetClass = assoc.getTarget().getFullName();
305: String sourceMult = mult2str(assoc.getSourceMultiplicity());
306: String targetMult = mult2str(assoc.getTargetMultiplicity());
307: String sourceRole = assoc.getSourceRole();
308: String targetRole = assoc.getTargetRole();
309:
310: String source, target;
311:
312: if (sourceRole != null) {
313: source = sourceRole + " : " + javaType2oclType(sourceClass)
314: + " " + sourceMult;
315: } else {
316: source = javaType2oclType(sourceClass) + " " + sourceMult;
317: }
318:
319: if (targetRole != null) {
320: target = targetRole + " : " + javaType2oclType(targetClass)
321: + " " + targetMult;
322: } else {
323: target = javaType2oclType(targetClass) + " " + targetMult;
324: }
325:
326: // find out if the association-ends are {ordered} or not
327: // N.B.: this requires role-names, will not work if they are missing
328: // source/target might be client/supplier or supplier/client
329: // in Toghether-speak. Try both ways.
330: String qLeft = getAssocQualifier(sourceRole, targetClass,
331: "supplierRole", "supplierQualifier");
332: String qRight = getAssocQualifier(sourceRole, targetClass,
333: "supplierRole", "clientQualifier");
334:
335: if (qLeft.equals("") && qRight.equals("")) {
336: qLeft = getAssocQualifier(targetRole, sourceClass,
337: "supplierRole", "clientQualifier");
338: qRight = getAssocQualifier(targetRole, sourceClass,
339: "supplierRole", "supplierQualifier");
340: }
341:
342: if (qLeft.equals("ordered") || qLeft.equals("{ordered}")) {
343: source = "{ordered} " + source;
344: }
345:
346: if (qRight.equals("ordered") || qRight.equals("{ordered}")) {
347: target = "{ordered} " + target;
348: }
349:
350: return source + " <-> " + target + ";\n";
351:
352: }
353:
354: private String super types2str(HashMapOfClassifier super types) {
355: String result = "";
356:
357: boolean addSeparator = false;
358: Iterator i = super types.keySet().iterator();
359: while (i.hasNext()) {
360: if (addSeparator) {
361: result += ", ";
362: }
363: UMLOCLClassifier classif = ((UMLOCLClassifier) super types
364: .get(i.next()));
365: result += qualifiedName(classif);
366: addSeparator = true;
367: }
368:
369: return result;
370: }
371:
372: private boolean bracketed(String s) {
373: return s.startsWith("<")
374: && (s.endsWith(">") || s.indexOf(">(") != -1);
375: }
376:
377: // we cannot handle all Java classes
378: private boolean classNotHandled(String s) {
379: return s.equals("Enumeration") || s.equals("Class")
380: || s.equals("<Default>");
381: }
382:
383: // some Java classes clash with built-in OCL types
384: private boolean classAlreadyInOCL(String s) {
385: return s.equals("Boolean") || s.equals("Integer")
386: || s.equals("String");
387: }
388:
389: private void addClassifier(UMLOCLClassifier classif) {
390: // array types are for some reason included by Together/KeY
391: // do not include these
392: if (classif.getName().endsWith("[]")) {
393: return;
394: }
395:
396: if (classNotHandled(classif.getName())
397: || classAlreadyInOCL(classif.getName())) {
398: return;
399: }
400:
401: HashMapOfClassifier super types = classif.getSupertypes();
402: HashMapOfFeatures features = classif.features();
403: HashMapOfAssociations assocs = classif.getAssociations();
404:
405: String pack = name2package(classif.getFullName());
406:
407: String super s = super types2str(super types);
408:
409: HashSet attrs = new HashSet();
410: HashSet opers = new HashSet();
411:
412: Iterator i = features.keySet().iterator();
413: while (i.hasNext()) {
414: UMLOCLFeature f = (UMLOCLFeature) features.get(i.next());
415: if (!bracketed(f.getName())) {
416: if (f instanceof UMLOCLStructuralFeature) {
417: attrs
418: .add(structFeature2str((UMLOCLStructuralFeature) f));
419: } else if (f instanceof UMLOCLBehaviouralFeature
420: && (!inhFromObject(f))) {
421: opers
422: .add(behavFeature2str((UMLOCLBehaviouralFeature) f));
423: }
424: }
425: }
426:
427: String assocsDef = "";
428: i = assocs.keySet().iterator();
429: while (i.hasNext()) {
430: UMLOCLAssociation assoc = (UMLOCLAssociation) assocs.get(i
431: .next());
432: if (!assocAlreadyDefined(assoc)) {
433: previousAssocs.add(assoc);
434: assocsDef += assoc2str(assoc);
435: }
436: }
437: if (!assocsDef.equals("")) {
438: String assocsDefs = (String) packAssoc.get(pack);
439: if (assocsDefs != null) {
440: packAssoc.put(pack, assocsDefs + assocsDef);
441: } else {
442: packAssoc.put(pack, assocsDef);
443: }
444: }
445:
446: String attrsDef = "";
447: i = attrs.iterator();
448: while (i.hasNext()) {
449: attrsDef += (String) i.next();
450: }
451: String opersDef = "";
452: i = opers.iterator();
453: while (i.hasNext()) {
454: opersDef += (String) i.next();
455: }
456:
457: String classDef = "<class> "
458: + classif.getName()
459: + "\n"
460: + (super s.equals("") ? "" : "<super> " + super s
461: + " </super>\n")
462: + (attrsDef.equals("") ? "" : "<attributes> "
463: + attrsDef + " </attributes>\n")
464: + (opersDef.equals("") ? "" : "<opers> " + opersDef
465: + " </opers>\n") + "</class>\n";
466:
467: String classDefs = (String) packClass.get(pack);
468: if (classDefs != null) {
469: classDefs = classDefs + "\n" + classDef;
470: } else {
471: classDefs = classDef;
472: }
473: packClass.put(pack, classDefs);
474: }
475:
476: /** export model information to a file
477: * @param path path for what file to write to
478: */
479: public void export(String path) {
480: try {
481: PrintStream stream = new PrintStream(
482: new BufferedOutputStream(new FileOutputStream(path)));
483: export(stream);
484: stream.flush();
485: stream.close();
486: } catch (FileNotFoundException e) {
487: logger.severe("Can not open file " + path
488: + " for writing model information.");
489: }
490:
491: }
492:
493: /** export model information
494: * @param ps export on this PrintStream
495: */
496: public void export(PrintStream ps) {
497: Iterator i = model.keySet().iterator();
498: while (i.hasNext()) {
499: addClassifier((UMLOCLClassifier) model.get(i.next()));
500: }
501:
502: i = packClass.keySet().iterator();
503: String pkg;
504:
505: while (i.hasNext()) {
506: pkg = (String) i.next();
507: ps.println("<package> " + pkg);
508:
509: ps.println((String) packClass.get(pkg));
510: ps.println();
511:
512: String pAssocs = (String) packAssoc.get(pkg);
513: if (pAssocs != null) {
514: ps.println("<associations>");
515: //ps.println(orderAssocs(pAssocs));
516: ps.println(pAssocs);
517: ps.println("</associations>");
518: }
519:
520: ps.println("</package>");
521: ps.println();
522: }
523: }
524:
525: /*
526: //To get all ordered associations to appear first
527: public String orderAssocs(String str) {
528: StringBuffer buffer = new StringBuffer(str);
529: LinkedList list = new LinkedList();
530: int index = buffer.indexOf("\n");
531: while (index != -1) {
532: String s = buffer.substring(0, index+1);
533: list.add(s);
534: buffer = buffer.delete(0, index+1);
535: index = buffer.indexOf("\n");
536: }
537:
538: StringBuffer result = new StringBuffer();
539: Iterator iter = list.iterator();
540: while (iter.hasNext()) {
541: String s = (String)iter.next();
542: if (s.startsWith("{ordered}")) {
543: result.insert(0, s);
544: } else {
545: result.append(s);
546: }
547: }
548: return result.toString();
549: }
550: */
551: }
|