Lesson 3: Accommodating Hardware Changes¶

Declaring an External Type for the Valve Parameters¶

The format and semantics of the valve parameters do not need to be known by the clients of the ValveHALBase component, namely the ValveControllerImpl. The ValveControllerImpl is simply acting as a conduit that feeds the data as an opaque block from its clients through to the ValveHALBase. In Coco, such data are declared as an external type in the provided port ValveHAL of ValveHALBase.

In order to be able to generate C++ code later in the tutorial, we need to specify the mapping between this external type and C++ code.

Add the following line to import the C++ language mappings:

import CPP

Add the following external type declaration labelled with the @CPP.mapToType attribute:

  @CPP.mapToType("ValveHALTypes::Params", .ConstReference, .User("ValveHALTypes.h"))
  external type ValveParameters

The @CPP.mapToType attribute specifies that the external type ValveParameters declared in Coco is mapped to the C++ type ValveHALTypes::Params specified in the header file called ValveHALTypes.h. In function calls, it is passed as a const &. This is one of several Coco features for specifying mappings between Coco and C++, which are explored in more details later on in the tutorial.

Adding a New Function¶

Declare a new function interface in ValveHAL for setting the parameters as follows:

  function setParameters(prms : ValveParameters) : Bool

This function takes an instance of ValveParameters, and returns true if they are valid, and false otherwise.

Extending the State Machine¶

The ValveHALBase software is a simple piece of handwritten code necessary to make the hardware/software interface directly callable by the code generated from a Coco component. It is important that it is simple because there is no automated method of ensuring that handwritten code implements its Coco port specification; this has to be checked by manual review. To simplify this process, it is good practice to ensure that the structure of the Coco port is aligned as closely as possible to that of the handwritten code.

Therefore, instead of changing the current port state machine into one with several user-defined states, the new behaviour will be added to Main using a boolean variable to keep track of whether parameters have been specified or not, and to guard the new event transitions. This should ensure that the Coco port will closely align to the handwritten ValveHALBase code.

The new requirement is that a valve movement is only allowed after a correct set of valve parameters has been accepted by ValveHALBase. Furthermore, once a set of parameters has been accepted, it is not allowed to change them.

Declare a new boolean variable in the state machine as follows:

    var paramsSet : Bool

By default, boolean variables are initialised to false.

Add the following event transition for the newly declared function setParameters(…) in Main:

    if (!paramsSet) setParameters(_ : ValveParameters) = paramsSet = nondet {
      true,
      false,
    }

This transition is guarded, and is therefore only enabled when the value of paramsSet is false. The function is called with _ as its argument, which is the wildcard pattern, and means that it matches any value. The value passed as an argument to this function cannot be referenced in the port state machine. This is required because the parameter is an unverifiable type.

The body of the event handler for this transition is a block expression with the following effect:

1. The nondet expression is evaluated to true or false, the choice being made nondeterministically;
2. The resulting value is assigned to the Boolean variable paramsSet;
3. The value assigned, namely the value of the assignment expression, is returned as the value of the setParameters(…) function call.

Finally, we must amend the event transition for the function move(…) by adding the following guard:

    if (paramsSet) move(_ : Cmd) = nil

This transition is now only enabled when paramsSet evaluates to true.

After making these changes, your ValveHAL port should look like the following:

import CPP


port ValveHAL {
  enum Cmd {
    case Open
    case Close
  }
  @CPP.mapToType("ValveHALTypes::Params", .ConstReference, .User("ValveHALTypes.h"))
  external type ValveParameters

  function setParameters(prms : ValveParameters) : Bool
  function move(cmd : Cmd) : Nil

  machine M {
    var paramsSet : Bool

    // accept or reject valve parameters and remember result
    if (!paramsSet) setParameters(_ : ValveParameters) = paramsSet = nondet {
      true,
      false,
    }
    // Move valve if valid parameters set
    if (paramsSet) move(_ : Cmd) = nil
  }
}

The complete Coco for this port can be found in Example_03B/src/ValveHAL.coco.

Verifying your Changes (Example_03B)¶

Run the verification on the modified Coco files in this example. The Coco Platform finds errors in both the SimulatorImpl and the ValveControllerImpl. Let’s start by analysing the error found in the SimulatorImpl component.

The SimulatorImpl is failing to implement its provided port with the following counterexample:

Modifying the SimulatorImpl¶

Inspecting the ValveHAL port we can see the following:

1. When setParameters(…) has been called and returns true, it cannot be called again.
2. The move(…) function can only be called after a successful call to setParameters(…).

To make SimulatorImpl comply with these requirements, we need to modify it to remember when a successful call has been made to the setParameters(…) function. Before this has occurred, the move(…) function must not be allowed. After this has occurred, the move(…) function must be allowed, but all further calls on setParameters(…) must be forbidden.

To achieve this, we are going to use transition guards. Modify the SimulatorImpl state machine as follows:

  machine M {
    var parmsSet : Bool
    if (!parmsSet) client.setParameters(_ : ValveHAL.ValveParameters) = parmsSet = true
    if (parmsSet) client.move(_ : ValveHAL.Cmd) = chronoSleep(seconds(10))
  }

The following line declares a variable called parmsSet of type Bool, which is initialised to false by default:

    var parmsSet : Bool

The following line defines a guarded transition for the setParameters(…) function; it is only enabled if parmsSet is false; its handler always returns true, and sets parmsSet to true:

    if (!parmsSet) client.setParameters(_ : ValveHAL.ValveParameters) = parmsSet = true

The following line defines a guarded transition for the move(…) function so that the transition is only enabled when parmsSet is true:

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

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

Verifying your Changes (Example_03C)¶

After modifying SimulatorImpl, re-run the verification. All of the assertions for your SimulatorImpl component should now pass.

However, the Coco Platform finds an error in one of the assertions for the ValveControllerImpl component. ValveHAL is also a required port of the ValveControllerImpl component, and with the changes we made to it above, the ValveControllerImpl no longer uses this required port correctly. The Coco Platform gives the following counterexample:

Importing ValveHAL Module Declarations¶

Add the following line to bring the declaration of ValveParameters into scope:

import unqualified ValveHAL

Extending the setup(…) Function with Parameters¶

Amend the setup(…) function interface declaration so that it has an input parameter, and returns a boolean, which reflects whether the parameters are valid or not:

  function setup(prms : ValveHAL.ValveParameters) : Bool

Modifying the state machine¶

Modify the state machine to reflect the changes made to the initialisation process. Specifically, in state Uninitialised, the transition specified for the function setup(_ : ValveHAL.ValveParameters) needs to reflect the possibility that the parameters might be rejected. The reasons for rejection are unknown by the port, not least because ValveParameters is an external data type, and therefore opaque to Coco. However, the port can reflect this behaviour by modelling it as nondeterministic choice between the parameters being accepted as valid or rejected as invalid.

Modify the transition as follows:

      setup(_ : ValveHAL.ValveParameters) = nondet {
        @represents("Invalid parameters")
        false,
        @represents("Valid parameters")
        {
          setNextState(Operational);
          true
        },
      }

The body of the event handler is now a nondet expression with the following two cases: false, indicating invalid parameters, in which case the state machine remains in the same state, and true, indicating valid parameters, and the state machine transitions to the state Operational. Each nondet case is labelled with a @represents attribute, which annotates these actions in any verification counterexamples that are generated.

The resulting ValveController port is as follows:

import unqualified ValveHAL

port ValveController {
  function setup(prms : ValveHAL.ValveParameters) : Bool
  function open() : Nil
  function close() : Nil
  function isOpen() : Bool
  function isClosed() : Bool
  function terminate() : Nil

  machine M {
    enum ValvePosition {
      case Open
      case Closed
      case Unknown
    }
    var position : ValvePosition = ValvePosition.Unknown

    isOpen() = position == ValvePosition.Open
    isClosed() = position == ValvePosition.Closed
    terminate() = setNextState(Terminated)

    state Uninitialised {
      setup(_ : ValveHAL.ValveParameters) = nondet {
        @represents("Invalid parameters")
        false,
        @represents("Valid parameters")
        {
          setNextState(Operational);
          true
        },
      }
    }
    state Operational {
      open() = {
        position = ValvePosition.Open;
      }
      close() = {
        position = ValvePosition.Closed;
      }
    }
  }
}

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

Verifying your Changes (Example_04A)¶

All of the updated ports and components verify successfully.