src/main/gov/nasa/jpf/vm/choice/BreakGenerator.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.choice;
  19
  20 import gov.nasa.jpf.vm.ChoiceGenerator;
  21 import gov.nasa.jpf.vm.ChoiceGeneratorBase;
  22 import gov.nasa.jpf.vm.ThreadChoiceGenerator;
  23 import gov.nasa.jpf.vm.ThreadInfo;
  24
  25 import java.io.PrintWriter;
  26
  27 /**
  28  * a pseudo CG that is used to break transitions. It can be used to break and
  29  * just reschedule the current thread, or to indicate an end state
  30  * (e.g. for System.exit())
  31  */
  32 public class BreakGenerator extends ChoiceGeneratorBase<ThreadInfo> implements ThreadChoiceGenerator {
  33
  34   protected ThreadInfo ti;
  35   protected int state = -1;
  36   protected boolean isTerminator;
  37
  38   public BreakGenerator (String id, ThreadInfo ti, boolean isTerminator) {
  39     super(id);
  40
  41     this.ti = ti;
  42     this.isTerminator = isTerminator;
  43   }
  44
  45   @Override
  46   public ThreadInfo getNextChoice () {
  47     assert !isTerminator : "illegal operation on terminal BreakGenerator";
  48     return (state == 0) ? ti : null;
  49   }
  50
  51   @Override
  52   public ThreadInfo getChoice (int idx){
  53     if (idx == 0){
  54       return ti;
  55     } else {
  56       throw new IllegalArgumentException("choice index out of range: " + idx);
  57     }
  58   }
  59
  60   @Override
  61   public void printOn (PrintWriter pw) {
  62     pw.println("BreakGenerator {" + ti.getName() + "}");
  63   }
  64
  65   @Override
  66   public void advance () {
  67     assert !isTerminator : "illegal operation on terminal BreakGenerator";
  68     state++;
  69   }
  70
  71   @Override
  72   public int getProcessedNumberOfChoices () {
  73     return (state >= 0) ? 1 : 0;
  74   }
  75
  76   @Override
  77   public int getTotalNumberOfChoices () {
  78     return 1;
  79   }
  80
  81   @Override
  82   public boolean hasMoreChoices () {
  83     if (isTerminator){
  84       return false;
  85     }
  86
  87     return (state < 0);
  88   }
  89
  90   @Override
  91   public void reset () {
  92     state = -1;
  93     isDone = false;
  94   }
  95
  96   @Override
  97   public boolean contains (ThreadInfo ti){
  98     return this.ti == ti;
  99   }
 100
 101   @Override
 102   public Class<ThreadInfo> getChoiceType() {
 103     return ThreadInfo.class;
 104   }
 105
 106   @Override
 107   public ChoiceGenerator<ThreadInfo> randomize() {
 108     return this;
 109   }
 110
 111   @Override
 112   public boolean isSchedulingPoint(){
 113     return true; // that's the whole point of having a BreakGenerator
 114   }
 115
 116 }