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

java.lang.Object
  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.