Main.java Source File

00001 package gov.nasa.arc.ase.jpf.jvm;
00002 
00003 import gov.nasa.arc.ase.jpf.*;
00004 import gov.nasa.arc.ase.util.Debug;
00005 
00006 //#ifdef MARK_N_SWEEP && REFERENCE_COUNT
00007 
00008 //#endif MARK_N_SWEEP && REFERENCE_COUNT
00009 
00010 //#ifdef CHILDREN_LOOKAHEAD && !DISTRIBUTED
00011 
00012 //#endif CHILDREN_LOOKAHEAD && !DISTRIBUTED
00013 
00014 //#ifdef SIBLING_STORING && !DISTRIBUTED
00015 
00016 //#endif SIBLING_STORING && !DISTRIBUTED
00017 
00018 //#ifdef SIBLING_CACHING && !DISTRIBUTED
00019 
00020 //#endif SIBLING_CACHING && !DISTRIBUTED
00021 
00022 //#ifdef BUCHI && DISTRIBUTED
00023 
00024 //#endif BUCHI && DISTRIBUTED
00025 
00026 //#ifdef BUCHI && PARALLEL
00027 
00028 //#endif BUCHI && PARALLEL
00029 
00030 //#ifdef DISTRIBUTED && !NO_STATIC_SYMMETRY
00031 
00032 //#endif DISTRIBUTED && !NO_STATIC_SYMMETRY
00033 
00034 //#ifdef DISTRIBUTED && !NO_DYNAMIC_SYMMETRY
00035 
00036 //#endif DISTRIBUTED && !NO_DYNAMIC_SYMMETRY
00037 
00038 /**
00039  * Main is a class used to execute JPF with the Java virtual machine.
00040  *
00041  * @author  Flavio Lerda
00042  * @author  Willem Visser
00043  * @version 1.0
00044  * @since   1.0
00045  */
00046 public class Main {
00047   /**
00048    * A String containing the version of the Java virtual machine. This field is
00049    * used to output the version information by the Engine class.
00050    *
00051    * @see gov.nasa.arc.ase.jpf.Engine#start()
00052    */
00053 
00054   public static String VERSION = "JVM 0.1 - (C) 2000 RIACS/NASA Ames Research Center";
00055 
00056   /**
00057    * Executes the model checker. After parsing the arguments, it initializes
00058    * the virtual machine and executes the model checker engine.
00059    *
00060    * @param args  an array of strings containing the program arguments
00061    */
00062 
00063   public static void main(String args[]) {
00064     try {
00065       /* Creates the options and initializes them */
00066       Engine.options = VirtualMachine.options = new JVMOptions(Main.class);
00067       Engine.init(args);
00068 
00069 //#ifdef DISTRIBUTED
00070 
00071 
00072 
00073 
00074 
00075 
00076 
00077 
00078 
00079 
00080 //#endif DISTRIBUTED
00081 
00082 //#ifdef PARALLEL
00083 
00084 
00085 
00086 
00087 
00088 
00089 
00090 //#endif PARALLEL
00091 
00092       Engine.run(new VirtualMachine());
00093     } catch(JPFErrorException e) {
00094       Debug.println(Debug.ERROR, "jpf: " + e.getMessage());
00095 //#ifdef BANDERA
00096       if (Engine.options.bandera)
00097     throw new JPFErrorException("");
00098       else 
00099     System.exit(1);
00100 //#else BANDERA
00101 
00102 //#endif BANDERA
00103     }
00104   }  
00105 }