The Process Algebra Tool

Screenshots

Click images to enlarge.

The first screen of the tool requests the user to select a particular theory. In the release versions of the tool, the tool should detect if the chosen theory is recursive and only one of the buttons "Enter Equation" or "Enter Recursive Specification" will be visible.

 
The Equation Editor consists of three main parts: the canvas on which the equation can be entered, the concrete panel from which symbols can be added to the canvas and the abstract panel with which entities can be defined.
Navigation on the canvas is possible with the mouse and the arrow keys. The mouse allows selection of a range of symbols. A selection can be deleted with the Delete button. The Delete brackets/function button allows to delete brackets surrounding a selection. If the brackets belong to a bracketed function, the function symbol is deleted as well.
The abstract panel (marked with Define Theory Entities) is used to define sets and mappings and to define the parameters of functions. After the parameter of a function is defined, a button for the function is added to the concrete panel. If the parameter is a new set or mapping, a button for this parameter is added to the abstract panel as well. If an action or variable is added to the appropriate set, a button for this entity is added to the concrete panel.
When the equation is entered, the user can check the syntactical correctness of the equation with the Validate button. If the validation is successful, the Prove button is enabled. The Prove button opens the Deriver frame.

The Deriver frame also consists of three main parts. The top of the frame shows two panels for the two sides of the equation to be proven, the result of derivation steps applied to each side and a comment for each derivation step. The user selects a side of the equation to apply an axiom to. The second part shows the axioms of the theory and the induction hypothesis if applicable. The user can select an axiom and the direction in which to apply it. The third part allows to select a term to which the axiom should be applied (symbols with blue border) and to enter a comment. After a successful derivation step, the axiom applied, the comment and the resulting term are added to the left or right equation panel.

Induction screen allows to select a variable on which to apply induction. Induction cases are defined by the algebra corresponding to the type of variable; in this case, m is a natural. The Deriver creates Deriver frames for each of the induction cases.