Design of JPF Visual

#Design of jpf-visual

This is the introduction of the design of the tool. Here is a brief overview of the classes of jpf-visual.

##Starting point ErrorTracePrinter is the publisher for which the main purpose is to get the error path from JPF. The error path of the type gov.nasa.jpf.vm.Path can be obtained by calling the method getPath(). For details about the JPF report API, we refer to the JPF Report API.

##The Error Trace Tab TraceVisualPanel obtains the error path by calling the method getPath() of the publisher ErrorTracePrinter. It creates a new tab on the rightmost side of the JPF shell. The method postCommand is the key, which processes the data and draws all the panels. It is called after the "Verify" button is clicked. If there is no error path (path == null), a dialogue box pops up to notify the user that there is no error found by JPF. Otherwise, there is an error with the application under test and an error path is generated, TraceVisualPanel will pass the path to TraceData to analyze it. It adds the ErrorTableAndMapPane which draws the main/central panel and the world map/right panel of the new tab. It also draws the navigation/left panel which have the buttons, the checkboxes, and the dropdown list. For a picture of the new tab and the description of the three panels (navigation panel, main panel and world map), see jpf-visual wiki home.

###Data Processing TraceData processes the error path and stores the data. It involves two passes of the path (possibly a third pass if there are synchronized method, see the method processTextLineForSynchronizedMethods()).

####First Pass The first pass simply groups the transitions by the thread ids.

####Second Pass The second pass is more complicated. It stores the texts which are shown in the main/central panel. For each transition in a group, it processes each step of that transition and adds the corresponding txtSrc, which could be source code without comments or the information of no sources, to a txtLinelist. lineTable stores the txtLinelists for each group.

In each step, it also analyzes the instructions. The method loadSynchronizedMethod stores all the method names which are synchronized methods. The method loadWaitNotify stores the position (group number and line number in txtLinelist) of the source code for which the instruction is a wait/notify instruction. The method loadLockUnlock stores the position of the source code for which the instruction is lock/unlock instruction. The methods loadFields and loadMethods stores the field names and method names for each class.

####The two helping classes TextLine represents a line of the source code of the application under test. TextLineList represents a list of TextLine.

###Main/Central Panel & World Map/Right Panel ErrorTableAndMapPane draws a split pane, with the main/central panel on the left and the world map/right panel on the right.

ContentPane is the main/central panel, it uses the library mxgraph to draw the table.

MenuPane is the menu bar of the main/central panel.

SummaryCell is used in ContentPane, which helps to draw the summary view of the trace.

LocationInGraph records the location of the element in the main/central, it is useful to locate the elements which are required to be modified (highlight, no highlight, invisible).