src/main/gov/nasa/jpf/vm/ChoiceGenerator.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 gov.nasa.jpf.util.ObjectList;
  21
  22 import java.util.Comparator;
  23
  24 /**
  25  * generic interface for configurable choice generators
  26  */
  27 public interface ChoiceGenerator<T> extends Cloneable {
  28
  29   //--- the basic ChoiceGenerator interface, mostly used by SystemState
  30
  31   T getNextChoice();
  32
  33   Class<T> getChoiceType();
  34
  35   boolean hasMoreChoices();
  36
  37   /**
  38    * to be called before the first advance(). Can be used in implementors to
  39    * initialize choices from context (similar to what listeners can do from
  40    * choiceGeneratorSet() notifications)
  41    */
  42   void setCurrent();
  43
  44   /**
  45    * advance to the next choice. This is the only method that really
  46    * advances our enumeration
  47    */
  48   void advance();
  49
  50   void advance(int nChoices);
  51
  52   void select(int nChoice);
  53
  54   boolean isDone();
  55
  56   void setDone();
  57
  58   boolean isProcessed();
  59
  60   /**
  61    *  this has to reset the CG to its initial state, which includes resetting
  62    * 'isDone'
  63    */
  64   void reset();
  65
  66   int getTotalNumberOfChoices();
  67
  68   int getProcessedNumberOfChoices();
  69
  70
  71   // choice getters. Note that not all CGs need to support them since
  72   // there is no requirement that CGs compute finite choice sets upon creation
  73
  74   T getChoice(int i);
  75   T[] getAllChoices();
  76   T[] getProcessedChoices();
  77   T[] getUnprocessedChoices();
  78
  79   ChoiceGenerator<?> getPreviousChoiceGenerator();
  80
  81   int getNumberOfParents();
  82
  83   /**
  84    * turn the order of choices random (if it isn't already). Only
  85    * drawback of this generic method (which might be a decorator
  86    * factory) is that our type layer (e.g. IntChoiceGenerator)
  87    * has to guarantee type safety. But hey - this is the first case where
  88    * we can use covariant return types!
  89    *
  90    * NOTES:
  91    * - this method may alter this ChoiceGenerator and return that or return
  92    * a new "decorated" version.
  93    * - random data can be read from the "Random random" field in this class.
  94    */
  95   ChoiceGenerator<T> randomize();
  96
  97   ChoiceGenerator<?> clone() throws CloneNotSupportedException;
  98
  99   ChoiceGenerator<?> deepClone() throws CloneNotSupportedException;
 100
 101   String getId();
 102
 103   int getIdRef();
 104
 105   void setIdRef(int idRef);
 106
 107   void setId(String id);
 108
 109   boolean isSchedulingPoint();
 110
 111   //--- the getters and setters for the CG creation info
 112   void setThreadInfo(ThreadInfo ti);
 113
 114   ThreadInfo getThreadInfo();
 115
 116   void setInsn(Instruction insn);
 117
 118   Instruction getInsn();
 119
 120   void setContext(ThreadInfo tiCreator);
 121
 122   void setStateId (int stateId);
 123
 124   int getStateId ();
 125
 126   String getSourceLocation();
 127
 128   boolean supportsReordering();
 129
 130   /**
 131    * reorder according to a user provided comparator
 132    * @returns instance to reordered CG of same choice type,
 133    * null if not supported by particular CG subclass
 134    *
 135    * Note: this should only be called before the first advance, since it
 136    * can reset the CG enumeration status
 137    */
 138   ChoiceGenerator<T> reorder (Comparator<T> comparator);
 139
 140   void setPreviousChoiceGenerator(ChoiceGenerator<?> cg);
 141
 142
 143   void setCascaded();
 144
 145   boolean isCascaded();
 146
 147   <T extends ChoiceGenerator<?>> T getPreviousChoiceGeneratorOfType(Class<T> cls);
 148
 149   /**
 150    * returns the prev CG if it was registered for the same insn
 151    */
 152   ChoiceGenerator<?> getCascadedParent();
 153
 154   /**
 155    * return array with all cascaded parents and this CG, in registration order
 156    */
 157   ChoiceGenerator<?>[] getCascade();
 158
 159   /**
 160    * return array with all parents and this CG, in registration order
 161    */
 162   ChoiceGenerator<?>[] getAll();
 163
 164   /**
 165    * return array with all CGs (including this one) of given 'cgType', in registration order
 166    */
 167   <C extends ChoiceGenerator<?>> C[] getAllOfType(Class<C> cgType);
 168
 169
 170   //--- the generic attribute API
 171   boolean hasAttr();
 172
 173   boolean hasAttr(Class<?> attrType);
 174
 175   /**
 176    * this returns all of them - use either if you know there will be only
 177    * one attribute at a time, or check/process result with ObjectList
 178    */
 179   Object getAttr();
 180
 181   /**
 182    * this replaces all of them - use only if you know
 183    *  - there will be only one attribute at a time
 184    *  - you obtained the value you set by a previous getXAttr()
 185    *  - you constructed a multi value list with ObjectList.createList()
 186    */
 187   void setAttr(Object a);
 188
 189   void addAttr(Object a);
 190
 191   void removeAttr(Object a);
 192
 193   void replaceAttr(Object oldAttr, Object newAttr);
 194
 195   /**
 196    * this only returns the first attr of this type, there can be more
 197    * if you don't use client private types or the provided type is too general
 198    */
 199   <A> A getAttr(Class<A> attrType);
 200
 201   <A> A getNextAttr(Class<A> attrType, Object prev);
 202
 203   ObjectList.Iterator attrIterator();
 204
 205   <A> ObjectList.TypedIterator<A> attrIterator(Class<A> attrType);
 206
 207 }