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
  • Database browser pane
  • Editing pane
  • Properties/Outline pane

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).

  • Error-handling controls The first toolbar group has arrow icons that will eventually be activated to support moving among error alert notices, which will be identified by small red, white-crossed circles above protocols showing in the Editing pane. Using these arrows you may navigate among any syntax errors detected by Pda in your protocol specfication. Note: you may also view each error directly by placing the cursor over the alert icons.

  • Layout support tools The second toolbar group only appears when a protocol is open for editing in the Editing pane. It offers layout support for protocol design actions. Its components are (1) undo/redo, (2) alignment, (3) editor graphics scaling, and (4) a toggle for quick editing actions. In the figure above, the scaling parameter shows as 100% of normal, and Quick Edit as not selected.

The small square colored boxes icon inside in the Application toolbar is your click-to-zoom button. Clicking it will zoom the figure in the Editing pane to fill the window to a scaling that keeps the protocol graphic’s relative height/width ratio untouched, while filling as much window as possible, as the figure below shows. To return to the unzoomed depiction, you can use the undo arrow in the toolbar or find 100% in the editor graphics scaling measurement in the pull-down menu next to the zoom icon. Alternatively, just click outside the protocol graphic and type the numeral 1.

Alignment icons are useful when you want to clean up positions of the internal agent actions in a protocol.

The Quick Edit option is a toggle that changes the default for toolbar selection in the Editing pane. When turned off, after each choice of an element from the Editing pane’s toolbar (e.g., Agent Stad), the default selection reverts to the Select arrow. When on, the last toolbar element used is again active for the next mouse click in the Editing pane.

Separated from these two groups, and located at the rightmost end of the Application toolbar, are buttons for choice of perspective. For this overview, we will work only with the default Pda perspective, which is shown selected in the figure (the Pda icon). Additional information on perspectives is available in the Preparation Subsection of the Example Section. 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.