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.visualization;
009:
010: import de.uka.ilkd.key.java.ProgramElement;
011: import de.uka.ilkd.key.java.SourceElement;
012: import de.uka.ilkd.key.java.reference.IExecutionContext;
013: import de.uka.ilkd.key.logic.PosInOccurrence;
014: import de.uka.ilkd.key.proof.Node;
015: import de.uka.ilkd.key.rule.PosTacletApp;
016: import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
017:
018: public class TraceElement {
019:
020: protected TraceElement nextInProof;
021: protected ContextTraceElement stepInto;
022: protected SourceElement programElement;
023: protected IExecutionContext executionContext;
024: protected Node node;
025: protected ProgramElement program;
026: protected PosInOccurrence posOfModality;
027:
028: static public final ContextTraceElement END = new ContextTraceElement();
029: static public final ParentContextTraceElement PARENTROOT = new ParentContextTraceElement();
030:
031: public TraceElement(SourceElement prElement, Node node,
032: TraceElement nip, ContextTraceElement ne) {
033: this (prElement, node, nip, ne, null);
034: }
035:
036: public TraceElement(SourceElement prElement, Node n,
037: TraceElement nip, ContextTraceElement ne,
038: IExecutionContext exCont) {
039: node = n;
040: posOfModality = n.getAppliedRuleApp().posInOccurrence();
041: nextInProof = nip;
042: stepInto = ne;
043: programElement = prElement;
044: executionContext = exCont;
045: ContextInstantiationEntry cie = ((PosTacletApp) n
046: .getAppliedRuleApp()).instantiations()
047: .getContextInstantiation();
048: program = (cie.contextProgram());
049: }
050:
051: public TraceElement() {
052: nextInProof = this ;
053: }
054:
055: public PosInOccurrence getPosOfModality() {
056: return posOfModality;
057: }
058:
059: public ProgramElement getProgram() {
060: return program;
061: }
062:
063: public SourceElement getSrcElement() {
064: return programElement;
065: }
066:
067: public TraceElement getNextInProof() {
068: return nextInProof;
069: }
070:
071: public ContextTraceElement getNextExecuted() {
072: return stepInto;
073: }
074:
075: public IExecutionContext getExecutionContext() {
076: return executionContext;
077: }
078:
079: public void setExecutionContext(IExecutionContext con) {
080: executionContext = con;
081: }
082:
083: public void setNextInProof(TraceElement he) {
084: nextInProof = he;
085: }
086:
087: public void setStepInto(ContextTraceElement he) {
088: stepInto = he;
089: }
090:
091: public int serialNr() {
092: if (node == null)
093: return -1;
094: return node.serialNr();
095: }
096:
097: /* public ProgramElement getProgram(){
098: return posOfModality.subTerm().executableJavaBlock().program();
099: }*/
100:
101: public Node node() {
102: return node;
103: }
104:
105: public String toString() {
106: String s = "TraceElement:\n";
107: if (this == END)
108: return "END";
109: if (this == PARENTROOT)
110: return "PARENTROOT";
111: if (node != null)
112: s = s + (serialNr() + "\n");
113: if (programElement != null)
114: s = s + programElement;
115: if (stepInto != null)
116: s = s + "\nNext executed: " + stepInto.serialNr();
117: return s;
118: }
119:
120: }
|