tracetable.java

AStar算法

/*******************************************************************************
 * Copyright © 2008 Sandro Badame. All Rights Reserved.
 * 
 * This software and the accompanying materials is available under the 
 * Eclipse Public License 1.0 (EPL), which accompanies this distribution, and is
 * available at http://visualjpf.sourceforge.net/epl-v10.html
 ******************************************************************************/
package com.javapathfinder.vjp.verify.view;

import gov.nasa.jpf.jvm.Transition;

import java.util.ArrayList;

import org.eclipse.jface.resource.ImageDescriptor;
import org.eclipse.jface.resource.ImageRegistry;
import org.eclipse.jface.viewers.ILabelProviderListener;
import org.eclipse.jface.viewers.ITableLabelProvider;
import org.eclipse.jface.viewers.StructuredSelection;
import org.eclipse.jface.viewers.TableViewer;
import org.eclipse.jface.viewers.Viewer;
import org.eclipse.swt.SWT;
import org.eclipse.swt.graphics.Image;
import org.eclipse.swt.widgets.Composite;
import org.eclipse.swt.widgets.Display;
import org.eclipse.swt.widgets.TableColumn;

import com.javapathfinder.vjp.VJP;
/**
 * The table used to display information about the thread trace generated by 
 * JPF during verification.
 * @author Sandro Badame
 *
 */
public class TraceTable extends TableViewer {
  /*
   * For our imaging needs
   */
  private static ImageRegistry imageRegistry = new ImageRegistry();
  private static final String THREAD_IMAGE = "images/threadimage.gif";
  
  static{
    imageRegistry.put(THREAD_IMAGE, 
                      ImageDescriptor.createFromURL(VJP.getResourceURL(THREAD_IMAGE)));
  }
  
  /**
   * @return the image that represents a transition being executed in a 
   *         particular thread.
   */
  public static Image getThreadImage(){
    return imageRegistry.get(THREAD_IMAGE);
  }
  
  private ArrayList<TransitionInfo> transitions =  new ArrayList<TransitionInfo>();
  private TransitionInfo currentTransition = null;
  private int threadCount = 1;
   

  /**
   * @param parent
   * @param style
   */
  public TraceTable(Composite parent, int style) {   
    super(parent, SWT.H_SCROLL | SWT.V_SCROLL | SWT.MULTI | SWT.FULL_SELECTION);
    setContentProvider(new ArrayContentProvider());
    setLabelProvider(new LabelProvider());
    reset();
  }
  
  private void createColumns() {
    getTable().setHeaderVisible(true);
    int style = SWT.CENTER;
    
    TableColumn typeColumn = new TableColumn(getTable(), style);
    typeColumn.setText("Type");
    typeColumn.pack();
    typeColumn.setWidth(200);
    
    TableColumn choiceColumn = new TableColumn(getTable(), style);
    choiceColumn.setText("Choice");
    choiceColumn.pack();
    choiceColumn.setWidth(300);
    
    TableColumn attributeColumn = new TableColumn(getTable(), style);
    attributeColumn.setText("Attributes");
    attributeColumn.pack();
    attributeColumn.setWidth(300);
  }
  
  /**
   * Called when a new set of choices has been created
   * @param cgType the type of choices
   * @param totalChoices the total number of choices to be explored
   */
  public void newChoiceSet(String cgType, int totalChoices){
    currentTransition = new TransitionInfo();
    cgType = cgType.substring(cgType.lastIndexOf('.')+1);
    currentTransition.cgType = cgType;
    currentTransition.totalChoices = totalChoices;
    transitions.add(currentTransition);
  }
  
  /**
   * Called when a choice is being advanced
   * @param choice which choice was advanced
   */
  public void choiceAdvanced(int choice){
    currentTransition.processedChoices = choice;

  }
  
  /**
   * Called when the state has advanced 
   * @param t the transition is advancing
   * @param stateId the id of the state
   * @param isEndState whether this is an end state
   * @param isVisitedState whether this is a visited state
   */
  //TODO There HAS to be a cleaner way.
  public void stateAdvanced(Transition t, int stateId, boolean isEndState, boolean isVisitedState){
    currentTransition.transition = t;
    currentTransition.stateId = stateId;
    currentTransition.endState = isEndState;
    currentTransition.visited = isVisitedState;
    safeRefresh();
    safeSelectLast();

  }
  
  /**
   * Backtrack from the current state
   */
  public void stateBacktrack(){
    transitions.remove(currentTransition);
    safeRefresh();
    safeSelectLast();

  }
  
  /**
   * Safely refresh the trace table.
   *
   */
  public void safeRefresh(){
    Display.getDefault().syncExec(new Runnable(){
      public void run(){
        refresh();
      }
    });
  }
  
  private class LabelProvider implements ITableLabelProvider {
    
    public String getColumnText(Object element, int columnIndex) {
      TransitionInfo t = (TransitionInfo) element;
        while(t.getThreadIndex() >0 && t.getThreadIndex() >= threadCount)
          addThreadColumn();

      if (columnIndex == getTypeColumnIndex())
        return t.cgType;
      if (columnIndex == getChoiceColumnIndex())
        return t.processedChoices + "/" + t.totalChoices;
      if (columnIndex == getAttributeColumnIndex()){
        StringBuilder s = new StringBuilder("ID: ").append(t.stateId);
        if (!t.visited || t.endState){
          s.append(" [");
          if (!t.visited)
            s.append("NEW");
          if (t.endState){
            if (!t.visited) s.append(',');
            s.append("END");
          }
          s.append(']');
        }
        return s.toString();
      }
      return null;
    }
    
    public Image getColumnImage(Object element, int columnIndex) {
      if (!showThreadColumns() || ((TransitionInfo) element).getThreadIndex() != columnIndex) 
        return null;
      return getThreadImage();
    }
    
    
    public boolean isLabelProperty(Object element, String property) {return true;}
    public void addListener(ILabelProviderListener listener) {}
    public void dispose() {}
    public void removeListener(ILabelProviderListener listener) {}
  }
  
  private boolean showThreadColumns(){
    return threadCount>1;
  }
  
  private void addThreadColumn(){
    TableColumn c = new TableColumn(getTable(), SWT.NULL, threadCount);
    c.setText(String.valueOf(threadCount));
    c.setToolTipText("Thread: "+threadCount);
    c.setWidth(100);
    c.pack();
    addColumnProperty();
    threadCount++;
    refresh();
  }
  
 
  private void addColumnProperty(){
    String[] p = (String[]) getColumnProperties();
    int i = -1;
    while(!p[++i].equals("T"));
    String[] n = new String[p.length+1];
    System.arraycopy(p, 0, n, 0, i);
    n[i] = String.valueOf(i);
    n[i+1] = "T";
    n[i+2] = "C";
  }
  
  public int getTypeColumnIndex(){
    return threadCount;
  }
  
  public int getChoiceColumnIndex(){
    return getTypeColumnIndex()+1;
  }
  
  public int getAttributeColumnIndex(){
    return getChoiceColumnIndex()+1;
  }
  
  public void clearAll() {
    transitions.clear();
    safeReset();
  }
  
  private void safeReset(){
    Display.getDefault().syncExec(new Runnable(){
      public void run() {
        reset();
      }      
    });
  }
  
  /**
   * Clear this table of all threads and transition information.
   *
   */
  public void reset(){
    threadCount = 0;
    setColumnProperties(new String[]{"T", "C"});
    if (getTable().isDisposed())
      return;
    for(TableColumn c : getTable().getColumns())
      c.dispose();
    createColumns();
    setInput(transitions); 
  }
  
  /**
   * Refresh this table
   */
  public void refresh(){
    repackColumns();
    super.refresh();
  }
  
  /**
   * repack all of the columns in this table
   *
   */
  public void repackColumns(){
    for(TableColumn c : getTable().getColumns())
      c.pack();
  }
  
  /**
   * A thread safe way to select the last transition
   */
  public void safeSelectLast(){
    Display.getDefault().asyncExec(new Runnable(){
      public void run(){
        selectLast();
      }
    });
  }
  
  /**
   * Sets the selection to be last transition, then makes the transition
   * visible
   */
  public void selectLast(){
    setSelection(new StructuredSelection(currentTransition), true);
  }
  
  class ArrayContentProvider extends  org.eclipse.jface.viewers.ArrayContentProvider{
    public void inputChanged(Viewer viewer, Object oldInput, Object newInput) {
      repackColumns();    
    }
  }

  /**
   * 
   * @return information about the currently verified transition
   */
  public TransitionInfo getCurrentTransitionInfo() {
    return currentTransition;
  }
  
  class TransitionInfo {
    public Transition transition;
    public String cgType;
    
    int totalChoices;
    int processedChoices;
    
    boolean visited;
    boolean endState;
    int stateId;
    
    public int getTransitionNumber(){
      return transitions.indexOf(this);
    }
    
    public int getThreadIndex(){
      return transition.getThreadIndex();
    }
  }

  
}