Contextual menus

Contextual menus appear in the Browser pane, the Editing pane, and the Properties pane. To pop-up a contextual menu, right-click in the pane itself or on an object within the pane.

Browser pane menus

Right-clicking in the browser pane produces results that are state dependent. If you have no folder nor protocol selected, your pop-up menu will offer you the option to create a New Root Folder. You would accept the option if you wanted to create an additional protocol collection at the top level of your browser hierarchy.

If you right-click with a folder already selected, you see a more elaborate pop-up offering, as shown in the next figure.

New provides a pull-out menu with options for Folder, Pda Diagram, and Pda Rule Diagram. Selecting the first will create a folder within your selected folder, useful for collecting subgroups of protocols. The next two, respectively, create an entry for a new protocol or rule. Pick one and you will be presented with a dialogue to name it.

New Root Folder is the same option offered when no folder is selected.

Move to Trash will install a Trash icon in your Browser toolbar and put a selected Folder or protocol or rule into it. If you open the Trash (double-click its icon), select and right-click an item, you are offered the option to restore it. If the Trash is empty, its icon is no longer displayed. If you click on the Trash icon in the Browser toolbar, then right-click on the Trash icon in the Browser, you gain the option of emptying the Trash. As usual, this is not undoable.

Rename provides a dialogue for changing the name of a folder, protocol, or rule.

Export to snapshot file, resp. Import from snapshot are the means by which you export, resp. import an item from your database, for sharing or archiving. Each will enable you to navigate in your platform’s file system for the operation.

Create working set allows you to create a filter in your database for convenience in loading and display. The next figure shows the dialogue with options for naming, overwriting, or merging working sets.

If you right-click with a protocol already selected, you see a pop-up menu with only one new option,Copy, as shown in the next figure.

The paired Paste can be executed if you select and right-click a target folder in the Browser.

Editing pane menus

The contextual menus in the Editing pane depend upon whether you wright-click on or in a protocol box or not. If you click outside all protocol boxes, a menu pops up, but only Zoom and Save result in any action that, in each case,is self-explanatory. The other items will be removed in future versions.

Clicking inside a protocol box, but not on an agent or send/receive arrow, brings up the important menu shown in the next figure.

Copy reference If you click inside a protocol box, outside of all agents, stads, and arrows, you will see Copy reference in the contextual menu. You can then paste the result into the existing protocol folder or another one that is open. Note, open protocols are shown as tabs above the Editor pane. Copying a reference is analogous to an alias (Mac) or shortcut [pointer] (Win). See the Usage Tips section for more information on this.

Edit Click on an item within a protocol box to open an editing window for that object. The editable items include in and out, stads and arrows. Actually, you edit the contents of the arrow, i.e., its payload description. Editing for in and out and arrows produces the same contextual menu. The entries are self-descriptive. Select Edit to change the value, then click anywhere outside the element to accept the change. Another option after Edit is selected for an object is to click on the object’s value in the Properties pane. If a small rectangle appears, clicking that will bring up a larger editing window. See the end of the Main Panel section for an example.

For a stad, the contextual menu contains items that relate to a state in the protocol’s evolution (that’s what a stad is). Many of the menu items are self-descriptive. The other ones of interest are: Specware: this will generate a MetaSlang representation for the stad. Generate s-expr: this will generate an s-expression for the stad. Specware and sexpr data for the collection of stads can be viewed by selecting the specware, resp. sexpr tab below the editing pane.

Collapse This option will collapse the detailed internal view of the protocol to the generic icon form. If your editing pane is full of protocols, you may wish to reduce the display’s complexity by collapsing all but the protocol of immediate interest.

Check Element(s) When you have edited a protocol in the Editing pane, you may wish to check for syntactic correctness without regenerating the whole protocol. Use this option to carry out that function.

Generate Protocol Contents When you edit certain elements in a protocol, the changes may naturally propagate to other items in the current protocol and child nodes in the refinement graph. Although you do not have to regenerate the contents, not doing so affects referential integrity.That is, your protocol will no longer necessarily adhere to structures in its lineage. By the same token, if you want to override a feature in a parent (or higher in the lineage) protocol, do not regenerate the contents you have edited. Opt carefully for override, since this action will immediately update your protocol’s definition in your database, with no recourse to Undo.

Create New Instance In many protocol derivations you will want a copy of a protocol for describing your refinement . Click on the parent, select Create New Instance, and the result is a child instance as shown in the next figure. Now work your refinement into the new instance. More detail can be found in the Example section.

Edit spec To examine and edit the specs associated with a protocol, use the Edit Spec command. As shown in the next figure this brings up a window with 3 tabs labeled User-Spec, Auth-Spec, and Prove Commands.

The User-Spec is where the user can enter a spec for the functions in the protocol. For example, in the CR protocol (the abstract Challenge-Response protocol) the following spec was entered to characterize the c and r functions.

spec
 op c: Agent * Agent * Nonce -> Term
  op r: Agent * Agent * Nonce -> Term
  axiom cr is
  fa(m:Nonce,agentA,agentB,sendingC,receivingR)
 	  agentA = creator(m) &&
         firstSendIn(sendingC, agentA, c(agentA,agentB,m)) &&
         receivingR isA receiveIn(agentA,r(agentA,agentB,m)) &&
         sendingC precedes receivingR
      =>
  (ex(receivingC,sendingR)
  receivingC isA receiveIn(agentB,c(agentA,agentB,m)) &&
  firstSendIn(sendingR, agentB, r(agentA,agentB,m)) &&
  sendingC precedes receivingC &&
  receivingC precedes sendingR &&
  sendingR precedes receivingR)
endspec

The Auth-Spec tab contains specs automatically generated by the Pda system. It contains several specs. The first spec is labeled UserBase and is a copy of the user spec with an import of the base theory for protocols.

If the protocol is an instance of another protocol, then the Auth-Spec contains a spec called Instance that contains theorems and conjectures derived from the specs for which this is an instance.

The last spec under the Auth-Spec tab is called Conjectures. It contains authentication conjectures generated by Pda from the protocol diagram.

Under the Prove Commands tab are prove commands of the form prove conjecture_name where conjecture_name is a conjecture in the Conjectures spec. The user can ask Pda to try to prove a conjecture by right clicking on a conjecture, moving the mouse down to Specware and then clicking on one of the Prove commands that pops up (these come from the contents of the Prove Commands tab). This causes Specware to try to prove the conjecture using Snark.

For more details, please see the Proofs section.

Apply Constructor Constructor design is under review. Design changes are certain, so until then this command should not be used.

Show in Derivation Browser If you right-click on a protocol in the Editing pane, this command will create a derivation browser palette to the right of the pane. All the protocols in your working set will be examined for their dependencies, which the browswer palette then displays. This is the same functionality you will find with the tree icon above the Browser pane.

Add default agent input/output edges This command refers to the input/output annotations at the top/bottom of an agent’s slice of the protocol. Select the protocol, choose this menu item and the notations for each Agent Ai will be created: in[Ai]/out[Ai], for each i. If the annotations are already present, even if not the default, no change will be made. One situation where this feature might be convenient is to roll back a user’s changes to the default in[]/out[].

Specware This item pulls out to offer the option Generate spec for protocol. Selecting this option will have no effect unless a Specware process has been started. (See the Installation Section). If you do have a process running, a formal specification in Specware’s language MetaSlang will be created.

Generate s-expr Please see the S-Expr Plug-in section for an explanation of this menu item.

Change font size This command can help make a protocol derivation easier to read. Click on any text entry in a protocol to select that component. Then right-click to bring up the contextual menu and select Change font size. You will be provide with a pop-up menu with options to increase or decrease the font size of the selected component.

Adjust bounds … @@ to be completed

Property pane menus

Fast View, Move, Size, Max/Min, Close

These contextual menu items provide options for altering the location of the panes. You reach the options by clicking in the Properties/Outline pane title area.

@@ to be completed

Copy

If you click in the region within the Properties pane, the item you are pointing to is placed on the Clipboard in the usual manner.

---