src/main/gov/nasa/jpf/vm/Transition.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 package gov.nasa.jpf.vm;
  19
  20 import java.util.Iterator;
  21
  22 /**
  23  * concrete type to store execution paths. TrailInfo corresponds to Transition,
  24  * i.e. all instructions executed in the context of a vm.forward() leading
  25  * into a new state
  26  */
  27 public class Transition implements Iterable<Step>, Cloneable {
  28
  29   ChoiceGenerator<?> cg;
  30   ThreadInfo ti;
  31
  32   private Step   first, last;
  33   int nSteps;
  34
  35   private Object annotation;
  36   String         output;
  37
  38   private int stateId = StateSet.UNKNOWN_ID;
  39
  40   public Transition (ChoiceGenerator<?> cg, ThreadInfo ti) {
  41     this.cg = cg;
  42     this.ti = ti;
  43   }
  44
  45   @Override
  46   public Object clone() {
  47     try {
  48       Transition t = (Transition)super.clone();
  49
  50       // the deep copy references
  51       t.cg = cg.clone();
  52       t.ti = (ThreadInfo)ti.clone();
  53
  54       return t;
  55
  56     } catch (CloneNotSupportedException cnsx){
  57       return null; // cannot happen
  58     }
  59   }
  60
  61   public String getLabel () {
  62     if (last != null) {
  63       return last.getLineString();
  64     } else {
  65       return "?";
  66     }
  67   }
  68
  69   public int getStateId() {
  70     return(stateId);
  71   }
  72
  73   public void setStateId(int id) {
  74     stateId = id;
  75   }
  76
  77   public void setOutput (String s) {
  78     output = s;
  79   }
  80
  81   public void setAnnotation (Object o) {
  82     annotation = o;
  83   }
  84
  85   public Object getAnnotation () {
  86     return annotation;
  87   }
  88
  89   public String getOutput () {
  90     return output;
  91   }
  92
  93   // don't use this for step iteration - this is very inefficient
  94   public Step getStep (int index) {
  95     Step s = first;
  96     for (int i=0; s != null && i < index; i++) s = s.next;
  97     return s;
  98   }
  99
 100   public Step getLastStep () {
 101     return last;
 102   }
 103
 104   public int getStepCount () {
 105     return nSteps;
 106   }
 107
 108   public ThreadInfo getThreadInfo() {
 109     return ti;
 110   }
 111
 112   public int getThreadIndex () {
 113     return ti.getId();
 114   }
 115
 116   public ChoiceGenerator<?> getChoiceGenerator() {
 117     return cg;
 118   }
 119
 120   public ChoiceGenerator<?>[] getChoiceGeneratorCascade(){
 121     return cg.getCascade();
 122   }
 123
 124   public void incStepCount() {
 125     nSteps++;
 126   }
 127
 128   void addStep (Step step) {
 129     if (first == null) {
 130       first = step;
 131       last = step;
 132     } else {
 133       last.next = step;
 134       last = step;
 135     }
 136     nSteps++;
 137   }
 138
 139   public class StepIterator implements Iterator<Step> {
 140     Step cur;
 141
 142     @Override
 143         public boolean hasNext () {
 144       return (cur != last);
 145     }
 146
 147     @Override
 148         public Step next () {
 149       if (cur == null) {
 150         cur = first;
 151       } else {
 152         if (cur != last) {
 153           cur = cur.next;
 154         } else {
 155           return null;
 156         }
 157       }
 158       return cur;
 159     }
 160
 161     @Override
 162         public void remove () {
 163       if (cur == null) {
 164         first = first.next;
 165       } else {
 166         Step s;
 167         for (s = first; s.next != cur; s = s.next);
 168         s.next = cur.next;
 169         cur = cur.next;
 170       }
 171     }
 172   }
 173
 174   @Override
 175   public Iterator<Step> iterator () {
 176     return new StepIterator();
 177   }
 178 }