src/main/gov/nasa/jpf/util/Trace.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18
  19 package gov.nasa.jpf.util;
  20
  21 import gov.nasa.jpf.ListenerAdapter;
  22 import gov.nasa.jpf.search.Search;
  23
  24 import java.util.ArrayList;
  25 import java.util.HashMap;
  26 import java.util.Iterator;
  27 import java.util.List;
  28
  29 /**
  30  * a generic, listener- created trace over property specific operations
  31  *
  32  * we could register this as a listener itself, but since it usually is used from
  33  * a listener, we might as well just delegate from there
  34  */
  35 public class Trace<T> extends ListenerAdapter implements Iterable<T> {
  36
  37   TraceElement<T> lastElement;
  38   TraceElement<T> lastTransition;
  39
  40   // for HeuristicSearches. Ok, that's braindead but at least no need for cloning
  41   HashMap<Integer,TraceElement<T>> storedTransition;
  42
  43
  44   // iterator that traverses the trace LIFO, i.e. starting from the last T
  45   class TraceIterator implements Iterator<T> {
  46
  47     TraceElement<T> cur;
  48
  49     TraceIterator () {
  50       cur = lastElement;
  51     }
  52
  53     @Override
  54         public boolean hasNext () {
  55       return (cur != null);
  56     }
  57
  58     @Override
  59         public T next () {
  60       if (cur != null){
  61         T op = cur.op;
  62         cur = cur.prevElement;
  63         return op;
  64       } else {
  65         return null;
  66       }
  67     }
  68
  69     @Override
  70         public void remove () {
  71       throw new UnsupportedOperationException("TraceElement removal not supported");
  72     }
  73   }
  74
  75   @Override
  76   public Iterator<T> iterator() {
  77     return new TraceIterator();
  78   }
  79
  80   public void addOp (T o){
  81     TraceElement<T> op = new TraceElement<T>(o);
  82
  83     if (lastElement == null){
  84       lastElement = op;
  85     } else {
  86       assert lastElement.stateId == 0;
  87
  88       op.prevElement = lastElement;
  89       lastElement = op;
  90     }
  91   }
  92
  93   public void removeLastOp() {
  94     if (lastElement != null){
  95       lastElement = lastElement.prevElement;
  96     }
  97   }
  98
  99   public T getLastOp() {
 100     if (lastElement != null) {
 101       return lastElement.getOp();
 102     }
 103
 104     return null;
 105   }
 106
 107   public int size() {
 108     int n=0;
 109     for (TraceElement<T> te = lastElement; te != null; te = te.prevElement) {
 110       n++;
 111     }
 112
 113     return n;
 114   }
 115
 116   public List<T> getOps () {
 117     // this is a rather braindead way around the limitation that we can't explicitly
 118     // create an T[] array object
 119
 120     ArrayList<T> list = new ArrayList<T>();
 121
 122     for (TraceElement<T> te = lastElement; te != null; te = te.prevElement) {
 123       list.add(te.getOp());
 124     }
 125
 126     // reverse
 127     for (int i=0, j=list.size()-1; i<j; i++, j--) {
 128       T tmp = list.get(j);
 129       list.set(j, list.get(i));
 130       list.set(i, tmp);
 131     }
 132
 133     return list;
 134   }
 135
 136   @Override
 137   public void stateAdvanced (Search search) {
 138     if (search.isNewState() && (lastElement != null)) {
 139       int stateId = search.getStateId();
 140
 141       for (TraceElement<T> op=lastElement; op != null; op=op.prevElement) {
 142         assert op.stateId == 0;
 143
 144         op.stateId = stateId;
 145       }
 146
 147       lastElement.prevTransition = lastTransition;
 148       lastTransition = lastElement;
 149     }
 150
 151     lastElement = null;
 152   }
 153
 154   @Override
 155   public void stateBacktracked (Search search){
 156     int stateId = search.getStateId();
 157     while ((lastTransition != null) && (lastTransition.stateId > stateId)){
 158       lastTransition = lastTransition.prevTransition;
 159     }
 160     lastElement = null;
 161   }
 162
 163   @Override
 164   public void stateStored (Search search) {
 165     if (storedTransition == null){
 166       storedTransition = new HashMap<Integer,TraceElement<T>>();
 167     }
 168
 169     // always called after stateAdvanced
 170     storedTransition.put(search.getStateId(), lastTransition);
 171   }
 172
 173   @Override
 174   public void stateRestored (Search search) {
 175     int stateId = search.getStateId();
 176     TraceElement<T> op = storedTransition.get(stateId);
 177     if (op != null) {
 178       lastTransition = op;
 179       storedTransition.remove(stateId);  // not strictly required, but we don't come back
 180     }
 181   }
 182
 183   @Override
 184   public Trace clone() {
 185     TraceElement<T> e0 = null, eLast = null;
 186
 187     for (TraceElement<T> e = lastElement; e != null; e = e.prevElement){
 188       TraceElement<T> ec = e.clone();
 189
 190       if (eLast != null){
 191         eLast.prevElement = ec;
 192         eLast = ec;
 193       } else {
 194         e0 = eLast = ec;
 195       }
 196     }
 197
 198     Trace<T> t = new Trace<T>();
 199     t.lastElement = e0;
 200
 201     return t;
 202   }
 203 }