src/tests/gov/nasa/jpf/test/mc/data/TimeModelTest.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18 package gov.nasa.jpf.test.mc.data;
  19
  20 import gov.nasa.jpf.util.test.TestJPF;
  21 import gov.nasa.jpf.vm.Verify;
  22
  23 import org.junit.Test;
  24
  25 /**
  26  * regression test for TimeModel implementations
  27  */
  28 public class TimeModelTest extends TestJPF {
  29
  30   @Test
  31   public void testSystemTime(){
  32
  33     if (verifyNoPropertyViolation("+vm.time.class=.vm.SystemTime")){
  34       long t1 = System.currentTimeMillis();
  35       System.out.printf("t1 = %d\n", t1);
  36
  37       boolean b2 = Verify.getBoolean();
  38       long t2 = System.currentTimeMillis();
  39       System.out.printf("  t2 = %d\n", t2);
  40
  41       boolean b3 = Verify.getBoolean();
  42       long t3 = System.currentTimeMillis();
  43       System.out.printf("    t3 = %d\n", t3);
  44
  45       assertTrue((t3 >= t2) && (t2 >= t1));
  46     }
  47   }
  48
  49   @Test
  50   public void testPathTime(){
  51
  52     if (!isJPFRun()){
  53       Verify.resetCounter(0);
  54       Verify.resetCounter(1);
  55     }
  56
  57     if (verifyNoPropertyViolation("+vm.time.class=.vm.ConstInsnPathTime")){
  58       long t1 = System.currentTimeMillis();
  59       System.out.printf("t1 = %d\n", t1);
  60
  61       boolean b2 = Verify.getBoolean(true); // we do falseFirst
  62       long t2 = System.currentTimeMillis();
  63       System.out.printf("  t2 = %d\n", t2);
  64
  65       if (b2){ // has to be second time around
  66         assertTrue(t2 == Verify.getCounter(0));
  67       } else {
  68         Verify.setCounter(0,(int)t2);
  69       }
  70
  71
  72       boolean b3 = Verify.getBoolean(true);  // store the result so that we don't state match
  73       long t3 = System.currentTimeMillis();
  74       System.out.printf("    t3 = %d\n", t3);
  75
  76       if (b3){ // has to be second time around
  77         assertTrue(t3 == Verify.getCounter(1));
  78       } else {
  79         Verify.setCounter(1,(int)t3);
  80       }
  81
  82       assertTrue((t3 > t2) && (t2 > t1));
  83     }
  84
  85
  86   }
  87
  88
  89 }