01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.unittest.cogent;
12:
13: import java.util.*;
14: import java.io.*;
15:
16: import de.uka.ilkd.key.java.*;
17: import de.uka.ilkd.key.logic.*;
18: import de.uka.ilkd.key.unittest.*;
19:
20: public class CogentModelGenerator implements DecProdModelGenerator {
21:
22: private SetOfTerm locations;
23: private HashMap term2class;
24: private CogentTranslation ct;
25:
26: public CogentModelGenerator(CogentTranslation ct, Services serv,
27: HashMap term2class, SetOfTerm locations) {
28: this .ct = ct;
29: this .term2class = term2class;
30: this .locations = locations;
31: }
32:
33: public Set createModels() {
34: HashSet models = new HashSet();
35: Model model = new Model(term2class);
36: try {
37: CogentResult response = DecisionProcedureCogent.execute(ct
38: .translate());
39: if (response.valid()) {
40: return models;
41: }
42: IteratorOfTerm it = locations.iterator();
43: while (it.hasNext()) {
44: Term t = it.next();
45: EquivalenceClass ec = (EquivalenceClass) term2class
46: .get(t);
47: if (ec.isInt()) {
48: model.setValue(ec, response.getValueForTerm(t, ct));
49: }
50: }
51: models.add(model);
52: } catch (IOException e) {
53: throw new CogentException(e);
54: }
55: return models;
56: }
57: }
|