データ定義部分を中心にいい加減に抜粋

class KernelState implements Restorable {
  public Heap heap;
  public ThreadList threads;
  public ClassLoaderList classLoaders;
  private Stack listeners;
               // current listeners waiting for notification of next change.

  static class KsMemento implements Memento {
    Memento threadsMemento;
    Memento cloadersMemento;
    Memento heapMemento;
    public KernelState restore (KernelState ks) {...}
  }
  ...
}

public class SystemState {
  static class Memento {
    ChoiceGenerator curCg;
    ChoiceGenerator nextCg;
    int atomicLevel;
    ChoicePoint trace;
    ThreadInfo execThread;
    int id;              // the state id
    LinkedHashMap restorers;
    ...
    void restore (SystemState ss) {...}
  }
  
  static class RestorableMemento extends Memento { // expensive
    void backtrack (SystemState ss) {...}
    void restore (SystemState ss) {...}
  }

  int id;                   /** the state id */
  ChoiceGenerator nextCg;
  ChoiceGenerator  curCg;
  ThreadInfo execThread;    
  LinkedHashMap restorers;
  public KernelState ks;
  public Transition trail;      /** trace information */
  boolean retainAttributes;
  boolean isIgnored;
  boolean isForced;  // treat this as a new state
  boolean isInteresting;
  boolean isBoring;
  boolean isBlockedInAtomicSection;
  public UncaughtException uncaughtException;
  boolean GCNeeded = false;
  int maxAllocGC;  // for an optimization
  int nAlloc;      // for an optimization
  int atomicLevel;
  int entryAtomicLevel;
  SchedulerFactory schedulerFactory;
  boolean recordSteps;
  ...
}