Creating a Coco Project¶

We start by creating a new Coco project in Eclipse as follows:

1. Make sure the Coco perspective is open as described above.
2. Select File → New → Coco Project.
3. Complete the project dialog as follows:
   1. Enter a project name. We will be writing a simple traffic light example in Coco for you to use, so we have called the project TrafficLight.
   2. Select Use default location, if not already selected by default, to specify that all the source files for this project are to be stored in your Eclipse workspace.
   3. Select Create separate folders for source files, if not already selected by default. This creates a folder named src, and all Coco source files must be created in this folder.
   4. Click on the Finish button.

Creating a Coco Module¶

To create a Coco module:

1. Ensure the TrafficLight project is selected in the Project Explorer view.
2. Select File → New → Coco Module.
3. Complete the Create New File dialog as follows:
   1. Select the TrafficLight project, expand its node and select the src folder.
   2. Enter a name for your Coco module in the File name field.
   3. Click Finish.

Insert the following Coco into your newly created module:

enum Colour {
  case Red
  case RedAmber
  case Green
  case Amber
}

port TrafficLight {
  function begin() : Nil
  outgoing signal lightStatus(colour : Colour)

  machine M {
    var status : Colour = .Red

    state InActive {
      begin() = {
        lightStatus(status);
        setNextState(Active);
      }
    }
    state Active {
      spontaneous = {
        status = match (status) {
          .Red => .RedAmber,
          .Green => .Amber,
          .Amber => .Red,
          .RedAmber => .Green,
        };
        lightStatus(status);
      }
    }
  }
}

@runtime(.MultiThreaded)
component TrafficLightImpl {
  val client : Provided<TrafficLight>

  machine M {
    state InActive {
      client.begin() = setNextState(Active.Stop)
    }
    state Active {
      state Stop {
        after(seconds(90)) = {
          client.lightStatus(.RedAmber);
          setNextState(ReadyToGo);
        }
      }
      state Go {
        after(seconds(120)) = {
          client.lightStatus(.Amber);
          setNextState(ReadyToStop);
        }
      }
      state ReadyToGo {
        after(seconds(3)) = {
          client.lightStatus(.Green);
          setNextState(Go);
        }
      }
      state ReadyToStop {
        after(seconds(3)) = {
          client.lightStatus(.Red);
          setNextState(Stop);
        }
      }
    }
  }
}

If you are writing this example yourself, you will see some of the features we have in the Coco editor, such as semantically-aware code completion, inline errors and warnings, and automatic formatting (upon saving). Further details about these features can be found in Coco Tooling - Eclipse.

In this traffic light example, we have a port called TrafficLight, and a component called TrafficLightImpl, which has an instance client of TrafficLight as its provided port, and no required ports. A component’s provided port acts as its specification, which the component must correctly implement. The Coco Platform will automatically formally verify whether this is the case, together with a number of other properties, and provide graphical counterexamples of any errors found. You can find further details about what properties are verified in the Coco Language Reference.

Verifying Coco¶

When you save your Coco module, and provided you have not introduced any syntax or type errors, you will see an assertion, labelled with the module name (in our case, TrafficLight), in the Assertions view. This view lists all of the assertions that will be formally verified by the Coco Platform. You can expand an assertion by clicking on the grey arrow in front of the assertion name to reveal the ports and components, and the properties that will be verified for each.

To verify the entire project, click on in the toolbar of the Assertions view:

There are a number of different assertion results that can arise from running the verification, each of which are denoted by a specific icon. A summary of them all can be found in Coco Tooling - Eclipse.

In our example, all of the assertions for the port pass (denoted by ), whereas the component has failed the assertion (denoted by ) that specifies that it must correctly implements its provided port. As illustrated above, if you hover your cursor over a failed assertion, then a tooltip is displayed with a brief description of the property being checked.

To debug this error, double-click on the failed assertion to open a Counterexamples view, which describes how the property was violated:

As illustrated above, the Counterexamples view consists of a graphical sequence diagram, describing (one of) the shortest sequences of interactions that the component could perform that led to it violating its provided port specification. For this type of counterexample, there are three swimlanes in the sequence diagram: one for the component (TrafficLight), one for the component’s provided port (client), and one labelled User, which represents an external entity invoking all possible calls allowed by the provided port. If the component correctly implements its provided port, then it must perform all events that its provided port specifies it must, and it must not be able to perform any events that are not permitted by its provided port. You can find a more detailed description of this property (and all other properties verified) in the Coco Language Reference.

In our example, we can see when the start() function is called on the component, it immediately returns. This is not allowed by its provided port, which specifies that when start() is called, the component must send the signal lightStatus(Colour.Red) and then return.

The Counterexamples view also provides additional information below the sequence diagram to help users understand the errors found by the verification. You can find further details about these features, and how you can use them effectively to debug your software, in Coco Tooling - Eclipse.

To correct the error found in our example, go to the component’s state InActive and replace the event transition for start() with the following:

client.start() = {
  client.lightStatus(.Red);
  setNextState(Active.Stop);
}

If you save your changes, and rerun the verification, then all of the assertions should now pass.

Generating Code¶

Now that your Coco project passes all of the verification checks, you can generate the corresponding C++ by simply right-clicking on your traffic light project in the Project Explorer pane, and select on Coco → Generate Code. The C++ code will be generated in the folder called generated.