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: package de.uka.ilkd.key.counterexample;
011:
012: import java.util.StringTokenizer;
013: import java.util.Vector;
014:
015: /**
016: * This class is a representation of the Model generated by mgtp
017: * displaying the values that the variables are assigned, the
018: * interpretation of subterms, the statistics of the latest mgtp
019: * run etc. All this in a hopefully
020: * readable text format which one can extract with the toString() Method
021: * @author Sonja Pieper
022: * @since 13/08/01
023: * @version 0.1
024: */
025: public class ModelRepresentation {
026:
027: private Vector vars;
028: private Vector subterms;
029: private Vector termeval;
030: private String model;
031:
032: public ModelRepresentation(String mgtpprove) {
033:
034: vars = new Vector();
035: subterms = new Vector();
036: termeval = new Vector();
037:
038: model = this .extractModel(mgtpprove);
039: this .processModel(this .model);
040:
041: }
042:
043: public String getVars() {
044: String s = new String();
045: for (int i = 0; i < vars.size(); i++) {
046: s = s + vars.elementAt(i) + "\n";
047: }
048: return s;
049: }
050:
051: public String getTermeval() {
052: String s = new String();
053: for (int i = 0; i < termeval.size(); i++) {
054: s = s + termeval.elementAt(i) + "\n";
055: }
056: return s;
057: }
058:
059: public String getSubterms() {
060: String s = new String();
061: for (int i = 0; i < subterms.size(); i++) {
062: s = s + subterms.elementAt(i) + "\n";
063: }
064: return s;
065: }
066:
067: private String extractModel(String prove) {
068: String m = new String();
069: //@@@ extract model from prove is not yet implemented
070: return m;
071: }
072:
073: private void processModel(String m) {
074:
075: String intpr = new String();
076: String zeile = new String();
077:
078: StringTokenizer zeilenteiler = new StringTokenizer(m, "\n");
079:
080: int i = 0;
081:
082: while (zeilenteiler.hasMoreElements()) {
083: i++;
084: zeile = zeilenteiler.nextToken();
085:
086: //interpretation: intpr kommt vor, val kommt nicht vor
087: if (zeile.startsWith("intpr")
088: && zeile.lastIndexOf("val") < 0) {
089: intpr = intpr + zeile + "\n";
090: }
091:
092: //Term evaluation: is kommt vor, arg kommt nicht vor
093: else if (zeile.startsWith("is")
094: && zeile.lastIndexOf("arg") < 0) {
095:
096: //Variable extraction "is(val(sk_....),...)":
097: if (zeile.startsWith("is(val(sk_")) {
098: int par = zeile.indexOf("),");
099: String sko = zeile.substring(7, par);
100: String val = zeile.substring(par + 2, zeile
101: .length() - 1);
102: if (val.lastIndexOf("val") < 0) {
103: vars.add(sko + " : " + val + "\n");
104: }
105: }
106: //Subterm extraction:
107: else {
108: zeile = zeile.substring(3, zeile.length() - 1);
109:
110: //schliessende klammer von val finden:
111: int open = 1;
112: int pos = 4;
113: while (open > 0) {
114: switch (zeile.charAt(pos)) {
115: case '(':
116: open++;
117: break;
118: case ')':
119: open--;
120: break;
121: }
122: pos++;
123: }
124:
125: //subterms = subterms + zeile + "\n";
126: String sub = zeile.substring(4, pos - 1);
127: String val = zeile.substring(pos + 1, zeile
128: .length());
129: if (val.lastIndexOf("val") < 0) {
130: if (sub.lastIndexOf("sk_") >= 0) {
131: subterms.add(sub + " : " + val + "\n");
132: } else {
133: termeval.add(termeval + sub + " : " + val
134: + "\n");
135: }
136: }
137: }
138:
139: }
140: }
141:
142: /* @@@ die ersetzung ist auskommentiert sk_var
143: for(int j=0;j<variables.size();j++){
144: String name = (variables.elementAt(j)).toString();
145: name = name.substring(5,name.lastIndexOf("->")-1);
146: ausgabe = mc.substitute(ausgabe,name);
147: }
148: */
149:
150: }
151:
152: }
|