UTJML

edu.utep.cs.utjml.compiler.rt
Class JMLAutomata

java.lang.Object
  extended by edu.utep.cs.utjml.compiler.rt.JMLAutomata

public class JMLAutomata
extends Object

A class representing finite automata to check call sequence specifications.

Version:
$Revision: 1.4 $
Author:
Yoonsik Cheon and Asha Perumendla

Constructor Summary
JMLAutomata(String[] labels, int[][][] trans)
          Constructs a JMLAutomata object when the location of the call sequence is not known.
JMLAutomata(String type, String loc, String[] labels, int[][][] trans)
          Constructs a JMLAutomata object.
 
Method Summary
 void checkTransition(String label)
          Makes a given transition.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

JMLAutomata

public JMLAutomata(String type,
                   String loc,
                   String[] labels,
                   int[][][] trans)
Constructs a JMLAutomata object.

Parameters:
loc - adds locations of the call sequences to the HashSet
labels - contains the list of labels for the Automata
trans - is a three dimensional array which contains possible transitions

JMLAutomata

public JMLAutomata(String[] labels,
                   int[][][] trans)
Constructs a JMLAutomata object when the location of the call sequence is not known.

Parameters:
labels - contains the list of labels for the Automata
trans - a three dimensional array which contains possible transitions
Method Detail

checkTransition

public void checkTransition(String label)
Makes a given transition. If the transition is impossilbe, throw an JMLCallSequenceError.


UTJML

UTJML is Copyright (C) 2004-2006 by University of Texas at El Paso and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the JML project.