---

Automaton.java

package gov.nasa.arc.ase.ltl;

// Written by Dimitra Giannakopoulou, 19 Jan 2001
import java.util.*;
import gov.nasa.arc.ase.util.graph.*;

class Automaton
{

  private LinkNode head;
  private LinkNode tail;
  private Node[] equivalence_classes; // array of representatives of equivalent states

  public Automaton ()
  {
    head = tail = null;
    equivalence_classes = null;
  }  
  public void add (Node nd)
  {
    LinkNode newNode = new LinkNode(nd, null);
    if (head == null) // set is currently empty
      head = tail = newNode;
    else // put element at end of list
    {
      tail.LinkWith(newNode);
      tail = newNode;
    }
  }  
  public Node alreadyThere (Node nd)
  {
    // is already there if old and next fields are the same

    LinkNode nextNd = head;
    while (nextNd != null)
    {
      Node currState = nextNd.getNode();

      if (currState.getField_next().equals(nd.getField_next())
      &&  currState.compare_accepting(nd))
      {
    //System.out.println("Match found");
    return currState;
      }
      else
    nextNd = nextNd.getNext();

    }

    //System.out.println("No match found for node " + nd.getNodeId());
    return null;
  }  
  public static void FSPoutput(State[] automaton)
  {
    boolean comma = false;
    if (automaton == null)
    {
      System.out.println("\n\nRES = STOP.");
      return;
    }
    else
      System.out.println("\n\nRES = S0,");

    int size = Pool.assign();
    for (int i = 0; i < size; i++)
    {
      if ((automaton[i] != null) && (i == automaton[i].get_representativeId())) // a representative so print
      {
    if (comma) System.out.println("),");
    comma = true;
    System.out.print("S" + automaton[i].get_representativeId());
    System.out.print("=");
    automaton[i].FSPoutput();
      }
    }
    System.out.println(").\n");
  }  
  /*    public int get_representative_id(int automaton_index, State[] automaton)
    {
    return equivalence_classes[automaton[automaton_index].get_equivalence_class()].getNodeId();
    }
   */

  public int index_equivalence (Node nd)
  {
    // check if next field of node is already represented

    int index;

    for (index=0; index < Pool.assign(); index++)
    {
      if (equivalence_classes[index] == null)
      {
    //  System.out.println("Null object");
    break;
      }
      else if (equivalence_classes[index].getField_next().equals(nd.getField_next()))
      {
    //  System.out.println("Successful merge");
    return(equivalence_classes[index].getNodeId());
      }
    }

    if (index == Pool.assign())
      System.out.println("ERROR - size of equivalence classes array was incorrect");
    equivalence_classes[index] = nd;
    return (equivalence_classes[index].getNodeId());
  }  
  public static Graph SMoutput(State[] automaton)
  {
    Graph g = new Graph();
    g.setStringAttribute("type", "gba");
    g.setStringAttribute("ac", "edges");

    if (automaton == null)
      return g;

    int size = Pool.assign();
    gov.nasa.arc.ase.util.graph.Node[] nodes = new gov.nasa.arc.ase.util.graph.Node[size];
    for(int i = 0; i < size; i++) {
      if ((automaton[i] != null) &&
      (i == automaton[i].get_representativeId())) {
    nodes[i] = new gov.nasa.arc.ase.util.graph.Node(g);
    nodes[i].setStringAttribute("label",
        "S"+automaton[i].get_representativeId());
      }
    }

    for(int i = 0; i < size; i++)
      if ((automaton[i] != null) &&
      (i == automaton[i].get_representativeId()))
    automaton[i].SMoutput(nodes, nodes[i]);

    if(Node.accepting_conds == 0)
      g.setIntAttribute("nsets", 1);
    else
      g.setIntAttribute("nsets", Node.accepting_conds);

    return g;
  }  
  public State[] structForRuntAnalysis()
  {
    // now also fixes equivalence classes
    Pool.stop();
    int automatonSize = Pool.assign();
    State[] RTstruct = new State[automatonSize];
    equivalence_classes = new Node[automatonSize];

    if (head == null) return RTstruct;

    LinkNode nextNd = head;
    Node current;

    while (nextNd != null)
    {
      current = nextNd.getNode();
      current.set_equivalenceId(index_equivalence(current));
      nextNd.getNode().RTstructure(RTstruct);
      nextNd = nextNd.getNext();
    }

    return RTstruct;
  }  
}

---