src/main/gov/nasa/jpf/util/automaton/Automaton.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.util.automaton;
  19
  20 import java.io.PrintStream;
  21
  22
  23 /**
  24  * generic class for modeling automatons
  25  *
  26  * Since this is used in so many extensions from both model and native code,
  27  * it seems appropriate to add a basis implementation to util.
  28  *
  29  * To make it more amenable to modeling (e.g. for native peer implementation),
  30  * we avoid using standard Java containers at the expense of efficiency for
  31  * large numbers of states and transitions
  32  */
  33 public class Automaton <S extends State> {
  34
  35   static final int STATE_INC = 16;
  36   static final int INPUT_INC = 16;
  37
  38   protected String label;
  39
  40   protected int nStates;
  41   protected State[] states;
  42
  43   protected int nInputs;
  44   protected String[] alphabet;
  45
  46   protected int current;
  47
  48
  49   public Automaton (String label, int numberOfStates, int numberOfInputs){
  50     this.label = label;
  51     states = new State[numberOfStates];
  52     alphabet = new String[numberOfInputs];
  53   }
  54
  55   public Automaton (String label, int numberOfStates){
  56     this( label, numberOfStates, INPUT_INC);
  57   }
  58
  59   public Automaton(String label){
  60     this(label, STATE_INC, INPUT_INC);
  61   }
  62
  63   public void addState (State newState){
  64     if (nStates == states.length){
  65       State[] a = new State[nStates + STATE_INC];
  66       System.arraycopy(states, 0, a, 0, nStates);
  67       states = a;
  68     }
  69
  70     states[nStates] = newState;
  71     newState.setId(nStates);
  72     nStates++;
  73   }
  74
  75   public void addStates (State ... newStates){
  76     int n = nStates + newStates.length;
  77     if (n >= states.length){
  78       State[] a = new State[n];
  79       System.arraycopy(states, 0, a, 0, nStates);
  80       states = a;
  81     }
  82
  83     for (int i=0; i<newStates.length; i++){
  84       State s = newStates[i];
  85       states[nStates] = s;
  86       s.setId(nStates);
  87       nStates++;
  88     }
  89   }
  90
  91   public String getLabel(){
  92     return label;
  93   }
  94
  95   public int getNumberOfStates(){
  96     return nStates;
  97   }
  98
  99   public S getCurrentState(){
 100     return (S)states[current];
 101   }
 102
 103   public String[] computeAlphabet(){
 104     for (int i = 0; i < nStates; i++) {
 105       State s = states[i];
 106       int nTrans = s.getNumberOfTransitions();
 107
 108       nextTransition:
 109       for (int j = 0; j < nTrans; j++) {
 110         Transition t = s.getTransition(j);
 111         String label = t.getLabel();
 112
 113         for (int k = 0; k < nInputs; k++) {
 114           if (alphabet[k].equals(label)) {
 115             break nextTransition;
 116           }
 117         }
 118
 119         if (nInputs == alphabet.length) {
 120           String[] a = new String[nInputs + INPUT_INC];
 121           System.arraycopy(alphabet, 0, a, 0, nInputs);
 122           alphabet = a;
 123         }
 124
 125         alphabet[nInputs] = label;
 126         nInputs++;
 127       }
 128     }
 129
 130     return alphabet;
 131   }
 132
 133   public String[] getAlphabet(){
 134     if (nInputs == 0){
 135       return computeAlphabet();
 136     } else {
 137       return alphabet;
 138     }
 139   }
 140
 141   public void printOn (PrintStream ps){
 142     ps.printf("Automaton '%s'\n", label);
 143
 144     for (int i=0; i<nStates; i++){
 145       states[i].printOn(ps);
 146     }
 147   }
 148 }