Eclipse¶

Coco Perspective¶

After installing the Coco Platform in Eclipse, the Coco Perspective will be the default one when Eclipse opens. It can also be opened in any of the following ways:

1. Click the Coco button at the extreme righthand end of the main Eclipse toolbar.
2. Click the Open Perspective button in the tool bar, and select Coco from the popup list.
3. Select Window → Perspective → Open Perspective → Other… → Coco in the Eclipse menu, and click Open.

By default, the Coco perspective consists of the following views:

Each view numbered above has the following functionality:

1. The Project Explorer view is where Coco projects, modules, and generated code are created, opened, closed, renamed and deleted.

2. The Coco Editor views are where Coco modules are edited.

3. This area has the following views:

   • Counterexamples view displays extensive debugging information for the verification errors found by the Coco Platform.
   • Simulator view is where users can drive the Coco simulator to interactively explore port and and component state machines, and counterexamples.

4. This area has the following views:

   • Assertions view displays the list of assertions to be verified, and their verification status.
   • Outline view displays the structure of the Coco module displayed in the currently selected editor view.

   Both views can be independently linked to the Coco Editor.

5. This area has the following views:

   • Console view displays console output.
   • Problems view displays messages for errors and warnings in Coco modules.
   • Progress view displays the verification progress.
   • State Machine Diagram view displays a graphical representation of Coco state machines.

Coco Preferences¶

The are a number of Coco-specific preferences, which can be view and modified in the usual way by selecting Eclipse → Preferences → Coco Platform, and clicking on one of the following options:

• Coco Editor:
  • Save Actions: when selected, the Coco is automatically formatted whenever it is saved.
  • Typing provides a range of editing preferences.
• Logs allows you to select whether crash reports are automatically submitted to Cocotec.
• Source Path specifies the build path entries used as the default when creating new Coco projects.
• Verification allows you to control whether the verification is run remotely or locally:
  • Disabled: The verification is always performed locally.
  • Enabled: The verification is performed by the remote verification service by default. If the service is not available, then the verification is performed locally.
  • Enabled (remote when available): The verification is performed by the remote verification service by default. If the service is not available, then the verification is performed locally.
  • Enabled (remote only): The verification is always run by the remote verification service. If the service is not available, then verification cannot be performed.

Coco Packages¶

A Coco project is simply a normal Eclipse project with a Coco package called Coco.toml, which contains the Coco-related configuration settings for your project. When you create a new Coco project in Eclipse, a Coco package called Coco.toml is automatically created at the top level of your project directory containing the package name, location of the Coco source files, and the Coco version. This is illustrated in the following example of a newly created Coco project called TrafficLights:

You can extend the Coco.toml file with additional configuration settings as described in the Packages section.

When using Coco in Eclipse, there is a one-to-one relationship between a project and a package: every project must have its own Coco package, and their names must be the same. If there are any dependencies between the Coco packages, then all of the corresponding projects have to be loaded into the Eclipse workspace.

Coco Editor¶

The Coco Platform provides a custom editor that supports a number of essential features for efficiently writing programs in Coco. The first of these is semantically-aware code completion, which provides a sorted list of options that has been with the most likely choices the user is seeking at the top of the list. This runs automatically as you type, and you can also invoke this by using the keyboard shortcut Ctrl+Space.

The editor performs continuous syntax and type checking as you type. By default, errors are highlighted by underlining the relevant code in red, and displaying an error icon next to the corresponding line number. Clicking on this icon displays a tooltip describing the error, which is also displayed in the Problems view.

The editor also raises warnings about your code, such as identifying variables that are unused. By default, the relevant code is underlined in yellow, and a warning icon is displayed next to the corresponding line number. Clicking on the icon displays a tooltip describing the warning, which is also displayed in the Problems view.

The Coco Platform will offer suggestions on how to solve errors and warnings where possible. You can apply these suggestions by double-clicking on an error or warning message in the Problems View, and invoking the Eclipse Quick Fix feature in the usual way by using the keyboard shortcut Cmd+1 on macOS, or Ctrl+1 on Linux/Windows.

By default, the Coco editor automatically formats your code upon every save of the Coco module. This setting can be customised in the Coco Preferences. You can also invoke the formatter at any time using the keyboard shortcut Cmd+Shift+F on macOS, or Ctrl+Shift+F on Linux/Windows. The format applied to a Coco project can be controlled by the formatting policy setting in the project’s Package File.

In addition to the keyboard shortcuts mentioned above, the Coco editor also has the following shortcut for commenting and uncommenting code: Cmd+/ for macOS, and Ctrl+/ for Linux/Windows.

Verifying Coco¶

The Coco Platform formally verifies Coco components and ports for a broad range of properties, ranging from runtime errors through to advanced liveness properties. A detailed overview of all the properties verified can be found in the Coco Language Reference. This section steps through how to run the verification, and understand the results.

Assertions View¶

The Assertions view displays all of the properties that can be verified for components and ports, and has the following buttons in its toolbar:

Icon	Meaning
	Runs the verification for all of the assertions listed in the Assertions view. If you hover your cursor over this icon, then you will see a tooltip appear highlighting this.
	Generates the code in the subfolder generated within your project. If the folder does not already exist, it will be automatically generated.
	Forces the project to be reloaded from disk.
	Expands the top-level assertions to reveal the next level in the assertion hierarchy.
	Contracts the hierarchy of assertions back to listing the top level of assertions only.
	This can be selected by clicking the View Menu icon (denoted by three grey dots), and links the Assertions view with the Coco Editor views, so that the corresponding assertions are displayed for a Coco module selected in the editor.

The assertions are arranged hierarchically for each Coco project. When a Coco project is open and selected in the Project Explorer view, all of the Coco modules in the project are displayed in the Assertions view. Expanding a module assertion reveals the ports and components within that module. If a Coco module has unresolved syntax or type errors in it, then the corresponding assertion is labelled with an error icon, and cannot be expanded. Expanding a component or port assertion reveals the individual groups of properties to be verified in each case.

An assertion can be expanded or contracted either by clicking on the grey arrow in front of its name, or by clicking on the corresponding icons in the Assertions view’s toolbar.

Each assertion is denoted by one of the following icons representing what kind of item it is:

Icon	Meaning
	Folder
	Coco module
	Implementation component
	Encapsulating component
	External component
	Port

In the following example, a project with one Coco module called TrafficLightCrossing has been opened, and all of the assertions have been expanded to show all of the properties to be verified for the components and ports. This module contains two ports called TrafficLight and Crossing, and one component called TrafficLightImpl.

The Assertions view has a search facility, which allows you to search the assertions tree for names of folders, modules, ports and components:

As soon as you start typing in the Search box, all of the non-matching items are filtered out of the list of assertions, for example:

The Assertions view also allows you to filter the assertions based on the type of item, or verification results. To select a filter, click on the filter icon next to the search box near the top of the Assertions view, which will result in a popup menu appearing with a list of options:

By default, all assertions are displayed unfiltered. You can select which assertions to filter out by ticking or unticking the options in the popup menu. For example, if you select Show Errors Only, then the Assertions view will only list assertions that have static errors in them (denoted by ), and will therefore not be verified:

As another example, if you untick Show Successfully Verified, then only the assertions that have failed the verification are listed in the Assertions view:

Running the Verification¶

The verification can only be run on Coco projects and modules that do not have any static errors in them. Assertions for modules that do have such errors are labelled with , and will also have corresponding error messages in the modules themselves.

The verification can be run on an entire project either by:

• Clicking on in the Assertions view toolbar;
• Right-clicking on the project in the Project Explorer view, and selecting Coco → Run Assertions or Coco → Run All Assertions; or
• Selecting the project in the Project Explorer view, and using the keyboard shortcut Cmd+R on macOS, or Ctrl+R on Linux/Windows.

The following table summarises the possible results and corresponding icons that assertions can be labelled with:

Icon	Assertion Status
	The Coco module has static errors in it, and therefore cannot be verified.
	Not verified.
	The verification is currently running.
	Passed the verification successfully.
	Failed the verification with a warning.
	Failed the verification with an error.
	The verification failed due to an error in the Coco module.
	Not verified due to a verification failure of an assertion that it depends upon.
	The verification failed due to an error with the remote verification service.
	An internal error occurred during the verification.
	A timeout occurred whilst running the remote verification.

The Coco Platform runs the verification for the assertions in a specific order, reflecting the dependencies between them. If an assertion fails, then all assertions that depend upon it passing the verification successfully will not be verified, and are labelled with accordingly.

By default, the Coco Platform will not rerun the verification for assertions that have cached verification results, thereby making the verification faster and more efficient, particularly when run on large projects. Assertions are labelled accordingly to indicate whether cached verification results are available, and if so what the results are. This can be overridden by holding down the Shift key when clicking the green play button in the Assertions view toolbar.

When editing Coco modules that have already been verified, the Coco Platform intelligently identifies which assertions are impacted by the changes made. For example, any changes made to comments in a module would not impact the verification results of any of the assertions. Only assertions impacted by the changes will become labelled with again when the changes are saved, and will therefore have to be reverified.

Rather than running the verification on an entire project, you can also verify individual assertions by simply double-clicking on them. This will verify the selected assertion, together with any other assertions that it depends upon. For example, when verifying a component assertion, the verification will also verify all ports that are provided or required by that component.

Counterexamples View¶

When the verification has finished, the assertions in the Assertions view are labelled with icons indicating the verification results, which are described in the assertions results table above. Running the verification on all of the assertions for our TrafficLightCrossing example leads to the following results:

As illustrated above, if you hover your cursor over any of the assertions, then a tooltip will be displayed providing a brief description of the property being verified, and its verification status. In this example, one of the well-formedness assertions for the TrafficLightImpl component has failed (denoted by ). As a result, a number of other assertions that depended upon this one were not able to be verified (denoted by ).

If an assertion has failed with a verification error, then you can view extensive debugging information describing the error by double-clicking on the failed assertion. Using our example above, the following counterexample of the error is displayed in the Counterexamples view:

With the exception of the reachability assertions, the top pane in the Counterexamples view displays a sequence diagram, describing (one of) the shortest sequences of interactions that led to the assertion being violated. The sequence diagram consists of swim lanes, one for each component or port involved in the counterexample, and some additional ones which vary depending on the type of assertion that failed. For example, in the counterexample presented above, there is a swim lane for the component TrafficLightImpl, the required port instance pedestrian, and then an additional one labelled User, which represents an external user invoking all possible calls allowed by the component. For further details on what properties are verified, together with examples of how the different types of verification errors are presented, see Coco Language Reference.

The bottom pane in the Counterexamples view displays additional debugging information, such as stack traces for all of the relevant components and ports, variable assignments, queue contents, and subscription status.

The two panes in the Counterexamples view are interactively linked to one another, and to the corresponding Coco Editor view. This means that you can explore different states in the counterexample either by clicking on any of the states in the sequence diagram, or by selecting states in the stack traces. This will highlight the corresponding code in the Coco Editor view, and show what values are assigned to the variables, along with other information such as the queue contents for your selected state.

The Counterexamples view also has a popup menu, which appears by right-clicking anywhere in the view, and provides the options for saving the sequence diagram image to a file, or copying it to the clipboard.

Note

When running the verification, the Counterexamples view displays the most recently loaded counterexample, even when the project has been reverified and the counterexample is not longer relevant. Therefore, it is good practice to either close the Counterexamples view before rerunning the verification, or make sure you refresh the counterexamples being displayed by double-clicking on any failed assertions after rerunning the verification again.

A counterexample can also be reopened in the simulator allowing you to explore alternative scenarios. To do this, either click on in the toolbar, and select the component or port instance in the dropdown list, or hover directly over one of the swim lane labels and click on that appears next to it:

This will launch the Simulator view with the counterexample loaded. You can then use the Coco Simulator in the normal way, for example by rolling back the simulation to an earlier state and exploring alternative paths to help understand and debug the error:

Coco Simulator¶

The Coco simulator allows port and component state machines to be interactively explored, where you can choose which event should be performed at each step. Further, you can also launch the simulator with a counterexample (generated by the verification), and explore alternative scenarios based on the counterexample.

To launch the Coco simulator, right-click on a port or component in the Assertions view, and select Simulate in the popup menu:

As illustrated above, the simulator is launched in the top pane of the Simulator view.

At the top of the pane, there is a toolbar with the following five buttons: the first one saves the sequence diagram image to a file, the next three buttons enable users to zoom-in, zoom-out, and restore the view to its original size, and the last button () closes the current simulation being run.

At the bottom of the pane, the Simulator view has another toolbar for driving the simulator with the following buttons:

Icon	Name	Meaning
	Step Into	Advances execution at the lowest instruction level of granularity, in particular stepping into any functions invoked.
	Step Over	Advances execution at a coarser statement/line level of granularity, in particular stepping past any functions invoked.
	Step Out	Advances until the current function/stack frame returns.
	Step to Event	Advances execution until the next externally visible event, for example a spontaneous transition or a call to a transition function on one of the components or ports.
	Select Next Event	Displays the event selector, so that you can choose the next spontaneous transition or transition function call to take place in the system.

The first four buttons listed above are collectively referred to as the step buttons. Note that for Step Into and Step Over, the granularity does not always map exactly to the familiar instruction and line level step functions of a conventional debugger due to the restrictions in the underlying computation model of the simulation.

To get started, click on one of the step buttons (for example, ), which will cause the event selector popup menu to appear listing the possible events that you can select. If more than one choice is displayed, then these reflect different possible interleavings of events. Clicking outside the event selector will hide it, and clicking causes it to be redisplayed. If the simulation has reached a state requiring you to choose an interleaving, then the step buttons will be disabled until an event has been selected. You can change your mind prior to continuing the simulation by redisplaying the event selector, and choosing a different event. To execute the selected event, click on one of the step buttons.

When clicking on one of the events in the event selector list, it will appear in blue in the sequence diagram, as illustrated below:

In the sequence diagram, the component or port state machine that is executed by each chosen step is highlighted with a dashed blue line around the label of the corresponding swim lane. For example, the pedestrian port instance is highlighted in the example above, as it is currently executing the spontaneous transition previously selected.

The bottom pane in the Simulator view displays the same additional debugging information as displayed in the Counterexamples view. The two panes in the Simulator view are interactively linked to one another, and to the Coco Editor view, as they are in the Counterexamples view. This means that the code corresponding to the most recent step selected in the simulator is highlighted. This is illustrated in the example above, where the pedestrian instance of the port Crossing is executing the spontaneous transition in state Main.

At any point in the simulation, you can roll back the simulation to an earlier state in your sequence diagram, and explore alternative scenarios. If you hover your curser over an earlier state in the sequence, the roll back icon will appear next to the state, as illustrated in the following example:

If you click on , then the simulator will roll back to this point in your simulation:

You can then continue stepping through different scenarios with the simulator in the normal way.

Visualising State Machines¶

The Coco Platform allows users to automatically generate graphical representations of their port and component state machines. To generate these diagrams, right-click on a port or component in the Assertions view, and select State Machine Diagram in the popup menu:

As illustrated above, the state machine diagram is shown in the State Machine Diagram view. This graphical representation displays all of the states declared in the original Coco state machine as rectangular nodes that are labelled with their corresponding state identifiers. The state hierarchy is also preserved in the graph; for example, in the state machine diagram above, the node labelled Stop is displayed within the node Active, which means that Stop must have been declared as a nested state within Active in the original Coco program.

The state machine diagram also displays all of the transitions declared between the states as directed edges between the nodes. These edges are either labelled with their corresponding event names, or with the labels specified in the @represents attribute where relevant.

The State Machine Diagram view’s toolbar provides you with the standard options for saving the diagram, setting the size of the image to fit within the existing view, and zooming in and out. In addition, it also provides the following two specialised options:

• Expand/Collapse Edges: This option allows you to choose between an expanded representation of the graph, where there is an individual directed edge for every transition declared between two states, or a collapsed representation where all of the event names of the transitions between the same two states are displayed in a list on a single directed edge. For example, in the traffic light example above, the graph is in the collapsed form, which is why the events stopTraffic() and after(seconds(120)) are listed together on a single edge transitioning from the state Go to ReadyToStop.
• Show/Hide Edge Labels: This option allows you to display or hide the labels on the graph edges.

By default, the state machine diagram is shown with the edges collapsed and labelled.

Generating Code¶

Once your Coco project passes all of the verification checks, you can automatically generate the code in one of the target programming languages supported by the Coco Platform either by:

• Clicking on in the Assertions view menu; or
• Right-clicking on your project in the Project Explorer view, and selecting Coco → Generate Code from the popup menu.

The code will be generated in the subfolder generated within your project. If the folder does not already exist, it will be automatically generated.

Creating a Support Bundle¶

You can create an obfuscated ZIP file of a Coco project, for example to send to Cocotec support, where all proprietary information is removed, all identifiers are obfuscated, and all comments are removed.

To create a support bundle directly in Eclipse, right-click on a project in the Project Explorer view, and select Coco → Create Support Bundle… from the popup menu:

The following popup will appear, where you can choose to export the ZIP file, or include it as an attachment in an email:

Getting Updates¶

To check for, and install, updates of the Coco Platform, select Help → Check for Updates.

You can customise how Eclipse reacts to new versions being available by selecting Eclipse → Preferences → Install/Update.

Uninstalling the Coco Platform¶

To uninstall the Coco Platform:

1. Select Eclipse → About Eclipse, and click Installation Details in the popup window.
2. Enter the word coco in the type filter text box, select all of the Coco-related entries, click Uninstall, and then click Finish.
3. Click Restart Now in the dialogue window to restart Eclipse.
4. Select Eclipse → Preferences, expand General to view its sublist of options, and click on Perspectives.
5. Select all entries with coco in the name. This can appear in the list as <coco> or <<coco>>. Click Delete to remove the Coco perspectives.

The Coco Platform is now uninstalled.