---

Transition.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 Transition
{
  private TreeSet propositions;
  private int pointsTo;
  private BitSet accepting;
  private boolean safe_accepting;


  public Transition (TreeSet prop, int nd_id, BitSet acc, boolean safety)
  {
    propositions = prop;
    pointsTo = nd_id;
    accepting = new BitSet(Node.getAcceptingConds());
    accepting.or(acc);
    safe_accepting = safety;
  }  
  public boolean enabled (Hashtable ProgramState)
  {
    Iterator mustHold = propositions.iterator();
    Formula form = null;
    char c;
    Boolean value;

    while (mustHold.hasNext())
    {
      form = (Formula) mustHold.next();
      switch (c = form.getContent()) {
    case 'N':
      value = (Boolean) ProgramState.get(form.getSub1().getName());
      if (value== null)
      {
        //                  System.out.println("Proposition not defined in program state");
        return false;
      }
      else
        if (value.booleanValue()) return false;
      break;
    case 't':
      break;
    case 'p':
      value = (Boolean) ProgramState.get(form.getName());
      if (value== null)
      {
        //                  System.out.println("Proposition not defined in program state");
        return false;
      }
      else
        if (!value.booleanValue()) return false;
      break;
      }
    }
    return true;
  }  
  public void FSPoutput()
  {
    if (propositions.isEmpty())
      System.out.print("TRUE{");
    else
    {
      // first print the propositions involved
      Iterator it = propositions.iterator();
      Formula nextForm = null;
      StringBuffer act = new StringBuffer();
      char cont; // stores content of formula
      boolean need_AND = false; // connect with AND multiple propositions

      while (it.hasNext())
      {
    nextForm = (Formula) it.next();
    //          if (nextForm.is_literal()) // only literals represent actions
    {

      cont = nextForm.getContent();
      if (need_AND)
        act.append("_AND_");
      need_AND = true;
      switch (cont)
      {
        case 'N':   act.append('N');
            act.append(nextForm.getSub1().getName());
            break;
        case 't' :  act.append("TRUE");
            break;
        default:    act.append(nextForm.getName());
            break;
      }
    }
      }
      System.out.print(act + "{");
    }
    if (Node.accepting_conds == 0)
    {
        if (safe_accepting == true)
        {
            System.out.print("0");
        }
    }
    else
    {
      for (int i=0; i<Node.accepting_conds; i++)
            if (!accepting.get(i))
                System.out.print(i);
    }
    // and then the rest - easy
    System.out.print("} -> S" + pointsTo + " ");
  }  
  public int goesTo ()
  {
    return pointsTo;
  }  
  public void SMoutput(gov.nasa.arc.ase.util.graph.Node[] nodes, gov.nasa.arc.ase.util.graph.Node node)
  {
    String guard = "-";
    String action = "-";

    if (!propositions.isEmpty()) {
      Iterator it = propositions.iterator();
      Formula nextForm = null;
      StringBuffer sb = new StringBuffer();
      char cont; // stores content of formula
      boolean need_AND = false; // connect with AND multiple propositions

      while (it.hasNext())
      {
    nextForm = (Formula) it.next();
    {
      cont = nextForm.getContent();
      if (need_AND)
        sb.append("&");
      need_AND = true;
      switch (cont)
      {
        case 'N':   sb.append('!');
            sb.append(nextForm.getSub1().getName());
            break;
        case 't' :  sb.append("true");
            break;
        default:    sb.append(nextForm.getName());
            break;
      }
    }
      }
      guard = sb.toString();
    }

    Edge e = new Edge(node, nodes[pointsTo], guard, action);

    if (Node.accepting_conds == 0)
    { 
        if (safe_accepting == true)
            e.setBooleanAttribute("acc0", true);
    }  
    else
      for(int i = 0; i < Node.accepting_conds; i++)
        if(!accepting.get(i))
            e.setBooleanAttribute("acc"+i, true);
  }  
}

---