src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.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.event;
  20
  21 import gov.nasa.jpf.util.Predicate;
  22 import gov.nasa.jpf.vm.ChoiceGeneratorBase;
  23 import gov.nasa.jpf.vm.SystemState;
  24
  25
  26 /**
  27  * ChoiceGenerator for Events.
  28  * This is basically just a pointer into the event tree
  29  */
  30 public class EventChoiceGenerator extends ChoiceGeneratorBase<Event> {
  31
  32   protected Event base;
  33   protected Event cur;
  34   protected int nProcessed;
  35
  36   protected EventContext ctx; // optional, can replace/expand events during execution
  37
  38   /**
  39    * convenience method to get successors from current CG chain
  40    */
  41   public static EventChoiceGenerator getNext (SystemState ss, String id, Event base, EventContext ctx){
  42     EventChoiceGenerator cgPrev = ss.getLastChoiceGeneratorOfType(EventChoiceGenerator.class);
  43     if (cgPrev == null){
  44       return new EventChoiceGenerator( id, base, ctx);
  45     } else {
  46       return cgPrev.getSuccessor(id, ctx);
  47     }
  48   }
  49
  50   public EventChoiceGenerator (String id, Event base){
  51     this(id, base, null);
  52   }
  53
  54   public EventChoiceGenerator (String id, Event base, EventContext ctx) {
  55     super(id);
  56     this.base = base;
  57     this.ctx = ctx;
  58   }
  59
  60   @Override
  61   public Event getChoice (int idx){
  62     if (idx >= 0){
  63       Event e = base;
  64       for (int i=0; i<idx; i++){
  65         e = e.alt;
  66         if (e == null){
  67           break;
  68         } else {
  69           return e;
  70         }
  71       }
  72
  73     }
  74     throw new IllegalArgumentException("choice index out of range: " + idx);
  75   }
  76
  77
  78   public void setContextExpander (EventContext ctx){
  79     this.ctx = ctx;
  80   }
  81
  82   public boolean containsMatchingChoice (Predicate<Event> predicate){
  83     for (Event e = base; e != null; e = e.getAlt()){
  84       if (predicate.isTrue(e)){
  85         return true;
  86       }
  87     }
  88     return false;
  89   }
  90
  91   public void addChoice (Event newEvent){
  92     for (Event e = base; e != null;){
  93       Event eAlt = e.getAlt();
  94       if (eAlt == null){
  95         e.setAlt(newEvent);
  96         return;
  97       }
  98       e = eAlt;
  99     }
 100   }
 101
 102   public EventChoiceGenerator getSuccessor (String id){
 103     return getSuccessor(id, null);
 104   }
 105
 106   public EventChoiceGenerator getSuccessor (String id, EventContext ctx){
 107     if (cur == null){
 108       return new EventChoiceGenerator(id, base.getNext(), ctx);
 109
 110     } else {
 111       Event next = cur.getNext();
 112
 113       if (cur instanceof CheckEvent){ // CheckEvents use next for conjunction
 114         while (next instanceof CheckEvent){
 115           next = next.getNext();
 116         }
 117       }
 118
 119       if (next != null){
 120         return new EventChoiceGenerator( id, next, ctx);
 121       } else {
 122         return null; // done
 123       }
 124     }
 125   }
 126
 127   @Override
 128   public Event getNextChoice () {
 129     return cur;
 130   }
 131
 132
 133   @Override
 134   public boolean hasMoreChoices () {
 135     if (cur == null){
 136       return (nProcessed == 0);
 137     } else {
 138       return (cur.getAlt() != null);
 139     }
 140   }
 141
 142   @Override
 143   public void advance () {
 144     if (cur == null){
 145       if (nProcessed == 0){
 146         cur = base;
 147         nProcessed = 1;
 148       }
 149     } else {
 150       cur = cur.getAlt();
 151       nProcessed++;
 152     }
 153
 154     if (ctx != null){
 155       Event newCur = ctx.map(cur);
 156       if (newCur != cur){
 157         cur = newCur;
 158       }
 159     }
 160   }
 161
 162   @Override
 163   public void reset () {
 164     isDone = false;
 165     cur = null;
 166     nProcessed = 0;
 167   }
 168
 169   @Override
 170   public int getTotalNumberOfChoices () {
 171     return base.getNumberOfAlternatives() + 1; // include base itself
 172   }
 173
 174   @Override
 175   public int getProcessedNumberOfChoices () {
 176     return nProcessed;
 177   }
 178
 179   @Override
 180   public String toString() {
 181     StringBuilder sb = new StringBuilder(getClass().getName());
 182     sb.append("{id:\"");
 183     sb.append(id);
 184     sb.append('"');
 185
 186     //sb.append(",isCascaded:");
 187     //sb.append(Boolean.toString(isCascaded));
 188
 189     sb.append(",[");
 190     for (Event e=base; e!= null; e = e.getAlt()){
 191       if (e != base){
 192         sb.append(',');
 193       }
 194       if (e == cur){
 195         sb.append(MARKER);
 196       }
 197       sb.append(e.toString());
 198     }
 199     sb.append("],cur:");
 200     sb.append(cur);
 201     sb.append("}");
 202
 203     return sb.toString();
 204   }
 205
 206   @Override
 207   public Class<Event> getChoiceType() {
 208     return Event.class;
 209   }
 210
 211   protected Event[] getFirstNChoices(int n){
 212     Event[] a = new Event[n];
 213
 214     Event e = base;
 215     for (int i=0; i<n; i++){
 216       a[i] = e;
 217       e = e.getAlt();
 218     }
 219
 220     return a;
 221   }
 222
 223   @Override
 224   public Event[] getAllChoices(){
 225     return getFirstNChoices( getTotalNumberOfChoices());
 226   }
 227
 228   @Override
 229   public Event[] getProcessedChoices(){
 230     return getFirstNChoices( getProcessedNumberOfChoices());
 231   }
 232
 233   @Override
 234   public Event[] getUnprocessedChoices(){
 235     int n=0;
 236     for (Event e=cur; e != null; e = e.getAlt()){
 237       n++;
 238     }
 239
 240     Event[] a = new Event[n];
 241
 242     Event e = cur;
 243     for (int i=0; i<n; i++){
 244       a[i] = e;
 245       e = e.getAlt();
 246     }
 247
 248     return a;
 249   }
 250 }