new analysis found one shared location that is not overwritten in the eyetracking...

diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Counter.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Counter.java
new file mode 100644 (file)
index 0000000..a5a4ac3
--- /dev/null
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Counter.java
@@ -0,0 +1,15 @@
+public class Counter {
+
+  static int idx = 0;
+
+  @TRUST
+  static boolean inc() {
+    idx++;
+  }
+
+  @TRUST
+  static int idx() {
+    return idx;
+  }
+
+}

diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java b/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java
index c3749fd7f8f62b7b9cca30fd591297f545f358aa..7d5dab744eb586d6e73f614ef81b8810b041eb37 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/DeviationScanner.java
@@ -43,12 +43,8 @@ public class DeviationScanner {
   public static final int DOWN = 7;\r
   public static final int RIGHT_DOWN = 8;\r
 \r
-  @LOC("DEV")\r
-  private int size;\r
-\r
   public DeviationScanner() {\r
     eyePositions = new EyePosition[3];\r
-    size = 0;\r
   }\r
 \r
   @LATTICE("THIS<C,C<IN,THISLOC=THIS")\r
@@ -62,65 +58,57 @@ public class DeviationScanner {
 \r
     SSJAVA.append(eyePositions, eyePosition);\r
 \r
-    if (size < eyePositions.length) {\r
-      size++;\r
-    }else{\r
-      size= eyePositions.length;\r
-    }\r
-\r
-  }\r
-\r
-  @RETURNLOC("THIS,DeviationScanner.DEV")\r
-  public int getEyePositionsSize() {\r
-    return size;\r
   }\r
 \r
   // @LATTICE("OUT<DEV,DEV<C,C<THIS,THIS<IN,C*,DEV*,OUT*,THISLOC=THIS,RETURNLOC=OUT")\r
-  @LATTICE("THIS<IN,THISLOC=THIS")\r
+  @LATTICE("THIS<C,THIS<IN,THISLOC=THIS,C*")\r
   @RETURNLOC("THIS,DeviationScanner.DEV")\r
   public int scanForDeviation(@LOC("IN") Rectangle2D faceRect) {\r
     @LOC("THIS,DeviationScanner.DEV") int deviation = NONE;\r
-    if (getEyePositionsSize() >= 3) {\r
-      @LOC("THIS,DeviationScanner.DEV") double deviationX = 0;\r
-      @LOC("THIS,DeviationScanner.DEV") double deviationY = 0;\r
-\r
-      @LOC("THIS,DeviationScanner.DEV") int lastIdx = -1;\r
-      for (@LOC("THIS,DeviationScanner.DEV") int i = 0; i < 3; ++i) {\r
-        if (lastIdx != -1) {\r
-          deviationX += (eyePositions[i].getX() - eyePositions[lastIdx].getX());\r
-          deviationY += (eyePositions[i].getY() - eyePositions[lastIdx].getY());\r
-        }\r
-        lastIdx = i;\r
+\r
+    for (@LOC("C") int i = 0; i < 3; i++) {\r
+      if (eyePositions[i] == null) {\r
+        return deviation;\r
       }\r
+    }\r
+\r
+    @LOC("THIS,DeviationScanner.DEV") double deviationX = 0;\r
+    @LOC("THIS,DeviationScanner.DEV") double deviationY = 0;\r
 \r
-      @LOC("THIS,DeviationScanner.DEV") final double deviationPercentX = 0.04;\r
-      @LOC("THIS,DeviationScanner.DEV") final double deviationPercentY = 0.04;\r
+    @LOC("THIS,DeviationScanner.DEV") int lastIdx = -1;\r
+    for (@LOC("THIS,DeviationScanner.DEV") int i = 0; i < 3; ++i) {\r
+      if (lastIdx != -1) {\r
+        deviationX += (eyePositions[i].getX() - eyePositions[lastIdx].getX());\r
+        deviationY += (eyePositions[i].getY() - eyePositions[lastIdx].getY());\r
+      }\r
+      lastIdx = i;\r
+    }\r
 \r
-      deviationX /= faceRect.getWidth();\r
-      deviationY /= faceRect.getWidth();\r
+    @LOC("THIS,DeviationScanner.DEV") final double deviationPercentX = 0.04;\r
+    @LOC("THIS,DeviationScanner.DEV") final double deviationPercentY = 0.04;\r
 \r
-      @LOC("THIS,DeviationScanner.DEV") int deviationAbsoluteX = 0;\r
-      @LOC("THIS,DeviationScanner.DEV") int deviationAbsoluteY = 0;\r
-      if (deviationX > deviationPercentX)\r
-        deviationAbsoluteX = 1;\r
-      if (deviationX < -deviationPercentX)\r
-        deviationAbsoluteX = -1;\r
-      if (deviationY > deviationPercentY)\r
-        deviationAbsoluteY = 1;\r
-      if (deviationY < -deviationPercentY)\r
-        deviationAbsoluteY = -1;\r
+    deviationX /= faceRect.getWidth();\r
+    deviationY /= faceRect.getWidth();\r
 \r
-      deviation = getDirectionFor(deviationAbsoluteX, deviationAbsoluteY);\r
+    @LOC("THIS,DeviationScanner.DEV") int deviationAbsoluteX = 0;\r
+    @LOC("THIS,DeviationScanner.DEV") int deviationAbsoluteY = 0;\r
+    if (deviationX > deviationPercentX)\r
+      deviationAbsoluteX = 1;\r
+    if (deviationX < -deviationPercentX)\r
+      deviationAbsoluteX = -1;\r
+    if (deviationY > deviationPercentY)\r
+      deviationAbsoluteY = 1;\r
+    if (deviationY < -deviationPercentY)\r
+      deviationAbsoluteY = -1;\r
 \r
-      if (deviation != NONE) {\r
-        eyePositions = new EyePosition[3];\r
-        size = 0;\r
-      }\r
-      // System.out.println(String.format("%.2f%% | %.2f%% => %d and %d >>> %s",\r
-      // deviationX*100, deviationY*100, deviationAbsoluteX, deviationAbsoluteY,\r
-      // deviation.toString()));\r
+    deviation = getDirectionFor(deviationAbsoluteX, deviationAbsoluteY);\r
 \r
+    if (deviation != NONE) {\r
+      eyePositions = new EyePosition[3];\r
     }\r
+    // System.out.println(String.format("%.2f%% | %.2f%% => %d and %d >>> %s",\r
+    // deviationX*100, deviationY*100, deviationAbsoluteX, deviationAbsoluteY,\r
+    // deviation.toString()));\r
 \r
     return deviation;\r
   }\r
@@ -154,7 +142,6 @@ public class DeviationScanner {
   public void clear() {\r
     System.out.println("CLEAR");\r
     eyePositions = new EyePosition[3];\r
-    size = 0;\r
   }\r
 \r
   public String toStringDeviation(@LOC("IN") int dev) {\r

diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java b/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
index ea5f7e08a15210c7b41091d12fe27e3d89e3f845..d8e593c7b1b2bca1cb63d1753a94924afc631c64 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/LEA.java
@@ -94,9 +94,10 @@ public class LEA {
 
     @LOC("C") int i = 0;
 
-    SSJAVA: while (i < 37) {
-      @LOC("IMG") Image image = ImageReader.readImage("data/b" + i + ".bmp");
-      i++;
+    SSJAVA: while (Counter.idx() < 37) {
+      @LOC("IMG") Image image = ImageReader.readImage("data/b" + Counter.idx() + ".bmp");
+      Counter.inc();
+      // i++;
       if (image == null) {
         break;
       }
@@ -109,15 +110,15 @@ public class LEA {
 
   private void processImage(@LOC("IN") Image image) {
     @LOC("THIS,LEA.POS") FaceAndEyePosition positions = implementation.getEyePosition(image);
-//    if (positions.getEyePosition() != null) {
-      deviationScanner.addEyePosition(positions.getEyePosition());
-      @LOC("THIS,LEA.DEV,DeviationScanner.DEV") int deviation =
-          deviationScanner.scanForDeviation(positions.getFacePosition());// positions.getEyePosition().getDeviation(lastPositions.getEyePosition());
-      if (deviation != DeviationScanner.NONE) {
-        System.out.println("deviation=" + deviationScanner.toStringDeviation(deviation));
-        // notifyEyeMovementListenerEyeMoved(deviation);
-      }
-//    }
+    // if (positions.getEyePosition() != null) {
+    deviationScanner.addEyePosition(positions.getEyePosition());
+    @LOC("THIS,LEA.DEV,DeviationScanner.DEV") int deviation =
+        deviationScanner.scanForDeviation(positions.getFacePosition());// positions.getEyePosition().getDeviation(lastPositions.getEyePosition());
+    if (deviation != DeviationScanner.NONE) {
+      System.out.println("deviation=" + deviationScanner.toStringDeviation(deviation));
+      // notifyEyeMovementListenerEyeMoved(deviation);
+    }
+    // }
     lastPositions = positions;
   }