001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 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 Daniel Larsson */package de.uka.ilkd.key.casetool.together;
014:
015: import java.io.IOException;
016: import java.util.Iterator;
017: import java.util.LinkedList;
018:
019: import com.togethersoft.openapi.ide.IdeAccess;
020:
021: import de.uka.ilkd.key.casetool.FunctionalityOnModel;
022: import de.uka.ilkd.key.casetool.HashMapOfClassifier;
023: import de.uka.ilkd.key.casetool.UMLOCLClassifier;
024: import de.uka.ilkd.key.gui.Main;
025: import de.uka.ilkd.key.logic.Name;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.TermFactory;
028: import de.uka.ilkd.key.logic.op.Function;
029: import de.uka.ilkd.key.logic.op.Operator;
030: import de.uka.ilkd.key.logic.op.TermSymbol;
031: import de.uka.ilkd.key.logic.op.oclop.OclOp;
032: import de.uka.ilkd.key.ocl.gf.ModelExporter;
033: import de.uka.ilkd.key.pp.LogicPrinter;
034: import de.uka.ilkd.key.pp.NotationInfo;
035: import de.uka.ilkd.key.pp.PresentationFeatures;
036: import de.uka.ilkd.key.pp.ProgramPrinter;
037: import de.uka.ilkd.key.proof.Node;
038: import de.uka.ilkd.key.proof.Proof;
039: import de.uka.ilkd.key.util.pp.StringBackend;
040:
041: /**
042: * Used for OCL Simplification.
043: * Wraps the machinery needed to, given a list of class names:
044: * <ol>
045: * <li> Extract the model representation of these classes and
046: * invoke the prover machinery on these representations.
047: * </li>
048: * <li> Extract the resulting terms (simplified invariants),
049: * pretty-print them into strings, and update the source
050: * code of the proper classes with these invariants.
051: * </li>
052: * </ol>
053: */
054: public class TogetherOCLSimplInterface {
055:
056: private Main main;
057: private UMLOCLTogetherModel umlModel;
058:
059: public TogetherOCLSimplInterface() {
060: }
061:
062: /**
063: * Performs the entire simplification.
064: * @param newClasses List of class names (Strings), whose
065: * invariants need to be simplified.
066: */
067: public void simplifyConstraints(LinkedList newClasses) {
068: IdeAccess.getIdeManager().saveAll();
069: IdeAccess.getIdeManager().synchronize();
070:
071: //Create the file "../modelinfo.umltypes" needed for the "ocl2taclet" tool
072: umlModel = new UMLOCLTogetherModel(null);
073: createModelInfoFile();
074:
075: //For each of the newly created/changed classes (the elements of "newClasses"),
076: //check if it has an invariant and if so, simplify it.
077: while (newClasses.size() > 0) {
078: String className = (String) newClasses.getFirst();
079: TogetherModelClass togetherClass = umlModel
080: .getTogetherReprModelClass(className);
081:
082: //If "togetherClass" has an invariant, continue with simplification
083: if (togetherClass != null
084: && togetherClass.getMyInv().trim().length() > 0) {
085: simplifyInvariant(togetherClass, newClasses);
086: } else {
087: newClasses.remove(className);
088: }
089: }
090: }
091:
092: /**
093: * Creates a file with information about the UML model
094: * and places it in the directory of the current
095: * Together project. Needed for the invocation of
096: * "ocl2taclet".
097: */
098: private void createModelInfoFile() {
099: HashMapOfClassifier hashMapOfCs = umlModel
100: .getUMLOCLClassifiers();
101:
102: //Temporary "hack" to cope with bug in the parsing of the file
103: // "../modelinfo.umltypes".
104: LinkedList list = new LinkedList();
105: Iterator iterator = hashMapOfCs.values().iterator();
106: while (iterator.hasNext()) {
107: UMLOCLClassifier classifier = (UMLOCLClassifier) iterator
108: .next();
109: String cName = classifier.getFullName();
110: if (cName.startsWith("java.util")) {
111: list.add(classifier.getName());
112: }
113: }
114: Iterator newIter = list.iterator();
115: while (newIter.hasNext()) {
116: hashMapOfCs.remove((String) newIter.next());
117: }
118: // ... end "hack"
119:
120: ModelExporter me = new ModelExporter(hashMapOfCs);
121: me.export(UMLOCLTogetherModel.getTogetherProjectDir()
122: + "/modelinfo.umltypes");
123: }
124:
125: /**
126: * Invokes the prover.
127: * @param togetherClass The representation of the class whose
128: * invariant is going to be simplified.
129: * @param newClasses Names of classes whose invariants
130: * still need to be simplified.
131: */
132: private void simplifyInvariant(TogetherModelClass togetherClass,
133: LinkedList newClasses) {
134: String res = FunctionalityOnModel
135: .simplifyInvariant(togetherClass);
136: main = Main.getInstance();
137:
138: //Do not continue until the prover exits (different threads).
139: while (main.isVisible()) {
140: synchronized (main.monitor) {
141: try {
142: main.monitor.wait();
143: } catch (InterruptedException e) {
144: e.printStackTrace();
145: }
146: }
147: }
148:
149: //Extract the simplified constraint
150: Proof proof = main.mediator().getProof();
151: Node node = proof.openGoals().iterator().next().node();
152: Term term = node.sequent().succedent().getFirst().formula()
153: .sub(0);
154: writeInvariantsToClasses(term, newClasses);
155: }
156:
157: /**
158: * Uses recursion to write the list of simplified
159: * invariants back to the source code of the proper classes.
160: */
161: private void writeInvariantsToClasses(Term listOfInvariants,
162: LinkedList newClasses) {
163: if (listOfInvariants.op() != OclOp.CONS_INV) {
164: return;
165: }
166: Term invariant = listOfInvariants.sub(0);
167:
168: //Find the together class corresponding to the OCL Classifier
169: //which is the context for the invariant.
170: String className = invariant.sub(0).op().name().toString();
171: String fixedClassName = className.replace('~', '.');
172: TogetherModelClass togetherClass = umlModel
173: .getTogetherReprModelClass(fixedClassName);
174:
175: //Get the actual invariant as a String
176: String inv = extractInvariantFromTerm(invariant.sub(1));
177:
178: //Update the UML model with the simplified invariant
179: if (togetherClass != null) {
180: togetherClass.setMyInv(inv);
181: newClasses.remove(fixedClassName);
182: }
183:
184: //Continue in the list of invariants.
185: writeInvariantsToClasses(listOfInvariants.sub(1), newClasses);
186: }
187:
188: /**
189: * @param term The simplified invariant in form of a Term.
190: * @return The same invariant as a String.
191: */
192: private String extractInvariantFromTerm(Term term) {
193: TermSymbol oclWrapper = (Function) main.mediator().func_ns()
194: .lookup(new Name("$OclWrapper"));
195: Term formula = TermFactory.DEFAULT.createFunctionTerm(
196: oclWrapper, term);
197: StringBackend backend = new StringBackend(55);
198: NotationInfo notInfo = NotationInfo.createInstance();
199:
200: //For pretty-printing of numbers. Have to refresh the NotationInfo (for some reason).
201: notInfo.createNumLitNotation((Operator) main.mediator()
202: .func_ns().lookup(new Name("#")));
203: notInfo.createNumLitNotation((Operator) main.mediator()
204: .func_ns().lookup(new Name("Z")));
205: notInfo.createNumLitNotation((Operator) main.mediator()
206: .func_ns().lookup(new Name("0")));
207: notInfo.createNumLitNotation((Operator) main.mediator()
208: .func_ns().lookup(new Name("1")));
209: notInfo.createNumLitNotation((Operator) main.mediator()
210: .func_ns().lookup(new Name("2")));
211: notInfo.createNumLitNotation((Operator) main.mediator()
212: .func_ns().lookup(new Name("3")));
213: notInfo.createNumLitNotation((Operator) main.mediator()
214: .func_ns().lookup(new Name("4")));
215: notInfo.createNumLitNotation((Operator) main.mediator()
216: .func_ns().lookup(new Name("5")));
217: notInfo.createNumLitNotation((Operator) main.mediator()
218: .func_ns().lookup(new Name("6")));
219: notInfo.createNumLitNotation((Operator) main.mediator()
220: .func_ns().lookup(new Name("7")));
221: notInfo.createNumLitNotation((Operator) main.mediator()
222: .func_ns().lookup(new Name("8")));
223: notInfo.createNumLitNotation((Operator) main.mediator()
224: .func_ns().lookup(new Name("9")));
225:
226: PresentationFeatures.ENABLED = true;
227: PresentationFeatures.modifyNotationInfo(notInfo, main
228: .mediator().func_ns());
229:
230: LogicPrinter lp = new LogicPrinter(new ProgramPrinter(),
231: notInfo, backend, main.mediator().getServices());
232: try {
233: lp.printTerm(formula);
234: backend.flush();
235: } catch (IOException ioe) {
236: ioe.printStackTrace();
237: }
238: return backend.getString();
239: }
240: }
|