Java PathFinder where to start?

When I started writing my tool, I realized it is a good idea to read the code of the great tool that several great people(?) have contributed---the Java PathFinder (JPF).
The entry point for reading Java PathFinder may be at

• gov.nasa.jpf.tools.JavaJPF : main() is here.
• gov.nasa.jpf.JPF : main class for JPF verification framework. It reads config, instantiates the Search and VM objects, and starts the Search.
• gov.nasa.jpf.jvm.JVM : the class for virtual machine that can move forward / backward one transition at a time.
• Besides, ThreadInfo, MethodInfo in gov.nasa.jpf.jvm are also worth looking.