src/main/gov/nasa/jpf/vm/BooleanChoiceGenerator.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.vm;
  19
  20 import gov.nasa.jpf.Config;
  21
  22 /**
  23  * a pretty simple ChoiceGenerator that returns a boolean
  24  * there is not much use in having a CG type interface (such as
  25  * IntChoiceGenerator) since there is hardly a need for a generic type hierarchy
  26  * of BooleanChoiceGenerator subtypes - what else can you do with true/false
  27  */
  28 public class BooleanChoiceGenerator extends ChoiceGeneratorBase<Boolean> {
  29
  30   // do we evaluate [false, true] or [true, false]
  31   protected boolean falseFirst = true;
  32
  33   protected int count = -1;
  34   protected boolean next;
  35
  36   public BooleanChoiceGenerator(Config conf, String id) {
  37     super(id);
  38
  39     falseFirst = conf.getBoolean("cg.boolean.false_first", true);
  40     next = falseFirst;
  41   }
  42
  43   public BooleanChoiceGenerator (String id) {
  44     super(id);
  45     next = falseFirst;
  46   }
  47
  48   public BooleanChoiceGenerator( String id, boolean falseFirst ){
  49     super(id);
  50
  51     this.falseFirst = falseFirst;
  52     next = falseFirst;
  53   }
  54
  55   @Override
  56   public boolean hasMoreChoices () {
  57     return !isDone && (count < 1);
  58   }
  59
  60   @Override
  61   public Boolean getNextChoice () {
  62     return next ? Boolean.TRUE : Boolean.FALSE;
  63   }
  64
  65   @Override
  66   public Class<Boolean> getChoiceType() {
  67     return Boolean.class;
  68   }
  69
  70   @Override
  71   public void advance () {
  72     if (count < 1) {
  73       count++;
  74       next = !next;
  75     }
  76   }
  77
  78   @Override
  79   public Boolean getChoice (int idx){
  80     if (idx == 0){
  81       return falseFirst ? Boolean.FALSE : Boolean.TRUE;
  82     } else if (idx == 1){
  83       return falseFirst ? Boolean.TRUE : Boolean.FALSE;
  84     } else {
  85       throw new IllegalArgumentException("choice index out of range: " + idx);
  86     }
  87   }
  88
  89   @Override
  90   public void reset () {
  91     count = -1;
  92     next = falseFirst;
  93
  94     isDone = false;
  95   }
  96
  97   @Override
  98   public int getTotalNumberOfChoices () {
  99     return 2;
 100   }
 101
 102   @Override
 103   public int getProcessedNumberOfChoices () {
 104     return (count+1);
 105   }
 106
 107   // that is pretty stupid, but for the sake of consistency we make it available
 108   Boolean[] getChoices(){
 109     Boolean[] vals = new Boolean[2];
 110     vals[0] = !falseFirst;
 111     vals[1] = falseFirst;
 112
 113     return vals;
 114   }
 115
 116   // not much use to support reordering, we just have two elements so reverse() will do
 117
 118   public boolean isFalseFirst(){
 119     return falseFirst;
 120   }
 121
 122   /**
 123    *  note this should only be called before the first advance since it resets
 124    *  the enumeration state
 125    */
 126   public void reverse(){
 127     falseFirst = !falseFirst;
 128     reset();
 129   }
 130
 131   @Override
 132   public String toString () {
 133     StringBuilder sb = new StringBuilder(getClass().getName());
 134     sb.append('[');
 135     sb.append("[id=\"");
 136     sb.append(id);
 137     sb.append('"');
 138
 139     sb.append(",isCascaded:");
 140     sb.append(isCascaded);
 141
 142     sb.append(",{");
 143
 144     if (count < 0){
 145       sb.append(!next);
 146       sb.append(',');
 147       sb.append(next);
 148     } else if (count == 0) {
 149       sb.append(MARKER);
 150       sb.append(next);
 151       sb.append(',');
 152       sb.append(!next);
 153     } else {
 154       sb.append(!next);
 155       sb.append(',');
 156       sb.append(MARKER);
 157       sb.append(next);
 158     }
 159     sb.append("}]");
 160     return sb.toString();
 161   }
 162
 163   @Override
 164   public BooleanChoiceGenerator randomize () {
 165     next = random.nextBoolean();
 166     return this;
 167   }
 168 }