--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/tests/gov/nasa/jpf/test/mc/data/PerturbatorTest.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,257 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+
+package gov.nasa.jpf.test.mc.data;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import gov.nasa.jpf.vm.Verify;
+
+import org.junit.Test;
+
+/**
+ * regression test for Perturbator listener
+ */
+public class PerturbatorTest extends TestJPF {
+
+  int data = 42;
+
+  public static void main(String[] args) {
+    runTestsOfThisClass(args);
+  }
+
+  @Test
+  public void testIntFieldPerturbation() {
+
+    if (!isJPFRun()){
+      Verify.resetCounter(0);
+    }
+
+    if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
+                                  "+perturb.fields=data",
+                                  "+perturb.data.class=.perturb.IntOverUnder",
+                                  "+perturb.data.field=gov.nasa.jpf.test.mc.data.PerturbatorTest.data",
+                                  "+perturb.data.delta=1")){
+      System.out.println("instance field perturbation test");
+      int d = data;
+      System.out.print("d = ");
+      System.out.println(d);
+
+      Verify.incrementCounter(0);
+      switch (Verify.getCounter(0)){
+        case 1: assert d == 43; break;
+        case 2: assert d == 42; break;
+        case 3: assert d == 41; break;
+        default:
+          assert false : "wrong counter value: " + Verify.getCounter(0);
+      }
+
+    } else {
+      assert Verify.getCounter(0) == 3;
+    }
+  }
+
+  @Test
+  public void testFieldPerturbationLocation() {
+
+    if (!isJPFRun()){
+      Verify.resetCounter(0);
+    }
+
+    if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
+                                  "+perturb.fields=data",
+                                  "+perturb.data.class=.perturb.IntOverUnder",
+                                  "+perturb.data.field=gov.nasa.jpf.test.mc.data.PerturbatorTest.data",
+                                  "+perturb.data.location=PerturbatorTest.java:87",
+                                  "+perturb.data.delta=1")){
+      System.out.println("instance field location perturbation test");
+
+      int x = data; // this should not be perturbed
+      System.out.print("x = ");
+      System.out.println(x);
+
+      int d = data; // this should be
+      System.out.print("d = ");
+      System.out.println(d);
+
+      Verify.incrementCounter(0);
+
+    } else {
+      assert Verify.getCounter(0) == 3;
+    }
+  }
+
+  int foo (int i) {
+    return i;
+  }
+  
+  int bar (int i, boolean b) {
+  	return i-1;
+  }
+
+  int bar (int i){
+    return i-1;
+  }
+
+  @Test
+  public void testIntReturnPerturbation() {
+    if (!isJPFRun()){
+      Verify.resetCounter(0);
+      Verify.resetCounter(1);
+    }
+
+    if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
+                                  "+perturb.returns=foo,bar",
+
+                                  "+perturb.foo.class=.perturb.IntOverUnder",
+                                  "+perturb.foo.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.foo(int)",
+                                  "+perturb.foo.location=PerturbatorTest.java:136",
+                                  "+perturb.foo.delta=1",
+
+                                  "+perturb.bar.class=.perturb.IntOverUnder",
+                                  "+perturb.bar.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.bar(int,boolean)",
+                                  "+perturb.bar.delta=5")){
+      int x, y;
+
+      System.out.println("int return perturbation test");
+
+      x = foo(-1); // this should not be perturbed ('foo' has a location spec)
+      System.out.print("foo() = ");
+      System.out.println(x);
+
+      x = foo(42); // line 136 => this should be
+      System.out.print("foo() = ");
+      System.out.println(x);
+
+      Verify.incrementCounter(0);
+      switch (Verify.getCounter(0)){
+        // foo() preturbations
+        case 1: assert x == 43; break;
+        case 2: assert x == 42; break;
+        case 3: assert x == 41; break;
+        default:
+          assert false : "wrong counter 0 (foo() perturbation) value: " + Verify.getCounter(0);
+      }
+
+      if (x == 41){
+        y = bar(40, false); // this too (no location spec for 'bar')
+        System.out.print("bar() = ");
+        System.out.println(y);
+
+        Verify.incrementCounter(1);
+        switch (Verify.getCounter(1)){
+          // bar() perturbations
+          case 1: assert y == 44; break;
+          case 2: assert y == 39; break;
+          case 3: assert y == 34; break;
+          default:
+            assert false : "wrong counter 1 (bar() perturbation) value: " + Verify.getCounter(1);
+        }
+      }
+
+    } else {
+      assert Verify.getCounter(0) == 3;
+      assert Verify.getCounter(1) == 3;
+    }
+  }
+  
+  static void printParams(int i, boolean b) {
+  	System.out.println("(" + i + ", " + b + ")");
+  }
+  
+  static int zoo(int i, boolean b) {
+  	printParams(i, b);
+  	if (b)
+  		return -1 * i;
+  	else
+  		return i;
+  }
+  
+  void printParam(long i, double d) {
+  	System.out.println("(" + i + ", " + d + ")");
+  }
+  
+  double foobar(long i, double d) {
+  	printParam(i, d);
+  	long j = i;
+  	return d + (j % 10);
+  }
+  
+  @Test
+  public void testParamPerturbation() {
+
+    if (!isJPFRun()){
+      Verify.resetCounter(0);
+      Verify.resetCounter(1);
+    }
+
+    if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
+                                  "+perturb.params=foo,zoo",
+                                  "+perturb.foo.class=.perturb.GenericDataAbstractor",
+                                  "+perturb.foo.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.foobar(long,double)",
+                                  "+perturb.foo.location=PerturbatorTest.java:233",        // <<<<<<<<< update if file is changed!
+                                  "+perturb.zoo.class=.perturb.GenericDataAbstractor",
+                                  "+perturb.zoo.method=gov.nasa.jpf.test.mc.data.PerturbatorTest.zoo(int,boolean)"
+    )) {
+      System.out.println("parameters perturbation test");
+
+      int e = zoo(42, false);
+      System.out.print("zoo = ");
+      System.out.println(e);
+
+      Verify.incrementCounter(0);
+      switch (Verify.getCounter(0)){
+        case 1: assert e == 21; break;
+        case 2: assert e == -21; break;
+        case 3: assert e == 0; break;
+        case 4: assert e == 0; break;
+        case 5: assert e == -84; break;
+        case 6: assert e == 84; break;
+        default:
+          assert false : "wrong counter value: " + Verify.getCounter(0);
+      }
+    
+      if (e == 84) {
+      	double d = foobar(42, 0.0); // no perturbation
+      	System.out.print("foobar = ");
+      	System.out.println(d);
+
+      	d = foobar(42, 0.0); // <<<< yes perturbation, line 233
+      	System.out.print("foobar = ");
+      	System.out.println(d);
+
+      	Verify.incrementCounter(1);
+      	switch (Verify.getCounter(1)){
+      	case 1: assert Math.abs(d - 0.586) < 0.0001; break;
+      	case 2: assert d == 2; break;
+      	case 3: assert d == 5.141; break;
+      	case 4: assert d == -1.414; break;
+      	case 5: assert d == 0; break;
+      	case 6: assert d == 3.141; break;
+      	case 7: assert d == -1.414; break;
+      	case 8: assert d == 0; break;
+      	case 9: assert d == 3.141; break;
+      	default:
+      		assert false : "wrong counter value: " + Verify.getCounter(1);
+      	}
+      }
+    } else {
+      assert Verify.getCounter(0) == 6;
+      assert Verify.getCounter(1) == 9;
+    }
+  }
+}