working on directto benchmark--removing code like unused constructors that hinder...

diff --git a/Robust/src/Benchmarks/mlp/directto/README.txt b/Robust/src/Benchmarks/mlp/directto/README.txt
index 3bc08bec034a0147609c1806247c29b891d9bf10..79c28d6c2a74638fc418e4ab10ae86a3b03b7e5c 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/README.txt
+++ b/Robust/src/Benchmarks/mlp/directto/README.txt
@@ -1,3 +1,63 @@
-The DirectTo benchmark reads in a text file to build a list of
-messages for tracking and routing aircraft without conflicts.
+Any statement *** in asterix *** is an assertion that
+disjoint reachability analysis should be able to verify.
 
+The DirectTo benchmark executes a list of messages from 
+an input file to solve a safe aircraft routing problem.
+
+The D2 (direct-to) singleton object has a singleton 
+reference to:
+ -ReadWrite, reads input file, creates messages
+ -MessageList, commands to execute for building problem
+ -Static, structure of static constants from input file
+ -AircraftList, all types of aircraft in problem
+ -FlightList, list of flights in algorithm
+ -FixList, list of fixes algorithm computes
+ -Algorithm, reads from Static
+ -TrajectorySynthesizer, reads from Static
+ -Flight, why a singleton Flight object?
+so:
+*** all memory in the program should be reachable from
+at most one of any singleton (D2, Static, etc) ***
+
+MessageList has a Vector of Message objects, where each
+one specifys an effect for other structures such as 
+setting a constant in the Static singleton, or adding
+an aircraft type to the Aircraft list, etc.  Message
+objects themselves only have references that are freshly
+allocated, so:
+*** Message objects should be disjoint ***
+
+The ReadWrite singleton appends new Message objects
+to the MessageList and has no references of its own,
+*** Nothing is reachable from a ReadWrite ***
+
+The Static singleton has primitive members, so
+*** Nothing is reachable from a Static ***
+
+AircraftList has a Vector of Aircraft objects, where
+each one has a String for type and some primitive
+attributes, where the type is generated from a
+StringTokenizer (getting a token gets a new String),
+and in practice is disjoint for every Aircraft, so:
+*** Aircraft objects should be disjoint ***
+
+FixList has a Vector of Fix objects, where each one
+has a String name and a Point2d (an alternate point
+in a flight plan?).  I believe they are not modified
+after being built from freshly allocated tokenizing,
+*** Fix objects should be disjoint ***
+
+FlightList has a Vector of Flight objects which have
+several fresh, set-once references (flightID String, 
+a Track, etc).
+Flight objects may share Aircraft (types),
+
+
+
+In Message.executeMessage(), if you comment out every
+message handler except any one of these, they cause 
+Message objects to show sharing:
+ - FlightList.addFlightPlan()
+ - FlightList.amendFlightInfo()
+ - FlightList.amendFlightPlan() (still a quick analysis!)
+ - FlightList.sendingAircraft()

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java
index 477e9d3495ce9661cf29e790f3459da801463115..ae30bed3821eb3732006499638fd1012de58b2d9 100755 (executable)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/D2.java
@@ -7,24 +7,22 @@
 public class D2 {
 
   public ReadWrite             singletonReadWrite            ; public ReadWrite             getReadWrite            () { return singletonReadWrite            ; }
+  public MessageList          singletonMessageList          ; public MessageList           getMessageList          () { return singletonMessageList          ; }
   public Static                singletonStatic               ; public Static                getStatic               () { return singletonStatic               ; }
   public AircraftList         singletonAircraftList         ; public AircraftList          getAircraftList         () { return singletonAircraftList         ; }   
-  public Algorithm            singletonAlgorithm            ; public Algorithm             getAlgorithm            () { return singletonAlgorithm            ; }
-  public FixList               singletonFixList                     ; public FixList               getFixList              () { return singletonFixList              ; }
-  public Flight                singletonFlight              ; public Flight                getFlight               () { return singletonFlight               ; }
   public FlightList           singletonFlightList           ; public FlightList            getFlightList           () { return singletonFlightList           ; }
-  public MessageList          singletonMessageList          ; public MessageList           getMessageList          () { return singletonMessageList          ; }
+  public FixList               singletonFixList                     ; public FixList               getFixList              () { return singletonFixList              ; }
+  public Algorithm            singletonAlgorithm            ; public Algorithm             getAlgorithm            () { return singletonAlgorithm            ; }
   public TrajectorySynthesizer singletonTrajectorySynthesizer; public TrajectorySynthesizer getTrajectorySynthesizer() { return singletonTrajectorySynthesizer; }
 
   public D2() {
     singletonReadWrite             = new ReadWrite            ();
+    singletonMessageList          = new MessageList          ();
     singletonStatic                = new Static               ();
     singletonAircraftList         = new AircraftList         ();
+    singletonFlightList                   = new FlightList           (); 
     singletonFixList              = new FixList              ();
     singletonAlgorithm            = new Algorithm            ();
-    singletonFlight                = new Flight               ("");
-    singletonFlightList                   = new FlightList           (); 
-    singletonMessageList          = new MessageList          ();
     singletonTrajectorySynthesizer = new TrajectorySynthesizer();
   }
 

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java
index d0cd5dce378f5a25ec76d79ce9bd4f9f11130ef5..9167b75ecadd2c0ba6dfaa145a3b8f24e2b87835 100755 (executable)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java
@@ -11,12 +11,6 @@ public class FlightList {
     f=new Vector(100);
   }
 
-  /*
-  public void addFlight(int index, Flight flight) {
-    f.addElement(index,flight);
-  }
-  */
-
   public  void addFlightPlan(D2 d2, int time, StringTokenizer st) { 
     Flight newFlight=disjoint flightAdd new Flight(st.nextToken());
     noFlights++;

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java
index 08c7e4f6bb8f762c07f158fa185f578715723583..f83a2e3ce755b947b13d610bd14281a1f089d58e 100755 (executable)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/Message.java
@@ -11,12 +11,6 @@ public class Message {
     this.parameters=parameters;
   }
 
-  public Message(Message m) {
-    this.time=m.time;
-    this.type=m.type;
-    this.parameters=m.parameters;
-  }
-
   public void executeMessage(D2 d2) {
     System.out.println("Executing message of type "+type);
 

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile b/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile
index 6892efc2e0b637206f7c77b469f5b9b028770eeb..df0027f98719a6dcf3a3c101c64bd160c69e52a7 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile
@@ -4,7 +4,7 @@ PROGRAM=test
 SOURCE_FILES=D2.java #smalltest.java
 
 BUILDSCRIPT=~/research/Robust/src/buildscript
-BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) -justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions
+BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) #-justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions
 
 all: $(PROGRAM).bin
 

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java
index 5a0c06f93ed2bcdd7219c3fee907f7d97a0ed1d4..6ebd0b5bbca1cf9a6e6ff1c3438fbe4c8077dfc6 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/D2.java
@@ -5,54 +5,44 @@
 //import java.io.*;
 
 public class D2 {
-  public ReadWrite rw;
 
-  private Static                singletonStatic               ; public Static                getStatic               () { return singletonStatic               ; }
-  private AircraftList         singletonAircraftList         ; public AircraftList          getAircraftList         () { return singletonAircraftList         ; }   
-  private Algorithm            singletonAlgorithm            ; public Algorithm             getAlgorithm            () { return singletonAlgorithm            ; }
-  private FixList              singletonFixList              ; public FixList               getFixList              () { return singletonFixList              ; }
-  private Flight               singletonFlight               ; public Flight                getFlight               () { return singletonFlight               ; }
-  private FlightList           singletonFlightList           ; public FlightList            getFlightList           () { return singletonFlightList           ; }
-  private MessageList          singletonMessageList          ; public MessageList           getMessageList          () { return singletonMessageList          ; }
-  private TrajectorySynthesizer singletonTrajectorySynthesizer; public TrajectorySynthesizer getTrajectorySynthesizer() { return singletonTrajectorySynthesizer; }
+  public ReadWrite             singletonReadWrite            ; public ReadWrite             getReadWrite            () { return singletonReadWrite            ; }
+  public MessageList          singletonMessageList          ; public MessageList           getMessageList          () { return singletonMessageList          ; }
+  public Static                singletonStatic               ; public Static                getStatic               () { return singletonStatic               ; }
+  public AircraftList         singletonAircraftList         ; public AircraftList          getAircraftList         () { return singletonAircraftList         ; }   
+  public FlightList           singletonFlightList           ; public FlightList            getFlightList           () { return singletonFlightList           ; }
+  public FixList               singletonFixList                     ; public FixList               getFixList              () { return singletonFixList              ; }
+  public Algorithm            singletonAlgorithm            ; public Algorithm             getAlgorithm            () { return singletonAlgorithm            ; }
+  public TrajectorySynthesizer singletonTrajectorySynthesizer; public TrajectorySynthesizer getTrajectorySynthesizer() { return singletonTrajectorySynthesizer; }
 
   public D2() {
+    singletonReadWrite             = new ReadWrite            ();
+    singletonMessageList          = new MessageList          ();
     singletonStatic                = new Static               ();
     singletonAircraftList         = new AircraftList         ();
+    singletonFlightList                   = new FlightList           (); 
     singletonFixList              = new FixList              ();
     singletonAlgorithm            = new Algorithm            ();
-    singletonFlight                = new Flight               ( "" );
-    singletonFlightList                   = new FlightList           (); 
-    singletonMessageList          = new MessageList          ();
-    singletonTrajectorySynthesizer = new TrajectorySynthesizer();
+    singletonTrajectorySynthesizer = new TrajectorySynthesizer();    
   }
 
   public static void main(String arg[]) {
     System.out.println("D2 - Application started");
 
     D2 d2 = new D2();
-
-    
-    d2.rw=new ReadWrite();
-    d2.rw.read(d2);
     
-
+    d2.getReadWrite().read(d2);
+        
     d2.getMessageList().executeAll(d2);
     
-    int count = 0;
+    /*
     while( d2.getFlightList().anyPlanesAlive() ) {
-       //      d2.getAlgorithm().doIteration(d2);
-      
-      count++;
-      if( count % 10000 == 0 ) {
-       //System.out.println( "iteration "+count );
-      }
-
-      if( count == 1000 ) {
-       break;
-      }
+      d2.getAlgorithm().doIteration(d2);
     }
 
-    d2.rw.write(d2);
+    d2.getReadWrite().write(d2);
+    */
+
+    System.out.println("D2 - Application finished");
   }
 }

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java
index b5bae9c52700a030c3b1810798ced48c072810ec..baad640cf1168a3888b84461344f79f62b88177e 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Flight.java
@@ -48,7 +48,7 @@ public class Flight /*implements Cloneable*/ {
   }
 
   public static Flight copyOf(Flight f) {
-    Flight fNew       = disjoint flightCopy new Flight(f.flightID);
+    Flight fNew       = /*disjoint flightCopy*/ new Flight(f.flightID);
     fNew.trialStatus  = f.trialStatus;
     fNew.aircraftType = f.aircraftType;
     fNew.track        = f.track;

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java
index d0cd5dce378f5a25ec76d79ce9bd4f9f11130ef5..1d9a500aa2b1334e598c950365a5f9d330a6bb07 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/FlightList.java
@@ -11,14 +11,8 @@ public class FlightList {
     f=new Vector(100);
   }
 
-  /*
-  public void addFlight(int index, Flight flight) {
-    f.addElement(index,flight);
-  }
-  */
-
   public  void addFlightPlan(D2 d2, int time, StringTokenizer st) { 
-    Flight newFlight=disjoint flightAdd new Flight(st.nextToken());
+    Flight newFlight=/*disjoint flightAdd*/ new Flight(st.nextToken());
     noFlights++;
     f.addElement(newFlight);
 

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java
index f002f4a50397e629943082aa66600948a2ba85d5..30542b6997430bde9f867b6eddab2236d990ab78 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/Message.java
@@ -11,17 +11,11 @@ public class Message {
     this.parameters=parameters;
   }
 
-  public Message(Message m) {
-    this.time=m.time;
-    this.type=m.type;
-    this.parameters=m.parameters;
-  }
-
   public void executeMessage(D2 d2) {
     System.out.println("Executing message of type "+type);
 
+    //static messages    
     /*
-    //static messages
     if (type.compareTo("SET_MAP_SIZE")==0) {
       System.out.println("Setting the map size...");
       d2.getStatic().setMapSize(parameters);
@@ -45,37 +39,44 @@ public class Message {
     else if (type.compareTo("REMOVE_FIX")==0) {
       System.out.println("Removing a fix...");
       d2.getFixList().removeFix(parameters);
-    }
-    else*/ if (type.compareTo("ADD_AIRCRAFT")==0) {
+    }   
+    else if (type.compareTo("ADD_AIRCRAFT")==0) {
       System.out.println("Adding an aircraft...");
       d2.getAircraftList().addAircraft(parameters);
-    } else
-    /*
+    }
     else if (type.compareTo("REMOVE_AIRCRAFT")==0) {
       System.out.println("Removing an aircraft...");
       d2.getAircraftList().removeAircraft(parameters);
     }
-    //dynamic messages
+    */
+
+    //dynamic messages    
+    /*
     if (type.compareTo("DO_WORK")==0)
       d2.getAlgorithm().setInitialTime(time);
     */
+
+    /*
     if (type.compareTo("ADD_FLIGHT_PLAN")==0) {
       System.out.println("Adding flight plan...");
       d2.getFlightList().addFlightPlan(d2,time,parameters);
     }
-    /*
-    else if (type.compareTo("REMOVE_FLIGHT_PLAN")==0) {
+    */
+
+
+    /*else if (type.compareTo("REMOVE_FLIGHT_PLAN")==0) {
       System.out.println("Removing flight plan...");
       d2.getFlightList().removeFlightPlan(time,parameters);            
-    }
+    }    
     else if (type.compareTo("AMEND_FLIGHT_INFO")==0) {
       System.out.println("Amending flight info...");
       d2.getFlightList().amendFlightInfo(d2, time,parameters);
-    }              
-    else if (type.compareTo("AMEND_FLIGHT_PLAN")==0) {
+    }      
+    else*/ if (type.compareTo("AMEND_FLIGHT_PLAN")==0) {
       System.out.println("Amending flight plan...");
       d2.getFlightList().amendFlightPlan(d2, time,parameters);        
-    }
+    }    
+    /*
     else if (type.compareTo("SENDING_AIRCRAFT")==0) {
       System.out.println("Sending aircraft data...");
       d2.getFlightList().sendingAircraft(d2, time,parameters);

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java
index c91db3bbd4ea375dcb90afedf76d3d0974f200bb..2f268cb414a4ff7dc2008aa3e53f0f4c39a511f2 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/MessageList.java
@@ -10,12 +10,13 @@ public class MessageList {
 
   public Message data() {
     Message m = (Message) messages.elementAt(0);
-    messages.removeElementAt(0);
     return m;
   }
     
   public Message next() {
-    return data();
+    Message m = (Message) messages.elementAt(0);
+    messages.removeElementAt(0);
+    return m;
   }
 
   public boolean hasNext() {

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java
index 5de6652bc9ce618b8b786a07d6718929ce1250ae..bec9ff85206e1c32e21eb05e037d1390d8ac8dcc 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/TrajectorySynthesizer.java
@@ -30,8 +30,7 @@ public class TrajectorySynthesizer {
   }
 
     public /*static*/ Trajectory updateTrajectory (D2 d2, double time, Flight flight) {
-       return null;
-       /*    System.out.println("Updating trajectory for "+flight.flightID);
+    System.out.println("Updating trajectory for "+flight.flightID);
     int i;
     setInitialParameters(flight);
     System.out.println("Starting position: "+currentPos);
@@ -62,7 +61,7 @@ public class TrajectorySynthesizer {
 
     flight.traject=traject;
     System.out.println("Finished updating trajectory ...");
-    return traject;*/
+    return traject;
   }
 
   private /*static*/ void setInitialParameters(Flight flight) {

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile
index 6892efc2e0b637206f7c77b469f5b9b028770eeb..bf80219efcc2c6f7638a3434a110cd16c908942b 100644 (file)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-small-for-testing/makefile
@@ -1,12 +1,18 @@
-MAIN_CLASS=D2 #smalltest
+MAIN_CLASS=D2
 
 PROGRAM=test
-SOURCE_FILES=D2.java #smalltest.java
+SOURCE_FILES=D2.java
 
 BUILDSCRIPT=~/research/Robust/src/buildscript
-BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) -justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions
+BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) 
 
-all: $(PROGRAM).bin
+#DBCALLFLAGS= -owndebugcaller main -owndebugcallee executeAll 
+DBCALLFLAGS= -owndebugcaller executeAll -owndebugcallee executeMessage -owndebugcallcount 1
+#DBCALLFLAGS= -owndebugcaller executeMessage -owndebugcallee amendFlightPlan
+
+ANALYZEFLAGS= -justanalyze $(DBCALLFLAGS) -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions
+
+all: $(PROGRAM)
 
 view: PNGs
        eog *.png &
@@ -16,9 +22,12 @@ PNGs: DOTs
 
 DOTs: $(PROGRAM).bin
 
-$(PROGRAM).bin: $(SOURCE_FILES)
+$(PROGRAM): $(SOURCE_FILES)
        $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM) $(SOURCE_FILES)
 
+analyze: $(SOURCE_FILES)
+       $(BUILDSCRIPT) $(BSFLAGS) $(ANALYZEFLAGS) -o $(PROGRAM) $(SOURCE_FILES)
+ 
 clean:
        rm -f  $(PROGRAM).bin
        rm -fr tmpbuilddirectory