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: package de.uka.ilkd.key.visualization;
09:
10: import java.util.Arrays;
11: import java.util.Comparator;
12: import java.util.LinkedList;
13:
14: import de.uka.ilkd.key.proof.Node;
15:
16: public class VisualizationModel {
17: ExecutionTraceModel[] traces;
18: Node node = null;
19: static Comparator comp = new TraceComparator();
20:
21: public VisualizationModel(Node node, ExecutionTraceModel[] traces) {
22: this .traces = traces;
23: this .node = node;
24: if (traces != null)
25: Arrays.sort(this .traces, comp);
26: }
27:
28: public Node getNode() {
29: return node;
30: }
31:
32: public ExecutionTraceModel[] getExecutionTraces() {
33: return traces;
34: }
35:
36: /**
37: * @return the Execution Trace Models that contain ContextTraceElements and
38: * that are of type 1
39: */
40: public ExecutionTraceModel[] getInterestingExecutionTraces() {
41: LinkedList result = new LinkedList();
42: for (int i = 0; i < traces.length; i++) {
43: if ((traces[i].getFirstContextTraceElement() != TraceElement.END)
44: && traces[i].getType() == ExecutionTraceModel.TYPE1) {
45: result.add(traces[i]);
46: }
47: }
48: ExecutionTraceModel[] exTraceModels = new ExecutionTraceModel[result
49: .size()];
50: result.toArray(exTraceModels);
51: return exTraceModels;
52: }
53:
54: /**
55: * @return true if t1 is more useful to understand the proof then t2
56: */
57:
58: public boolean compare(ExecutionTraceModel t1,
59: ExecutionTraceModel t2) {
60: if (t1.getRating() > t2.getRating())
61: return true;
62: else if (t1.getRating() == t2.getRating())
63: return t1.getFirstTraceElement().serialNr() > t2
64: .getFirstTraceElement().serialNr();
65: return false;
66: }
67:
68: public static class TraceComparator implements Comparator {
69: public int compare(Object o1, Object o2) {
70: ExecutionTraceModel t1 = (ExecutionTraceModel) o1;
71: ExecutionTraceModel t2 = (ExecutionTraceModel) o2;
72: if (t1.getRating() == t2.getRating())
73: return 0;
74: else if (t1.getRating() < t2.getRating())
75: return 1;
76: return -1;
77:
78: }
79:
80: public boolean equals(Object o1, Object o2) {
81: ExecutionTraceModel t1 = (ExecutionTraceModel) o1;
82: ExecutionTraceModel t2 = (ExecutionTraceModel) o2;
83: return (t1.getRating() == t2.getRating());
84: }
85:
86: }
87:
88: }
|