Lesson 1: The Valve Controller Project¶

Defining the Architecture¶

The valve controller project is broken down into three simple software components, as illustrated in the following architecture diagram.

The provided port of each component is annotated with a label of the form x : X, where X is the port declaration, and x is an instance of X.

The topmost component called Application is a client of the valve controller component, and can therefore make calls on and receive signals from the valve controller. This component is outside the scope of this tutorial, but is included in the architecture to highlight the fact that there would typically be an application layer that uses the valve controller software being developed in this tutorial.

The component called ValveControllerImpl is the one being developed in this tutorial. It implements all of the hardware-independent logic, and provides all of the functions to the application layer. The partitioning of the software into the ValveControllerImpl and ValveHALBase components is designed to meet the requirement R4 and R5 above.

Finally, the component called ValveHALBase implements the hardware abstraction layer, which is responsible for abstracting away all of the hardware/software interface details about how the valve is connected and processes commands. Its implementation is written directly in C++, and is the minimum code needed to provide an interface to the hardware which is callable by a Coco component. We will see how Coco handles code developed in other languages, which interacts with the software being developed in Coco.

The components are connected together via ports as illustrated in the architecture diagram above. For example, the ValveControllerImpl component has a provided port called client (which is an instance of the port ValveController). This port specifies the functions and signals provided by this component to its clients. In contrast, ValveControllerImpl also has a required port called hal, which specifies the functions and signals implemented by the ValveHALBase component, and which ValveControllerImpl uses. These connections are declared in an encapsulating component and automatically established at runtime by the generated code.

Building Ports and Components¶

The next step is to start developing the ports and components defined in the software architecture above. Using the valve controller component as an example, the recommended steps for building this component are as follows:

1. Identify the functions and signals that the valve controller component has to implement, and provide to other components in its environment.
2. Define a port with these function and signal declarations, together with a precise description of how the valve controller component must behave across this port boundary. This port will become the provided port of the valve controller component, which it will have to implement.
3. Identify the other components in the system that will be used by the valve controller component. In this case, there is only one, namely the HAL component. Follow steps 1 and 2 to define a port for the HAL, which describes the interactions between the HAL and its client (i.e. the valve controller). This port will become the provided port for the HAL, which it has to implement correctly, and the required port for the valve controller.
4. Build the implementation of the valve controller as a Coco component.
5. Make small incremental steps, and run the verification frequently. This is referred to as a verification-driven development approach, and supports developers by making full use of the automated verification to find all of the errors for them as they build their software.
6. When all of the components are implemented and verify correctly, generate the corresponding C++ code.

Creating a new Coco Module¶

Create a new module called ValveController as follows:

1. Select the ValveProject project. If you selected Create separate folders for source files when creating the project, the Coco Platform expects all Coco files to be in the src subfolder and you must select this as the place where the new Coco source file will be created.

2. Select File → New → Coco Module.

3. Complete the module dialog box as follows:

   
   1. Enter ValveController as the file name.
   2. Click on the Finish button.

Your new module will appear in the project explorer window under the ValveProject folder. You may need to expand the project folder to see your new Coco module. The newly created Coco file is automatically opened in the editor window.

Declaring a Port¶

To declare a port for the valve controller, add the following lines to the newly created ValveController module:

port ValveController {
}

This declares a port called ValveController, the body of which will be declared inside the braces.

Declaring Function Interfaces¶

This simple port will start with four function interface declarations to initialise, terminate, open, and close a valve. To declare these new functions, add the following declarations in the body of ValveController:

  function setup() : Nil
  function open() : Nil
  function close() : Nil
  function terminate() : Nil

None of the functions have parameters, and they all return Nil, which is analogous to void in C++.

Specifying Behaviour¶

In addition to declaring functions and signals, a port can also specify the ordering in which all interactions across the port can occur. This behaviour is specified by declaring a state machine in the port declaration. Port state machines are often nondeterministic as they only specify a partial view of how a component interacts on a given boundary, in terms of the events that are visible across that boundary, and omits any of the implementation details.

A provided port P_C of some component C essentially acts as a contractual specification for how C will behave with respect to other components that use it. For example ValveController is the provided port of the ValveControllerImpl component, and will therefore specify how the ValveControllerImpl component will interact with the software application layer that uses it ValveController also acts as a specification for the ValveControllerImpl component, and the Coco Platform will formally verify whether ValveControllerImpl correctly implements ValveController. This will be discussed further in this lesson when all of the ports and components are verified by the Coco Platform.

To add the port behaviour to ValveController, extend your port by adding the following state machine declaration after the function interface declarations:

  machine M {
  }

The example state machine M above is empty, and therefore its initial state is Main. Although it does not have any transitions declared, it is still a valid state machine, and specifies that no functions are allowed to be called of ValveController.

The next step is to declare a new event state, called Uninitialised, as follows:

  machine M {
    state Uninitialised {
      setup() = setNextState(Operational)
    }
  }

Uninitialised is now the initial state of M. It has a single event transition, which says that when setup() is called, the state machine will transition to a state called Operational. The action setNextState(Operational) is a call to the built-in function setNextState(…) passing Operational as its parameter to specify the state to which that the state machine will change completing the transition.

Uninitialised does not declare transitions for any of the other functions in ValveController, which means that a component requiring this port is not permitted to call these other functions while the port is in this state.

port Explicit {
  function start() : Nil
  function stop() : Nil

  machine M {
    start() = {}
    stop() = illegal
  }
}

port Implicit {
  function start() : Nil
  function stop() : Nil

  machine M {
    start() = {}
  }
}

The Coco editor will show a static error in your current version of ValveController, because Operational has not been declared yet. This error will disappear once this state has been added as follows:

  machine M {
    state Uninitialised {
      setup() = setNextState(Operational)
    }
    state Operational {
      open() = {}
      close() = {}
    }
  }

In Operational, the functions open() and close() can be repeatedly called, and in both cases the state machine will simply remain in the same state.

The final step in completing ValveController is to add the termination behaviour:

  machine M {
    terminate() = setNextState(Terminated)

    state Uninitialised {
      setup() = setNextState(Operational)
    }
    state Operational {
      open() = {}
      close() = {}
    }
  }

The highlighted transition specifies that when the function terminate() is called, the state machine will transit to Terminated. This transition has been declared directly in Main only, which means that it will fire when terminate() is called in any of the user-defined states in Main.

The complete Coco for this port declaration is in Example_01A/src/ValveController.coco.

Declaring a HAL Port¶

Create a new module called ValveHAL, and add the following port declaration:

port ValveHAL {
  enum Cmd {
    case Open
    case Close
  }
}

ValveHAL declares an enum called Cmd with named values Open and Close, which will be used to indicate which way the valve should be moved. It is declared locally within the ValveHAL port, and references to it will have to be qualified by the port name.

Add the following function interface declaration:

  function move(cmd : Cmd) : Nil

This function takes a parameter of type Cmd to indicate which way the valve is being requested to move.

Complete ValveHAL by adding the following state machine declaration:

port ValveHAL {
  enum Cmd {
    case Open
    case Close
  }
  function move(cmd : Cmd) : Nil

  machine M {
    move(_ : Cmd) = {}
  }
}

This port is stateless, and allows move(Open) or move(Close) to be repeatedly called by its client to open or close the valve respectively. In this example, its client will be the valve controller software being developed in this tutorial.

Note the following line in the state machine:

    move(_ : Cmd) = {}

ValveHAL does not use the parameter cmd. In order to prevent Coco warning us about this, the parameter name is specified as the wildcard _. The complete Coco for this port declaration is in Example_01A/src/ValveHAL.coco.

Declaring an external component for the HAL¶

Create a new module called ValveHALBase, and add the following external component declaration:

import unqualified ValveHAL

@runtime(.MultiThreaded)
external component ValveHALBase {
  val client : Provided<ValveHAL>
}

The external component ValveHALBase has a provided port called client, which is an instance of the port ValveHAL declared above. This component will be used when code is generated for the other Coco components being implemented.

The complete Coco for this external component declaration is in Example_01A/src/ValveHALBase.coco.

Results (Example_01A)¶

All of the ports and components we have built so far in this tutorial verify correctly. Assuming the manually-written C++ implementation of the ValveHALBase component correctly implements its provided port, then this means that the code generated by the Coco Platform for the ValveControllerImpl component will compile and execute as expected, without any errors.

If you are interested in provoking the Coco Platform to find a verification error in order to see what a graphical counterexample looks like, then you can make the following amendment to the state machine declaration in the ValveControllerImpl component to comment out the termination behaviour, and rerun the verification:

// client.terminate() = setNextState(Terminated)

The verification will find an error in one of the assertions for the ValveControllerImpl component, because it no longer correctly implements its provided port.

Alternatively, there are plenty of counterexamples presented in the Verification section in the Coco Language Reference, and more will be generated throughout the rest of the tutorial.

Building a SimulatorImpl Component¶

The hardware simulator is a simple Coco component that implements the ValveHAL as its provided port. When called to move, it simply sleeps for 10 seconds to simulate a blocking valve hardware that takes 10 seconds to operate. The SimulatorImpl component is declared as follows:

import CPP
import unqualified ValveHAL

// Access to the stdlib function std::this_thread::sleep_for
@CPP.mapToValue("std::this_thread::sleep_for", .System("thread"))
external function chronoSleep(t : Duration) : Nil = {}

@runtime(.MultiThreaded)
component SimulatorImpl {
  val client : Provided<ValveHAL>

  machine M {
    client.move(_ : ValveHAL.Cmd) = chronoSleep(seconds(10))
  }
}

The function chronoSleep(t : Duration) is declared as an external function, and is labelled with the @CPP.mapToValue attribute. This maps the external function to the C++ signature of the standard library function std::this_thread::sleep_for(t : Duration), and specifies the system header file to be included in the generated code.

The built-in Coco type Duration is automatically mapped onto the standard library type std::chrono::duration. This means that when Coco encounters a reference to chronoSleep(t), it will output std::this_thread::sleep_for(t) in the corresponding generated C++.

The state machine has a single transition declared in Main:

    client.move(_ : ValveHAL.Cmd) = chronoSleep(seconds(10))

When the function client.move(cmd : ValveHAL.Cmd) is called, it calls the function chronoSleep(seconds(10)) defined above.

This is the entire behaviour for the simulator.

The complete Coco for this component is in Example_02A/src/SimulatorImpl.coco.

Declaring an Encapsulating Component¶

An encapsulating component is a component that defines a collection of components, and specifies how they are connected together. It can have zero or more provided or required ports, but it cannot have a state machine. It must declare instances of all the components it owns and have a constructor that includes connector functions, specifying the connections between the encapsulating component’s ports and those of the component instances it owns.

Declare the following encapsulating component:

import unqualified SimulatorImpl
import unqualified ValveController
import unqualified ValveControllerImpl
import unqualified ValveHAL

@runtime(.MultiThreaded)
component TestValveGroup {
  val client : Provided<ValveController>

  val valve : ValveControllerImpl
  val hal : SimulatorImpl

  init() = {
    connect(client, valve.client);
    connect(valve.hal, hal.client);
  }
}

The following architecture diagram is a graphical representation of TestValveGroup:

TestValveGroup is an encapsulating component that provides one port client, and owns two component instances, valve of type ValveControllerImpl and hal of type SimulatorImpl. The init() declaration is its constructor, which specifies how the component instances are connected together. In this case, init() specifies that:

1. The TestValveGroup component’s own provided port client is connected to the provided port client of the component instance valve.
2. The required port hal in component instance valve is connected to the client port of the component instance hal.

The complete Coco for this encapsulating component is in Example_02A/src/TestValveGroup.coco.