In the next image you can see the CoPS' environment. On the top there is the main menu, just below you can see the toolbar with shortcut buttons to the main actions of CoPS. For instance, the toolbar allows you to specify the security property to be checked. On the left there is the system treeview, which is useful to both move on an agent and verify it. The main area is the editor pane, where you can edit your systems. On the bottom you find the kernel messages area, which tells you error and warning messages, the result of the security check, and some time/space execution information. On the very bottom there is the status bar.

click to enlarge

In the image you can also see the code-autocompletion list and the graph viewer.

To start you can either edit a new system or load it from a file (e.g., one of the examples available on this site). The editor has the standard utilities: cut, copy, paste, undo, redo, open, save, create a new file, and find/replace text.

The process must be declared using the SPA language, an extension of Milner's CCS. The sintax rules are recalled in the "Sintax Help..." of the "Help" menu. You need to use three keywords:

1. bi: to declare an agent (BInd agent). After a "bi" there must be a space (new line, tab, ...), a variable identifier starting with an uppercase character, an other space, and then the agent definition. For instance, "bi A (a.A+b.A+c.A+d.A)\S".
2. basi: to Bind Action Set Identifier. After a "basi" there must be a space, a variable, an other space, and then a list of action identifiers, starting with a lowercase character, separed by spaces. For instance, "basi S a b".
3. acth: to declare the high actions set (Act_H). It has to be declared at most one time. The sintax is the same as the "basi" one, but without the variable for the name of the set. For instance, "acth c e f".

To speed up the editing you can use the code auto-completion utility which remembers the actions and agents just used. If you need to rewrite same the action many times, you can: write the initial letters of the identifier and press CTRL+SPACE to see all the possible completions. To select the right one either use arrow keys or continue to write and CoPS moves the selection to the more similar idientifier. When you have choosen press the Return key or a non alphanumeric key (e.g., an operator or the spacebar).

Now that you have declared the process you want to test if it is secure. To do this from the toolbar you have to: select the security property that you want to verify; check if you want to use the compositional technique; click the green "V" button to start the verifier. In case of errors or warnings you can view them by clicking the two buttons on the toolbar (last two before the info button).

click to enlarge

If everything is all right, in the kernel messages area you can see the security results. When the kernel has finished you can view the graph of the system by clicking the button on the toolbar.

Notice that when you check the system (by clicking on the toolbar check button or from the menu "Tool") CoPS verifies the first agent declared in the file. If you have choosen to check weak or strong bisimulation, then CoPS compares the first two agents declared.
To change this default behaviour you can right click on the agent that you want to verify in the treeview on the left. You will see a context menu. Here you can choose "Check Agent". You can proceed similarly in the case of bisimulation comparison (instructions on the status bar will drive you).

SETTINGS

It is also possible to customize the sintax highlight. To do this select the menu item "Settings..." in the "Edit" menu and choose the "Fonts" tab. We suggest you to use for the internal action tau a font which writes "tau" instead of "t" (e.g., "Euclid"). The next image shows the fonts settings dialog.