Store.java Source File

00001 package gov.nasa.arc.ase.jpf;
00002 
00003 import gov.nasa.arc.ase.jpf.jvm.ArrayWrapper;
00004 import gov.nasa.arc.ase.jpf.jvm.VirtualMachine;
00005 import gov.nasa.arc.ase.util.Cache;
00006 import gov.nasa.arc.ase.util.Debug;
00007 import java.util.*;
00008 
00009 public class Store implements iStore {
00010   private static Object NULL = new Object();
00011   private Hashtable store = new Hashtable();
00012   private Cache cache;
00013   private int size = 0;
00014   private int cls = -1;
00015 
00016 // ifdef BUCHI
00017 
00018 // ifdef NO_COMPRESSION
00019 
00020 //#else NO_COMPRESSION
00021 
00022 //#endif NO_COMPRESSION
00023 
00024 
00025 
00026 
00027 
00028 
00029 // ifdef NO_COMPRESSION
00030 
00031 
00032 //#endif NO_COMPRESSION
00033 
00034 
00035 
00036 
00037 //#endif BUCHI
00038   public Store() {
00039 // ifdef DISTRIBUTED
00040 // ifdef SIBLING_CACHING
00041 
00042 
00043 //#endif SIBLING_CACHING
00044 //#endif DISTRIBUTED
00045   }  
00046 // ifdef DISTRIBUTED
00047 
00048 
00049 
00050 
00051 // ifdef SIBLING_STORING
00052 
00053 // ifdef SIBLING_STORING
00054 
00055 // ifdef NO_COMPRESSION
00056 
00057 //#else NO_COMPRESSION
00058 
00059 //#endif NO_COMPRESSION
00060 
00061 
00062 
00063 // ifdef DEBUG_DISTRIBUTED
00064 
00065 //#endif DEBUG_DISTRIBUTED
00066 
00067 
00068 
00069 
00070 
00071 
00072 
00073 //#endif SIBLING_STORING
00074 // ifdef SIBLING_CACHING
00075 
00076 // ifdef NO_COMPRESSION
00077 
00078 //#else NO_COMPRESSION
00079 
00080 //#endif NO_COMPRESSION
00081 
00082 
00083 
00084 
00085 
00086 // ifdef DEBUG_DISTRIBUTED
00087 
00088 //#endif DEBUG_DISTRIBUTED
00089 
00090 
00091 
00092 
00093 //#endif SIBLING_CACHING
00094 
00095 
00096 
00097 //#endif SIBLING_STORING
00098 //#endif DISTRIBUTED
00099 
00100   public int getSize() {
00101     return size;
00102   }  
00103   public void initial(iKernelState state) {
00104 // ifdef BUCHI
00105 
00106 //#endif BUCHI
00107 
00108 // ifdef DISTRIBUTED
00109 
00110 
00111 
00112 
00113 
00114 // ifdef DEBUG_SEARCH
00115 
00116 //#endif DEBUG_SEARCH
00117 
00118 
00119 
00120 
00121 //#endif DISTRIBUTED
00122 // ifdef NO_COMPRESSION
00123 
00124 //#else NO_COMPRESSION
00125       Object o = state.getStoringData();
00126 //#endif NO_COMPRESSION
00127 
00128       store.put(o, NULL);
00129 // ifdef NO_COMPRESSION
00130       Runner.storage_memory += ((gov.nasa.arc.ase.jpf.jvm.ArrayWrapper)o).size();
00131       size += ((gov.nasa.arc.ase.jpf.jvm.ArrayWrapper)o).size();
00132 //#endif NO_COMPRESSION
00133 // ifdef DISTRIBUTED
00134 
00135 //#endif DISTRIBUTED
00136   }  
00137   public int lastClass() {
00138     return cls;
00139   }  
00140   public boolean put(iKernelState state){
00141 // ifdef DISTRIBUTED
00142 
00143 
00144 
00145 
00146 // ifdef CHILDREN_LOOKAHEAD
00147 
00148 
00149 
00150 //#endif CHILDREN_LOOKAHEAD
00151 
00152 // ifdef CHILDREN_LOOKAHEAD
00153 
00154 
00155 
00156 // ifdef DEBUG_SEARCH
00157 
00158 //#endif DEBUG_SEARCH
00159 
00160 
00161 
00162 
00163 
00164 
00165 // ifdef DEBUG_SEARCH
00166 
00167 //#endif DEBUG_SEARCH
00168 
00169 
00170 
00171 
00172 
00173 
00174 //#endif CHILDREN_LOOKAHEAD
00175 
00176 // ifdef SIBLING_STORING
00177 
00178 //#else SIBLING_STORING
00179 
00180 // ifdef SIBLING_STORING
00181 
00182 //#endif SIBLING_STORING
00183 
00184 // ifdef SIBLING_CACHING
00185 
00186 //#endif SIBLING_CACHING
00187 
00188 //#endif SIBLING_STORING
00189 
00190 // ifdef SIBLING_STORING
00191 // ifdef DEBUG_DISTRIBUTED
00192 
00193 //#endif DEBUG_DISTRIBUTED
00194 
00195 
00196 
00197 //#endif SIBLING_STORING
00198 
00199 
00200 // ifdef CHILDREN_LOOKAHEAD
00201 
00202 
00203 //#endif CHILDREN_LOOKAHEAD
00204 
00205 
00206 
00207 
00208 // ifdef DEBUG_DISTRIBUTED
00209 
00210 //#endif DEBUG_DISTRIBUTED
00211 
00212 
00213 // ifdef DEBUG_SEARCH
00214 
00215 //#endif DEBUG_SEARCH
00216 // ifdef CHILDREN_LOOKAHEAD
00217 
00218 
00219 
00220 
00221 //#endif CHILDREN_LOOKAHEAD
00222 
00223 
00224 
00225 //#endif DISTRIBUTED
00226 
00227 // ifdef NO_COMPRESSION
00228 
00229 //#else NO_COMPRESSION
00230     Object o = state.getStoringData();
00231 //#endif NO_COMPRESSION
00232 
00233     if (store.containsKey(o)) return false;
00234 
00235     store.put(o, NULL);
00236 // ifdef NO_COMPRESSION
00237     Runner.storage_memory += ((gov.nasa.arc.ase.jpf.jvm.ArrayWrapper)o).size();
00238     size += ((gov.nasa.arc.ase.jpf.jvm.ArrayWrapper)o).size();
00239 //#endif NO_COMPRESSION
00240 
00241     return true;
00242   }  
00243   public void setSize(int s) {
00244     size = s;
00245   }  
00246   public void switchTo(int c, Hashtable ht, int s) {
00247     cls = c;
00248     store = ht;
00249     size = s;
00250   }  
00251 }