Adding new examples and tests: Groovy and Java programs.
authorrtrimana <rtrimana@uci.edu>
Fri, 28 Jun 2019 23:33:03 +0000 (16:33 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 28 Jun 2019 23:33:03 +0000 (16:33 -0700)
17 files changed:
examples/BoundedBuffer.java [new file with mode: 0644]
examples/BoundedBuffer.jpf [new file with mode: 0644]
examples/ConcurrentCount.java [new file with mode: 0644]
examples/ConcurrentCount.jpf [new file with mode: 0644]
examples/DiningPhil.java [new file with mode: 0644]
examples/DiningPhil.jpf [new file with mode: 0644]
examples/NumericValueCheck.java [new file with mode: 0644]
examples/NumericValueCheck.jpf [new file with mode: 0644]
examples/Racer.groovy [deleted file]
examples/Rand.groovy
examples/Rand.jpf
examples/RandComplex.groovy [new file with mode: 0644]
examples/RandComplex.jpf [new file with mode: 0644]
examples/StopWatch.java [new file with mode: 0644]
examples/StopWatch.jpf [new file with mode: 0644]
examples/TestExample-coverage.jpf [new file with mode: 0644]
examples/TestExample.java [new file with mode: 0644]

diff --git a/examples/BoundedBuffer.java b/examples/BoundedBuffer.java
new file mode 100644 (file)
index 0000000..985fbc1
--- /dev/null
@@ -0,0 +1,143 @@
+/*
+ * 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.
+ */
+
+/**
+ * concurrency example with deadlock
+ * adapted from "Concurrency: State Models & Java Programs", Jeff Magee & Jeff Kramer
+ * 
+ * Note there need to be at least 2x buffer_size instances of either producers or
+ * consumers in order to produce the deadlock, which basically depends on 
+ * a notification choice between a consumer and a producer in a context where
+ * only threads of the notifier type are still runnable
+ * 
+ * This is a good benchmark for state management/matching in a small heap context.
+ * Higher numbers of buffer size and producers/consumers result in a nice
+ * state explosion
+ */
+public class BoundedBuffer {
+  
+  static int BUFFER_SIZE = 1;
+  static int N_PRODUCERS = 4;
+  static int N_CONSUMERS = 4;
+  
+  static Object DATA = "fortytwo";
+      
+  //--- the bounded buffer implementation
+  protected Object[] buf;
+  protected int in = 0;
+  protected int out= 0;
+  protected int count= 0;
+  protected int size;
+  
+  public BoundedBuffer(int size) {
+    this.size = size;
+    buf = new Object[size];
+  }
+
+  public synchronized void put(Object o) throws InterruptedException {
+    while (count == size) {
+      wait();
+    }
+    buf[in] = o;
+    //System.out.println("PUT from " + Thread.currentThread().getName());
+    ++count;
+    in = (in + 1) % size;
+    notify(); // if this is not a notifyAll() we might notify the wrong waiter
+  }
+
+  public synchronized Object get() throws InterruptedException {
+    while (count == 0) {
+      wait();
+    }
+    Object o = buf[out];
+    buf[out] = null;
+    //System.out.println("GET from " + Thread.currentThread().getName());
+    --count;
+    out = (out + 1) % size;
+    notify(); // if this is not a notifyAll() we might notify the wrong waiter
+    return (o);
+  }
+  
+  //--- the producer
+  static class Producer extends Thread {
+    static int nProducers = 1;
+    BoundedBuffer buf;
+
+    Producer(BoundedBuffer b) {
+      buf = b;
+      setName("P" + nProducers++);
+    }
+
+    @Override
+       public void run() {
+      try {
+        while(true) {
+          // to ease state matching, we don't put different objects in the buffer
+          buf.put(DATA);
+        }
+      } catch (InterruptedException e){}
+    }
+  }
+  
+  //--- the consumer
+  static class Consumer extends Thread {
+    static int nConsumers = 1;
+    BoundedBuffer buf;
+
+    Consumer(BoundedBuffer b) {
+      buf = b;
+      setName( "C" + nConsumers++);
+    }
+
+    @Override
+       public void run() {
+      try {
+        while(true) {
+            Object tmp = buf.get();
+        }
+      } catch(InterruptedException e ){}
+    }
+  }
+
+  //--- the test driver
+  public static void main(String [] args) {
+    readArguments( args);
+    //System.out.printf("running BoundedBuffer with buffer-size %d, %d producers and %d consumers\n", BUFFER_SIZE, N_PRODUCERS, N_CONSUMERS);
+
+    BoundedBuffer buf = new BoundedBuffer(BUFFER_SIZE);
+   
+    for (int i=0; i<N_PRODUCERS; i++) {
+      new Producer(buf).start();
+    }
+    for (int i=0; i<N_CONSUMERS; i++) {
+      new Consumer(buf).start();
+    }
+  }
+  
+  static void readArguments (String[] args){
+    if (args.length > 0){
+      BUFFER_SIZE = Integer.parseInt(args[0]);
+    }
+    if (args.length > 1){
+      N_PRODUCERS = Integer.parseInt(args[1]);      
+    }
+    if (args.length > 2){
+      N_CONSUMERS = Integer.parseInt(args[2]);      
+    }
+  }
+}
diff --git a/examples/BoundedBuffer.jpf b/examples/BoundedBuffer.jpf
new file mode 100644 (file)
index 0000000..bdd86dc
--- /dev/null
@@ -0,0 +1,4 @@
+target = BoundedBuffer
+
+# this should produce a deadlock
+target.args = 2,4,1
\ No newline at end of file
diff --git a/examples/ConcurrentCount.java b/examples/ConcurrentCount.java
new file mode 100644 (file)
index 0000000..cedfd4e
--- /dev/null
@@ -0,0 +1,59 @@
+import java.util.concurrent.atomic.AtomicBoolean;
+
+public class ConcurrentCount {
+       static final int COUNT = 30000;
+       volatile static int count = COUNT;
+       volatile static AtomicBoolean lock = new AtomicBoolean(false); 
+       static int a = 0;
+       static int b = 0;
+       
+       public static void main(String args[]) {
+               
+               new Thread() {
+                       
+                       @Override
+                       public void run() {
+                               while(count > 0) {
+                                       if (lock.get()) continue;
+                                       lock.set(true);
+                                       decreaseCount();
+                                       a++;
+                                       lock.set(false);
+                                       
+                                       
+                               }
+                       }
+               }.start();
+               
+        new Thread() {
+                       
+                       @Override
+                       public void run() {
+                               while(count > 0) {
+                                       if (lock.get()) continue;
+                                       lock.set(true);
+                                       decreaseCount();
+                                       b++;
+                                       lock.set(false);
+                                       
+                                       
+                               }
+                       }
+               }.start();
+               
+               while(count > 0);
+               //System.out.println("a = " + a);
+               //System.out.println("b = " + b);
+               //System.out.println("a + b = " + (a + b));
+               //System.out.println("count = " + count);
+
+               //Checks for concurrency error (which should be found when using model checking)
+               assert a + b == COUNT;
+       }
+       
+       private static synchronized void decreaseCount() {
+               count--;
+       }
+
+}
+
diff --git a/examples/ConcurrentCount.jpf b/examples/ConcurrentCount.jpf
new file mode 100644 (file)
index 0000000..331cb24
--- /dev/null
@@ -0,0 +1,3 @@
+listener=.listener.CGMonitor
+
+target = ConcurrentCount
diff --git a/examples/DiningPhil.java b/examples/DiningPhil.java
new file mode 100644 (file)
index 0000000..7295a5a
--- /dev/null
@@ -0,0 +1,64 @@
+/*
+ * 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.
+ */
+
+public class DiningPhil {
+
+  static class Fork {
+  }
+
+  static class Philosopher extends Thread {
+
+    Fork left;
+    Fork right;
+
+    public Philosopher(Fork left, Fork right) {
+      this.left = left;
+      this.right = right;
+      //start();
+    }
+
+    @Override
+       public void run() {
+      // think!
+      synchronized (left) {
+        synchronized (right) {
+          // eat!
+        }
+      }
+    }
+  }
+  
+  static int nPhilosophers = 6;
+
+  public static void main(String[] args) {
+    if (args.length > 0){
+      nPhilosophers = Integer.parseInt(args[0]);
+    }
+    
+    //Verify.beginAtomic();
+    Fork[] forks = new Fork[nPhilosophers];
+    for (int i = 0; i < nPhilosophers; i++) {
+      forks[i] = new Fork();
+    }
+    for (int i = 0; i < nPhilosophers; i++) {
+      Philosopher p = new Philosopher(forks[i], forks[(i + 1) % nPhilosophers]);
+      p.start();
+    }
+    //Verify.endAtomic();
+  }
+}
\ No newline at end of file
diff --git a/examples/DiningPhil.jpf b/examples/DiningPhil.jpf
new file mode 100644 (file)
index 0000000..901b818
--- /dev/null
@@ -0,0 +1,3 @@
+target = DiningPhil
+
+search.class = .search.heuristic.BFSHeuristic
diff --git a/examples/NumericValueCheck.java b/examples/NumericValueCheck.java
new file mode 100644 (file)
index 0000000..d99f092
--- /dev/null
@@ -0,0 +1,31 @@
+/*
+ * 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.
+ */
+
+/**
+ * example to catch numeric value rnge violations with the NumericValueChecker listener
+ */
+public class NumericValueCheck {
+  
+  public static void main (String[] args){
+    double someVariable;
+    
+    someVariable = 42;  // what else
+    
+    someVariable = 12345; // ..That's the number only an idiot would have on his luggage
+  }
+}
diff --git a/examples/NumericValueCheck.jpf b/examples/NumericValueCheck.jpf
new file mode 100644 (file)
index 0000000..6fa8a95
--- /dev/null
@@ -0,0 +1,10 @@
+target = NumericValueCheck
+
+listener = .listener.NumericValueChecker
+
+# NumericValueChecker configuration
+range.vars = 1
+range.1.var = NumericValueCheck.main(java.lang.String[]):someVariable
+range.1.min = 0
+range.1.max = 42
diff --git a/examples/Racer.groovy b/examples/Racer.groovy
deleted file mode 100644 (file)
index e8df2f8..0000000
+++ /dev/null
@@ -1,24 +0,0 @@
-class Racer implements Runnable {
-     int d = 42
-
-     public void run () {
-          doSomething(1001)
-          d = 0                              // (1)
-     }
-
-     static void main (String[] args){
-          Racer racer = new Racer()
-          Thread t = new Thread(racer)
-          t.start()
-
-          doSomething(1000)
-          int c = 420 / racer.d              // (2)
-          println c
-     }
-     
-     def doSomething (int n) {
-          try { 
-               Thread.sleep(n) 
-          } catch (InterruptedException ix) {}
-     }
-}
index 4d6ff32..11b5caa 100644 (file)
@@ -3,12 +3,12 @@ class Rand {
                println("Groovy model-checking")
                Random random = new Random(42);
        
-               int a = random.nextInt(2)
-               int b = random.nextInt(3)
+               int a = random.nextInt(10)
+               int b = random.nextInt(10)
                println("a=" + a)
                println("  b=" + b)
 
-               int c = a/(b+a -2)
+               int c = a/(b+a -5)
                println("    c=" + c)
        }
 }
index 57cd211..e81cc62 100644 (file)
@@ -1,3 +1,3 @@
 target = Rand
 cg.enumerate_random = true
-report.console.property_violation=error,trace
+#report.console.property_violation=error,trace
diff --git a/examples/RandComplex.groovy b/examples/RandComplex.groovy
new file mode 100644 (file)
index 0000000..fc2d647
--- /dev/null
@@ -0,0 +1,28 @@
+// This function runs when the SmartApp is installed
+def installed(a, b, c) {
+       println("a=" + a)
+       initialize(a, b, c)
+}
+
+// This function is where you initialize callbacks for event listeners
+def initialize(a, b, c) {
+       println("  b=" + b)
+       finalize(a, b, c)
+}
+
+def finalize(a, b, c) {
+       println("    c=" + c)
+       result(a, b, c)
+}
+
+def result(a, b, c) {
+       int d = a/(b+c-10)
+       println("       d=" + d)
+}
+
+Random random = new Random(42)
+int a = random.nextInt(10)
+int b = random.nextInt(10)
+int c = random.nextInt(10)
+installed(a,b,c)
+println "End of call!"
\ No newline at end of file
diff --git a/examples/RandComplex.jpf b/examples/RandComplex.jpf
new file mode 100644 (file)
index 0000000..49d418d
--- /dev/null
@@ -0,0 +1,3 @@
+target = RandComplex
+cg.enumerate_random = true
+#report.console.property_violation=error,trace
diff --git a/examples/StopWatch.java b/examples/StopWatch.java
new file mode 100644 (file)
index 0000000..8da5066
--- /dev/null
@@ -0,0 +1,35 @@
+/*
+ * 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.
+ */
+
+/**
+ * example to show how to explore off-nominal paths
+ */
+public class StopWatch {
+  
+  public static void main(String[] args){
+    long tStart = System.currentTimeMillis();
+    System.out.println("some lengthy computation..");
+    long tEnd = System.currentTimeMillis();
+    
+    if (tEnd - tStart > 1000){
+      throw new RuntimeException("it took too long..");
+    }
+    
+    System.out.println("all fine, finished in time");
+  }
+}
diff --git a/examples/StopWatch.jpf b/examples/StopWatch.jpf
new file mode 100644 (file)
index 0000000..2cabef9
--- /dev/null
@@ -0,0 +1,3 @@
+target = StopWatch
+
+listener = .listener.StopWatchFuzzer
diff --git a/examples/TestExample-coverage.jpf b/examples/TestExample-coverage.jpf
new file mode 100644 (file)
index 0000000..75d9ed4
--- /dev/null
@@ -0,0 +1,7 @@
+target = TestExample
+
+listener=.listener.CoverageAnalyzer
+
+coverage.include = T1,T2
+coverage.show_methods = true
+#coverage.show_bodies = true
\ No newline at end of file
diff --git a/examples/TestExample.java b/examples/TestExample.java
new file mode 100644 (file)
index 0000000..48aebdc
--- /dev/null
@@ -0,0 +1,74 @@
+/*
+ * 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.
+ */
+
+class T1 {
+  int d = 42;
+
+  public int func1(int a, int b) {
+    if (a > b) {
+      return 1;
+    } else if (a == b) {
+      return 0;
+    } else {
+      return -1;
+    }
+  }
+
+  public boolean func2(boolean cond) {
+    if (cond && (d > 40)) {
+      d--;
+    } else {
+      d++;
+    }
+    return cond;
+  }
+}
+
+class T2 {
+
+  public int computeSomething (int a, int b){
+    try {
+      return a / b;
+    } catch (ArithmeticException ax){
+      return -1; // pretty lame error handling
+    }
+  }
+
+  public void doSomething() {
+    System.out.println("something");
+  }
+}
+
+public class TestExample {
+
+  public static void main(String[] args) {
+    T1 t1 = new T1();
+
+    assert t1.func1(1, 0) > 0;
+    assert t1.func1(0, 1) < 0;
+
+    assert t1.func2(true) == true;
+    assert t1.func2(false) == false;
+
+
+    T2 t2 = new T2();
+
+    assert t2.computeSomething(42, 42) == 1.0;
+  }
+}
+