---

Node.java

package gov.nasa.arc.ase.ltl;

// Written by Dimitra Giannakopoulou, 19 Jan 2001
import java.util.*;

class Node implements Comparable
{
  private int nodeId;
  private TreeSet incoming;
  private TreeSet toBeDone;
  private TreeSet old;
  private TreeSet next;
  private BitSet accepting; 
  private BitSet right_of_untils;
  private Node OtherTransitionSource;
  public static int accepting_conds = 0;
  private static boolean init_collapsed = false;
  private int equivalenceId;

  public Node () 
  {
    nodeId = Pool.assign();
    incoming = new TreeSet();
    toBeDone = new TreeSet();
    old = new TreeSet();
    next = new TreeSet();
    OtherTransitionSource = null;
    accepting = new BitSet(accepting_conds);
    right_of_untils = new BitSet(accepting_conds);
  }  
  public Node (TreeSet in, TreeSet newForm, TreeSet done, TreeSet nx, BitSet acc, BitSet rous)
  {
    nodeId = Pool.assign();
    incoming = new TreeSet(in);
    toBeDone = new TreeSet(newForm);
    old = new TreeSet(done);
    next = new TreeSet (nx);
    OtherTransitionSource = null;
    accepting = new BitSet(accepting_conds);
    accepting.or(acc);
    right_of_untils = new BitSet(accepting_conds);
    right_of_untils.or(rous);
  }  
  public boolean compare_accepting(Node nd) 
  {
    //if (nodeId == 0) 
    //  System.out.println("Has it been collapsed yet? : " + init_collapsed);
    if (nodeId == 0 && !init_collapsed) 
    {   
      // System.out.println("Potentially collapse " + nodeId + " with " + nd.nodeId);
      return true;
    }   
    return (accepting.equals(nd.accepting)); // compare their BitSets
  }  
  public int compareTo(Object f) 
  {
    if (this == f) return(0);
    else return(1);

  }  
  public static Node createInitial(Formula form) 
  {
    accepting_conds = form.processRightUntils(); // first mark right forms of untils;
    Formula.until_forms = new Formula[accepting_conds];
    Formula.untils.toArray(Formula.until_forms);

    Node init = new Node();
    init.nodeId = 0;
    if (form.getContent() != 't') 
      init.decompose_ands_for_next(form);

    return init;
  }  
  public void debug()
  {
    Iterator iterOld = old.iterator();
    Formula nextForm = null;

    //      System.out.println("debugging now");
    while (iterOld.hasNext()) 
    {
      nextForm = (Formula) iterOld.next();
      //            System.out.println("Content is " + nextForm.getContent());
    }
  }  
  public void decompose_ands_for_next (Formula form) 
  {
    if (form.getContent() == 'A')   
    {   
      decompose_ands_for_next(form.getSub1());
      decompose_ands_for_next(form.getSub2());
    }
    else if (is_redundant(next, null, form) == false)
      next.add(form);
  }  
  public Automaton expand (Automaton states) 
  {
    //      System.out.println("expand entered"); // debugging
    Node tempNode;
    if (toBeDone.isEmpty()) 
    {
      if (nodeId != 0) update_accepting();
      //            System.out.println("New is empty!");
      tempNode = states.alreadyThere(this);
      if (tempNode != null)
      { 
    //              System.out.println("Node " + nodeId + " collapsed with " + tempNode.nodeId);
    tempNode.modify(this);
    return states;
      }
      else 
      {
    Node NewN = new Node();
    NewN.incoming.add(this);
    NewN.toBeDone.addAll(next);

    /* // OLD CODE?
       if (!next.isEmpty()) 
       {
       Formula test = (Formula) next.first();
       }
     */ 

    states.add(this);
    return (NewN.expand(states));
      } 
    }
    else // toBeDone is not empty
    {
      Formula temp_form;
      Formula ita = (Formula) toBeDone.first();
      toBeDone.remove(ita);

      //System.out.println("\n\nExpanding " + ita + " for node " + nodeId);

      if (testForContradictions(ita) ) 
      {
    //System.out.println("Finished expand - contradiction");
    return states;
      }
      // no contradiction
      TreeSet set_checked_against = new TreeSet();
      set_checked_against.addAll(old);
      set_checked_against.addAll(toBeDone);


      if (is_redundant(set_checked_against, next, ita))         
    return expand(states);

      // not redundant either

      if (!ita.is_literal()) 
      {
    switch (ita.getContent()){

      case 'U':
      case 'W':
      case 'V': 
      case 'O':
        Node node2 = split(ita);
        return node2.expand(this.expand(states));
      case 'X':
        decompose_ands_for_next(ita.getSub1());
        if (ita.is_right_of_until())
          right_of_untils.set(ita.get_rightOfUntils_index());
        return expand(states);                                  
      case 'A':
        temp_form = ita.getSub1();
        if (! old.contains(temp_form))
          toBeDone.add(temp_form);
        temp_form = ita.getSub2();
        if (! old.contains(temp_form))
          toBeDone.add(temp_form);
        if (ita.is_right_of_until())
          right_of_untils.set(ita.get_rightOfUntils_index());
        return expand(states);
      default:
        System.out.println("default case of switch entered");
        return null;
    }
      }
      else // ita represents a literal
      {
    //              System.out.println("I am now working on literal " + ita.getContent()); // Debug
    // must do a test for contradictions first
    if (ita.getContent() != 't') old.add(ita);
    //              System.out.println("added to " + nodeId + " formula " + ita);
    if (ita.is_right_of_until())
      right_of_untils.set(ita.get_rightOfUntils_index());
    return(expand(states));
      }

    }

  }  
  public int get_equivalenceId ()
  {
    return equivalenceId;
  }  
  public static int getAcceptingConds () 
  {
    return accepting_conds;
  }  
  public TreeSet getField_next () 
  {
    return next;
  }  
  public TreeSet getField_old () 
  {
    return old;
  }  
  public int getId() 
  {
    return nodeId;
  }  
  public int getNodeId() 
  {
    return nodeId;
  }  
  private static boolean is_redundant(TreeSet main_set, TreeSet next_set, Formula ita) 
  {
    if (( ita.is_special_case_of_V(main_set)) || // my addition - correct??? 
    ((ita.is_synt_implied(main_set, next_set))
     &&
     (!(ita.getContent() == 'U') || (ita.getSub2().is_synt_implied(main_set, next_set)))))
    {           
      //System.out.println("Looks like formula was redundant");
      return true;
    }
    else
      return false;
  }  
  private boolean is_safety_acc_node() 
  {
    if (next.isEmpty()) return true;

    Iterator iterNext = next.iterator();
    Formula nextForm = null;

    // all formulas present must be of type V or W, otherwise false
    while (iterNext.hasNext()) 
    {
      nextForm = (Formula) iterNext.next();
      if (nextForm.getContent() != 'V' && nextForm.getContent() != 'W') 
    return false;
    }

    return true;
  }  
  public boolean isInitial() 
  {
    return nodeId == 0;
  }  
  private void modify(Node current) 
  {
    boolean match = false;
    Node Tail= this, Alternative = this;

    if (this.nodeId == 0 && !init_collapsed) 
    {
      accepting = current.accepting;
      init_collapsed = true;
    }


    while (Alternative != null)  
    {
      if (Alternative.old.equals(current.old)) 
      {
    Alternative.incoming.addAll(current.incoming);
    match = true;
      } 

      Tail = Alternative;
      Alternative = Alternative.OtherTransitionSource; 


    }


    if (!match) Tail.OtherTransitionSource = current;
  }  
  public void print() 
  {
    System.out.println("\n\nPrinting node " + nodeId);
    Iterator iterNext = next.iterator();
    Formula nextForm = null;

    // all formulas present must be of type V or W, otherwise false
    while (iterNext.hasNext()) 
    {
      nextForm = (Formula) iterNext.next();
      System.out.println("Formula: " + nextForm.toString());
    }


  }  
  public static void reset_static() 
  {
    accepting_conds = 0;
    init_collapsed = false;
  }  
  public void RTstructure(State[] RTautomaton) 
  {
    boolean safety = false;
    if (RTautomaton[nodeId] == null) 
      RTautomaton[nodeId] = new State(accepting, equivalenceId);
    else
      RTautomaton[nodeId].update_acc(accepting, equivalenceId);

    if (is_safety_acc_node())       
    {
      RTautomaton[nodeId].update_safety_acc(true);
      safety = true;
    }       

    Node Alternative = this;

    while (Alternative != null) 
    {
      Iterator iterIncom = Alternative.incoming.iterator();
      Node nextNode;

      while (iterIncom.hasNext()) 
      {
    nextNode = (Node) iterIncom.next();
    int stateId = nextNode.getId();
    if (RTautomaton[stateId] == null)
      RTautomaton[stateId] = new State();
    RTautomaton[stateId].add(new Transition(Alternative.old, equivalenceId, accepting, safety));
      } 

      Alternative = Alternative.OtherTransitionSource;
    }   
  }  
  public void set_equivalenceId (int value)
  {
    equivalenceId = value;
  }  
  private Node split (Formula form) 
  {
    //System.out.println("Split is entered");
    Formula temp_form;
    // first create Node 2
    Node Node2 = new Node ( this.incoming, this.toBeDone, this.old, 
    this.next, this.accepting, this.right_of_untils);



    temp_form = form.getSub2();
    if (! old.contains(temp_form)) //New2(n) not in old
      Node2.toBeDone.add(temp_form);
    if (form.getContent() == 'V')   // both subformulas are added to New2
    {   temp_form = form.getSub1();
      if (! old.contains(temp_form)) // subformula not in old
    Node2.toBeDone.add(temp_form);
    }   


    // then substitute current Node with Node 1
    temp_form = form.getSub1();
    if (! old.contains(temp_form))  //New1(n) not in old
      toBeDone.add(temp_form);
    temp_form = form.getNext();
    if (temp_form != null) decompose_ands_for_next(temp_form);  


    /* now check what needs to be stored and what accepting BitSets to update */
    if (form.getContent() == 'U') // this is an until formula
    {   
      //System.out.println("so what happened?");
      accepting.set(form.get_untils_index());
      Node2.accepting.set(form.get_untils_index());
    }
    if (form.is_right_of_until())
    {
      right_of_untils.set(form.get_rightOfUntils_index());  
      Node2.right_of_untils.set(form.get_rightOfUntils_index());    
    }
    /* following lines are probably unecessary because we never split literals!*/
    if (form.is_literal()) /* because we only store literals... */
    {
      old.add(form);
      System.out.println("added " + form); // never supposed to see that
      Node2.old.add(form);  
    }

    //System.out.println("Node split into itself and node : " + Node2.nodeId);
    //print();
    //Node2.print();

    return (Node2);
  }  
  private boolean testForContradictions(Formula ita) 
  {

    Formula Not_ita = ita.negate();
    if (Not_ita.is_synt_implied(old, next))
      return true;
    else
      return false; 
  }  
  public void update_accepting() 
  {
    accepting.andNot(right_of_untils);
    // just do now the bitwise or so that accepting gets updated
  }  
}

---