Menu featuresUser ManualOverviewMain panel

Main panel

Open Pda as you would any application on your machine. During loading, you will be asked if you wish to select the folder in which your workspace is held. Browse your own file system should you need to. You can also set a flag to avoid that dialog each time.

Pda will then ask if you want to start Specware on your machine. The result of your choice (and whether you have Specware installed, should you click OK, shows in the colored (red/green) icon at the bottom of the Pda's main panel.

Pda remembers where you were when you last saved and closed the application. The following figure is what you would see if you had the 6_1_1 protocol open for development. (6_1_1 is a name chosen for convenient reference into the ClarkJacob97 listing of protocols.)

The main Pda panel contains four primary components:

Pda toolbar The Pda toolbar is divided into two main groups, each with several components. Where a component has an icon to illustrate the underlying functionality, there is also a cursor-activated descriptor providing a text description. To expose this, simply hold the cursor over the icon (no mouse click).

Notice that the Pda toolbar has a dynamic aspect. When you close all protocols in the Editing pane (see below), the Pda toolbar collapses to just the first two components. In this state, with no protocol open, they are not operative.

Database Browser pane The Database Browser pane is where protocols in your database are organized and displayed. (More precisely, this is where those protocols in your working set within your database are displayed.) The presentation is folder-based, ordered alphabetically, but the actual storage is data-based. In the figure above, you will see displayed the first several protocols in the ClarkJacob library grouping. Each protocol will have derivation constituents. In the case of 6_1_1, the derivation is trivial, i.e., there is just the single derivation component. More complex protocol derivations will have multiple protocol components. These will be listed below their parent in the Browser.

To view a protocol, you right-click the tree icon adjacent to the protocol name. Your protocol will open in the protocol graphic editing pane to the right and will also be displayed above that graphic as a tab. This action produced the figure above. Note: double- clicking a protocol component in the Browser will also open the protocol in the Editing pane.

An important part of the Database Browser is the mini-toolbar that appears just below the Pda Database Browser tab. The several icons there are divided into three groups: (1) folder view, (2) derivation view, and (3) working set view. As with the icons in the Application toolbar, there is a cursor-activated descriptor.

The Database Browser display control is particularly important. The first two icons are just a collapse/expand duo. The third one, however, is a pull-down menu that enables control over which folders are displayed in the browser. In particular, notice there the concept of a working set, a feature that offers many conveniences. For example, loading protocols into your workspace upon opening Pda can be more efficient if you just load what you need. The same idea applies for exporting a working set, which you might do in order to share your protocol work with a colleague.

Editing pane Perhaps the region where you will place most of your focus is the Editing pane. In the figure above, you see a simple icon that represents a protocol named P_6_1_1. To its left are mini-toolbar buttons that operate within the context of the Protocol editor: Select, Marquee, Protocols (expanded in the figure), Constructors, and Rules. Below the main editor window are two tabs (Graph, sexpr): these control what is displayed in the Editing pane. Graph is the default selection; it shows the derivation graph depicted in a agent-arrows format, while sexpr shows a lisp-like representation for the flow of actions in the protocol under edit. See the Tips for Use Section for more information on sexpr.

Expanding (double-clicking) P_6_1_1 reveals the picture in the next figure:

For convenience the protocol elements in this example are summarized here.(For greater detail, please see the Reference Manual where the Pda protocol derivation language for protocol is presented.) The graph shows two agents, A (Alice) and B (Bob). Alice arrives at the protocol with text elements t1 and t2 already available. She creates a nonce x and sends to Bob a compound message with components t1 and a payload of (x, B, t1) encrypted by a key K[A,B] shared between them. The elements in the Protocol Mini Toolbar used to build P_6_1_1 are exposed. More information on their use is located below.

Properties/Outline pane The remaining section of the main panel is tied closely to the protocol editor pane. The next figure shows the Outline tab selected in the Properties/Outline pane. Often a protocol derivation will not conveniently fit in the Editor pane. Move the shaded viewing port in the Outline pane to expose the desired protocol section in the Editor pane.

The Properties pane is useful for seeing a summary of high level properties of each aspect of a protocol, but perhaps even moreso for editing some of them. The next figure shows how to do this. You reach this stage by clicking on the Properties tab, then right-click on a protocol element, select edit from the pop-up contextual window, click on the corresponding value in Properties, and then double-click the small rectangle to its right.

Last updated: July 17, 2006
Send comments and questions to, For more information, see also Dusko's homepage

Menu featuresUser ManualOverviewMain panel