Package org.svvrl.goal.core.aut.fsa

Class FSA

java.lang.Object
org.svvrl.goal.core.AbstractEditable
org.svvrl.goal.core.aut.Automaton
org.svvrl.goal.core.aut.fsa.FSA
All Implemented Interfaces:
java.beans.PropertyChangeListener, java.io.Serializable, java.lang.Cloneable, java.util.EventListener, Editable
Direct Known Subclasses:
ConfigurationAutomaton, ProfileAutomaton
public class FSA
extends Automaton
An FSA is a finite state automaton, including nondeterministic classic finite word automaton (NFW), nondeterministic Büchi word automaton (NBW), nondeterministic co-Büchi word automaton (NCW), nondeterministic generalized Büchi word automaton (NGBW), nondeterministic Muller word automaton (NMW), nondeterministic Rabin word automaton (NRW), nondeterministic Streett word automaton (NSW), and nondeterministic parity word automaton (NPW).
Author:
Ming-Hsien Tsai
See Also:
Serialized Form

  • Constructor Details

    • FSA

      public FSA​(AlphabetType atype, Position lpos)
      Constructor with the alphabet type and the label position.
      Parameters:
      atype - the alphabet type
      lpos - the label position

  • Method Details

    • addState

      public boolean addState​(State s)
      Description copied from class: Automaton
      Inserts a state created outside to this automaton. The state will not be inserted if there is another existing state with the same ID.
      Overrides:
      addState in class Automaton
      Parameters:
      s - the state to be inserted
      Returns:
      true if the state is not already contained in this automaton

    • newState

      public FSAState newState​(int id)
      Description copied from class: Automaton
      Creates a new state with an ID. Different automata types can override this function to create state objects from different classes.
      Specified by:
      newState in class Automaton
      Parameters:
      id - the unique ID of the state
      Returns:
      a new state with that ID

    • createState

      public FSAState createState()
      Description copied from class: Automaton
      Creates a new state of the automaton. The state will be placed at a random location. The created state is guaranteed to be in this automaton.
      Overrides:
      createState in class Automaton
      Returns:
      a new state of the automaton

    • createState

      public FSAState createState​(java.awt.Point p)
      Description copied from class: Automaton
      Creates a new state of the automaton at a specified location. The created state is guaranteed to be in this automaton.
      Overrides:
      createState in class Automaton
      Parameters:
      p - the position of the state
      Returns:
      a new state of the automaton

    • newTransition

      public FSATransition newTransition​(int id, State from, State to)
      Description copied from class: Automaton
      Creates a new instance of a transition.
      Specified by:
      newTransition in class Automaton
      Parameters:
      id - the unique transition ID
      from - the source state of the transition
      to - the destination state of the transition
      Returns:
      a new transition with ID id from from to to

    • createTransition

      public FSATransition createTransition​(State from, State to, java.lang.String label)
      Description copied from class: Automaton
      Creates a transition to the automaton. The returned transition is guaranteed to be in this automaton.
      Overrides:
      createTransition in class Automaton
      Parameters:
      from - the source state of the transition
      to - the destination state of the transition
      label - the label on the transition
      Returns:
      a new transition from from to to with label symbol if there is no such transition, the existing transition if this automaton has a transition from from to to with the label symbol, null if from is null, to is null, or the symbol is not valid

    • clone

      public FSA clone()
      Overrides:
      clone in class Automaton

    • newInstance

      protected Automaton newInstance()
      Description copied from class: Automaton
      Creates a new automaton that has the same type of this automaton. Note that this methods should only create an instance.
      Specified by:
      newInstance in class Automaton
      Returns:
      a new automaton that has the same type of this automaton

    • getRunsForInput

      public java.util.List<StateRun> getRunsForInput​(InputSequence input)
      Returns all possible runs of this automaton on a specified (unexpanded) input sequence starting from some initial state. Note that each run will start with an initial state.
      Parameters:
      input - an unexpanded input sequence
      Returns:
      all possible runs of this automaton on input

    • getRunsForInput

      public java.util.List<StateRun> getRunsForInput​(State start, InputSequence input)
      Returns all possible traces of this automaton starting from a specified state on a specified (unexpanded) input sequence. Note that each trace will start with the specified state. If the input sequence is empty, this method will return a state list containing only the starting state.
      Parameters:
      start - a starting state
      input - an unexpanded input sequence
      Returns:
      all possible traces of this automaton starting from start on input

    • getInputForPath

      public InputSequence getInputForPath​(StateRun run)
      Returns an input sequence that has a specified run of this automaton, null if there is no input sequence that has such a run.
      Parameters:
      run - a state run
      Returns:
      an input sequence that has the run path of this automaton, null if there is no input sequence that has such a run