Contextual menus

Contextual menus

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

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.

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.

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.

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.

Contextual menus