2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.test.mc.data;
21 import gov.nasa.jpf.util.test.TestJPF;
22 import gov.nasa.jpf.vm.Verify;
24 import java.util.Random;
26 import org.junit.Test;
29 * test of gov.nasa.jpf.vm.Verify nondeterministic data initailization
31 public class RandomTest extends TestJPF {
32 private void run (int n){
33 int i = Verify.getInt(0,n); // we should backtrack 0..n times to this location
34 Verify.incrementCounter(0); // counter '0' should have value (n+1) after JPF is done
35 System.out.println(i);
38 @Test public void testRandom () {
40 Verify.resetCounter(0);
42 if (verifyNoPropertyViolation()){
46 if (Verify.getCounter(0) != 4){
47 fail("wrong number of paths");
52 @Test public void testRandomBFS () {
54 Verify.resetCounter(0);
56 if (verifyNoPropertyViolation("+search.class=gov.nasa.jpf.search.heuristic.BFSHeuristic")){
60 if (Verify.getCounter(0) != 4){
61 fail("wrong number of paths");
68 @Test public void testJavaUtilRandom () {
70 if (verifyUnhandledException("java.lang.ArithmeticException", "+cg.enumerate_random=true")) {
71 Random random = new Random(42); // (1)
73 int a = random.nextInt(4); // (2)
74 System.out.print("a=");
75 System.out.println(a);
77 //... lots of code here
79 int b = random.nextInt(3); // (3)
80 System.out.print("a=");
82 System.out.print(",b=");
83 System.out.println(b);
86 int c = a / (b + a - 2); // (4)
87 System.out.print("a=");
89 System.out.print(",b=");
91 System.out.print(",c=");
92 System.out.println(c);