---

State.java

package gov.nasa.arc.ase.ltl;

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

class State implements Comparable
{
  private int representativeId = -1;
  private LinkedList transitions;
  private BitSet accepting;
  private boolean safety_acceptance;

  public State()
  {
    transitions = new LinkedList();
    accepting = null;
    safety_acceptance = false;
  }  
  public State(int equivId)
  {
    transitions = new LinkedList();
    accepting = null;
    safety_acceptance = false;
    representativeId = equivId;
  }  
  public State(BitSet acc)
  {
    transitions = new LinkedList();
    accepting = acc;
    safety_acceptance = false;
  }  
  public State(BitSet acc, int equivId)
  {
    transitions = new LinkedList();
    accepting = acc;
    safety_acceptance = false;
    representativeId = equivId;
  }  
  public boolean accepts(int i)
  {
    return (! (accepting.get(i)));
    // because in my accepting array 0 corresponds to accepting
  }  
  public void add(Transition trans)
  {
    transitions.add(trans);

  }  
  public int compareTo(Object f)
  {
    if (this == f) return(0);
    else return(1);
  }  
  /*    public boolean isAccepting()
    {
    return accepting;
    }
   */

  public void FSPoutput()
  {
    ListIterator iter = transitions.listIterator(0);
    Transition nextTrans;
    boolean first_trans = true;

    while (iter.hasNext())
    {
      nextTrans = (Transition) iter.next();
      if (first_trans)
      {
    System.out.print("(");
    first_trans = false;
      }
      else
    System.out.print("|");
      nextTrans.FSPoutput();

    }
  }  
  public int get_representativeId()
  {
    return (representativeId);
  }  
  public boolean is_safe ()
  {
    return safety_acceptance;
  }  
  public void set_representativeId(int id)
  {
    representativeId = id;
  }  
  public void SMoutput(gov.nasa.arc.ase.util.graph.Node[] nodes, gov.nasa.arc.ase.util.graph.Node node) {
    ListIterator iter = transitions.listIterator(0);
    Transition nextTrans;
    boolean first_trans = true;

    while (iter.hasNext()) {
      nextTrans = (Transition)iter.next();
      nextTrans.SMoutput(nodes, node);
    }
  }  
  public void step (Hashtable ProgramState, TreeSet newStates, State[] automaton)
  {
    ListIterator iter = transitions.listIterator(0);
    Transition nextTrans;

    while (iter.hasNext())
    {
      nextTrans = (Transition) iter.next();
      if (nextTrans.enabled(ProgramState))
    newStates.add(automaton[nextTrans.goesTo()]);
    }
  }  
  public void update_acc(BitSet acc)
  {
    accepting = acc;
  }  
  public void update_acc(BitSet acc, int equivId)
  {
    accepting = acc;
    representativeId = equivId;
  }  
  public void update_safety_acc (boolean val)
  {
    safety_acceptance = val;
  }  
}

---