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: package de.uka.ilkd.key.unittest;
009:
010: import java.util.*;
011: import de.uka.ilkd.key.java.*;
012: import de.uka.ilkd.key.java.expression.literal.*;
013:
014: /**
015: * Contains a mapping of locations to concrete values for them.
016: */
017: public class Model {
018:
019: protected static final Boolean boolTrue = new Boolean(true);
020: protected static final Boolean boolFalse = new Boolean(false);
021:
022: private HashMap class2value;
023: private HashMap term2class;
024:
025: public Model(HashMap term2class) {
026: this (new HashMap(), term2class);
027: }
028:
029: private Model(HashMap class2value, HashMap term2class) {
030: this .class2value = class2value;
031: this .term2class = term2class;
032: }
033:
034: public Model copy() {
035: return new Model((HashMap) class2value.clone(), term2class);
036: }
037:
038: public void setValue(EquivalenceClass ec) {
039: if (ec.isInt()) {
040: class2value.put(ec, new IntValueContainer(ec
041: .getConcreteIntValue(term2class)));
042: } else if (ec.isBoolean()) {
043: class2value.put(ec, new BooleanValueContainer(ec
044: .getConcreteBooleanValue(term2class)));
045: }
046: }
047:
048: public void setValue(EquivalenceClass ec, int i) {
049: class2value.put(ec, new IntValueContainer(new Integer(i)));
050: }
051:
052: public void setValue(EquivalenceClass ec, boolean b) {
053: class2value.put(ec, b ? new BooleanValueContainer(boolTrue)
054: : new BooleanValueContainer(boolFalse));
055: }
056:
057: public void setValue(EquivalenceClass ec, ValueContainer vc) {
058: class2value.put(ec, vc);
059: }
060:
061: public int size() {
062: return class2value.size();
063: }
064:
065: /**
066: * Returns an array of possible values <code>ec</code> can have in this
067: * model.
068: */
069: // currently merging of models is disabled, so <code>ec</code> has always
070: // only one value
071: public Expression[] getValuesAsExpressions(EquivalenceClass ec) {
072: Object o = class2value.get(ec);
073: /* if(o instanceof Integer){
074: return new Expression[]{new IntLiteral(((Integer) o).intValue())};
075: }
076: if(o instanceof Boolean){
077: return new Expression[]{(o==boolTrue ?
078: BooleanLiteral.TRUE :
079: BooleanLiteral.FALSE)};
080: }*/
081: if (o == null) {
082: return new Expression[] { new IntLiteral(15) };
083: }
084: if (o instanceof ValueContainer) {
085: return ((ValueContainer) o).getValuesAsExpressions();
086: }
087: return null;
088: }
089:
090: /**
091: * Returns the value <code>ec</code> has in this model.
092: */
093: public Expression getValueAsExpression(EquivalenceClass ec) {
094: Expression[] earr = getValuesAsExpressions(ec);
095: if (earr != null) {
096: return earr[0];
097: }
098: return null;
099: }
100:
101: public ValueContainer getValue(EquivalenceClass ec) {
102: return (ValueContainer) class2value.get(ec);
103: }
104:
105: /** If m differs from this model only by one value the models are merged,
106: * i.e. the one differing entry is replaced by an interval created from
107: * the two different values of the corresponding equivalence class.
108: * Iff the merge is successful or this Model already subsumes m
109: * true is returned.
110: */
111: public boolean merge(Model m) {
112: EquivalenceClass diff = null;
113: Iterator it = class2value.keySet().iterator();
114: ValueContainer newValue = null;
115: boolean super Set = true;
116: int neCount = 0;
117: while (it.hasNext()) {
118: EquivalenceClass ec = (EquivalenceClass) it.next();
119: ValueContainer v0 = getValue(ec);
120: ValueContainer v1 = m.getValue(ec);
121: if (!v0.equals(v1)) {
122: neCount++;
123: if (diff == null) {
124: if (neCount > 1) {
125: return false;
126: }
127: if (!v0.contains(v1)) {
128: diff = ec;
129: newValue = v0.union(v1);
130: }
131: } else if (neCount > 1) {
132: return false;
133: }
134: }
135: if (!v0.contains(v1)) {
136: super Set = false;
137: }
138: }
139: if (diff != null && newValue != null) {
140: class2value.put(diff, newValue);
141: return true;
142: } else {
143: return super Set;
144: }
145: }
146:
147: public int hashCode() {
148: return 17;
149: }
150:
151: public String toString() {
152: String result = "Model :\n{\n";
153: Iterator it = class2value.keySet().iterator();
154: while (it.hasNext()) {
155: Object o = it.next();
156: result += o + " = " + class2value.get(o) + "\n";
157: }
158: result += "}";
159: return result;
160: }
161:
162: public boolean equals(Object o) {
163: if (o == null || !(o instanceof Model)) {
164: return false;
165: }
166: return class2value.equals(((Model) o).class2value);
167: }
168: }
|