src/tests/gov/nasa/jpf/vm/SystemStateTest.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
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.util.test.TestJPF;
  22 import gov.nasa.jpf.vm.BooleanChoiceGenerator;
  23 import gov.nasa.jpf.vm.ChoiceGenerator;
  24 import gov.nasa.jpf.vm.SystemState;
  25 import gov.nasa.jpf.vm.choice.DoubleChoiceFromList;
  26 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  27
  28 import org.junit.Test;
  29
  30
  31 /**
  32  * unit test driver for SystemState functions
  33  */
  34 public class SystemStateTest extends TestJPF {
  35
  36   static class MyJVM extends SingleProcessVM {
  37
  38     @Override
  39         protected void notifyChoiceGeneratorSet (ChoiceGenerator<?>cg) {
  40       System.out.println("notifyChoiceGeneratorSet: " + cg);
  41     }
  42     @Override
  43         protected void notifyChoiceGeneratorAdvanced (ChoiceGenerator<?>cg) {
  44       System.out.println("notifyChoiceGeneratorAdvanced: " + cg);
  45     }
  46     @Override
  47         protected void notifyChoiceGeneratorProcessed (ChoiceGenerator<?>cg) {
  48       System.out.println("notifyChoiceGeneratorProcessed: " + cg);
  49     }
  50   }
  51
  52   static class MySystemState extends SystemState {
  53   }
  54
  55
  56   @Test
  57   public void testCascadedCGops() {
  58
  59     MyJVM vm = new MyJVM();
  60     MySystemState ss = new MySystemState();
  61
  62     IntChoiceFromSet       cg0 = new IntChoiceFromSet( "cg0", -100, -200); // not cascaded
  63     BooleanChoiceGenerator cg1 = new BooleanChoiceGenerator("cg1"); // false,true
  64     IntChoiceFromSet       cg2 = new IntChoiceFromSet( "cg2", 1, 2);
  65     DoubleChoiceFromList    cg3 = new DoubleChoiceFromList( "cg3", 42.1, 42.2);
  66
  67     cg2.isCascaded = true;
  68     cg1.isCascaded = true;
  69
  70     cg3.prev = cg2;
  71     cg2.prev = cg1;
  72     cg1.prev = cg0;
  73     ss.curCg = cg3;
  74
  75     cg0.advance();
  76
  77     //--- test initial advance
  78     System.out.println("--- testing advanceCurCg()");
  79     ss.advanceCurCg(vm);
  80
  81     assert cg0.getNextChoice() == -100;
  82     assert cg1.getNextChoice() == false;
  83     assert cg2.getNextChoice() == 1;
  84     assert cg3.getNextChoice() == 42.1;
  85
  86
  87     //--- test advanceCascadedParent
  88     System.out.println("--- testing advanceCascadedParent()");
  89     cg2.advance(2);
  90     cg3.advance(2);
  91
  92     assert !cg2.hasMoreChoices();
  93     assert !cg3.hasMoreChoices();
  94
  95     System.out.println(cg1);
  96     System.out.println(cg2);
  97     System.out.println(cg3);
  98
  99     ss.advanceCascadedParent(vm,cg3);
 100
 101     assert cg0.getNextChoice() == -100;
 102     assert cg1.getNextChoice() == true;
 103     assert cg2.getNextChoice() == 1;
 104     assert cg3.getNextChoice() == 42.1;
 105   }
 106
 107   @Test
 108   public void testCascadedCGadvance() {
 109
 110     MyJVM vm = new MyJVM();
 111     MySystemState ss = new MySystemState();
 112
 113     BooleanChoiceGenerator cg1 = new BooleanChoiceGenerator("cg1"); // false,true
 114     IntChoiceFromSet       cg2 = new IntChoiceFromSet( "cg2", 1, 2);
 115     DoubleChoiceFromList    cg3 = new DoubleChoiceFromList( "cg3", 42.1, 42.2);
 116
 117     cg2.isCascaded = true;
 118     cg1.isCascaded = true;
 119
 120     cg3.prev = cg2;
 121     cg2.prev = cg1;
 122     ss.curCg = cg3;
 123
 124     int n = 0;
 125     while (ss.advanceCurCg(vm)){
 126       System.out.println("--");
 127       n++;
 128     }
 129
 130     assert n == 8;
 131   }
 132 }