/******************************************************************************* * 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();    }  }  }