---

Store.java

package gov.nasa.arc.ase.jpf;

import gov.nasa.arc.ase.util.Cache;
import gov.nasa.arc.ase.util.Debug;
import java.util.Hashtable;

public class Store implements iStore {
  private static Boolean OnStack = new Boolean(true);
  private static Boolean OffStack = new Boolean(false);
  private Hashtable store = new Hashtable();

//#endif BUCHI
  public Store() {
  }  
//#ifdef BUCHI
  public BuchiSet BuchiGet(iSystemState state) {
    Object o = state.getData();

//#ifdef DEBUG

//#endif DEBUG
    BuchiSet buchis = (BuchiSet)store.get(o);

    if(buchis == null) {
      buchis = new BuchiSet();
      store.put(o, buchis);
      Engine.getJPF().status.unique++;
      Engine.getJPF().status.storageMemory += state.getDataSize(o);
    }

    return buchis;
  }  
  public int check(iSystemState state) {
    return check(state.getData());
  }  
  public int check(Object o) {
    if(store.containsKey(o)) {
      Boolean b = (Boolean)store.get(o);

      if(b.booleanValue())
    return ONSTACK;

      return OFFSTACK;
    }

    return NEW;
  }  
  public void initial(iVirtualMachine vm) {
//#ifdef BUCHI
    if(Engine.options.buchi != null) return;
//#endif BUCHI

    iSystemState state = vm.getSystemState();
    Object o = state.getData();

    store.put(o, OnStack);

    Engine.getJPF().status.storageMemory += state.getDataSize(o);
  }  
  public void offStack(iSystemState state) {
//#ifdef BUCHI
    if(Engine.options.buchi != null) return;
//#endif BUCHI
    store.put(state.getData(), OffStack);
  }  
  public int put(iVirtualMachine vm) {
    iSystemState state = vm.getSystemState();
    Object o = state.getData();
    int r = check(o);

    if(r == NEW) {
      store.put(o, OnStack);
      Engine.getJPF().status.storageMemory += state.getDataSize(o);
    }

    return r;
  }  
  public int put2(iSystemState state) {
    return check(state.getData());
  }  
}

---