iVirtualMachine.java Source File

00001 package gov.nasa.arc.ase.jpf;
00002 
00003 import java.util.*;
00004 import edu.ksu.cis.bandera.jjjc.decompiler.*;
00005 import java.lang.reflect.Method;
00006 
00007 public interface iVirtualMachine {
00008 // ifdef DISTRIBUTED
00009 
00010 
00011 // ifdef CHILDREN_LOOKAHEAD
00012 
00013 
00014 
00015 
00016 
00017 
00018 //#endif CHILDREN_LOOKAHEAD
00019 //#endif DISTRIBUTED
00020 
00021 // ifdef BUCHI
00022 
00023 
00024 
00025 
00026 
00027 
00028 
00029 
00030 
00031 //#endif BUCHI
00032  public boolean         Backtrack(); 
00033  public boolean         CheckInvariant(iProperty p); 
00034  public FilenameLinePair        ErrorBackward(); 
00035  public FilenameLinePair        ErrorForward(); 
00036  /************************************************************/
00037 
00038 
00039 
00040  public FilenameLinePair        ErrorInit(); 
00041  public int                     ErrorPathLength(); 
00042  public int         Forward(); 
00043  public ErrorTrailInterface getErrorTrail(); 
00044  public Path                    getErrorTrail_from_file(); 
00045  /************************************************************/
00046  public Path                    getErrorTrail_to_file(); 
00047  public Path                    getErrorTrail1(); 
00048  public iKernelState        getKernelState(); 
00049  public iSystemState        getSystemState(); 
00050  public int                     nextThreadToExecute(); 
00051  public int                     previousThreadToExecute(); 
00052  public void            ShowErrorTrail(); 
00053  public void            ShowErrorTrail(Path p); 
00054  public int         simForward(); // for simulation  
00055  public void                    SimulateErrorTrail(Path p); 
00056 }