disjointness annotations to D2

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/Flight.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/Flight.java
index 4089257b8799f25b87c816d8cc7a5dcb0c794a80..25529f54fac292bc7fcfc2221a620b268fd12e28 100755 (executable)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-java/Flight.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/Flight.java
@@ -51,7 +51,7 @@ public class Flight /*implements Cloneable*/ {
   }
 
   public static Flight copyOf( D2 d2, Flight f) {
-    Flight fNew       = new Flight(d2, f.flightID);
+    Flight fNew       = disjoint flightCopy new Flight(d2, f.flightID);
     fNew.trialStatus  = f.trialStatus;
     fNew.aircraftType = f.aircraftType;
     fNew.track        = f.track;

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java
index f1a5c1e59444e8dff94fe67b26a6f060d6fbb2a3..4049d2741a5143e8c5d425211a9e30d32ebd10e6 100755 (executable)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/FlightList.java
@@ -21,7 +21,7 @@ public class FlightList {
   */
 
   public /*static*/ void addFlightPlan(int time, StringTokenizer st) { 
-    Flight newFlight=new Flight(d2, st.nextToken());
+    Flight newFlight=disjoint flightAdd new Flight(d2, st.nextToken());
     noFlights++;
     f.addElement(newFlight);
     FlightPlan fAux=new FlightPlan();

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/MessageList.java b/Robust/src/Benchmarks/mlp/directto/mlp-java/MessageList.java
index b5af4b372e9297fcf44cb8d7339a52b699f7e171..826f7814855e4d1d345b283f24dc2701ef6be409 100755 (executable)
--- a/Robust/src/Benchmarks/mlp/directto/mlp-java/MessageList.java
+++ b/Robust/src/Benchmarks/mlp/directto/mlp-java/MessageList.java
@@ -38,7 +38,7 @@ public class MessageList {
     StringTokenizer st=new StringTokenizer(line);
     int time=Integer.parseInt(st.nextToken());
     String type=st.nextToken();        
-    Message newMessage=new Message(d2,time,type,st);
+    Message newMessage=disjoint msgs new Message(d2,time,type,st);
     messages.addElement(newMessage);
     if (type.equals("DO_WORK"))
       return true;

diff --git a/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile b/Robust/src/Benchmarks/mlp/directto/mlp-java/makefile
index 168cf6cebf1c2f3e6ad1ab5d0864a084736608a7..d9679373eb2229e687baab3964cb5d3be76c2a2b 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=*.java
 
 BUILDSCRIPT=~/research/Robust/src/buildscript
-BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) #-justanalyze -ownership -ownallocdepth 1 -ownwritedots final -enable-assertions
+BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) -justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions
 
 all: $(PROGRAM).bin