Lesson 9: Introducing Slots¶

Storing the Valve Parameters¶

The ValveDriverImpl component will receive the valve parameter values from its client via the setup(…) function, store them, and then pass them on when it makes calls on ValveHAL to move the value.

The first step is to declare a variable of type ValveHAL.ValveParameters to store these parameter values when it receives them.

ValveParameters is an external type, which means that it is not verifiable, and not defaultable. We can specify that a custom external type is defaultable by declaring an instance of Default, but we will assume that there is no such instance declared for ValveParameters in this example. Further, the ValveDriverImpl is not able to assign an initial value as part of its variable declaration, as it does not have a valid value until its client calls the setup(…) function. This means that we cannot declare the variable as follows:

var params : ValveHAL.ValveParameters

You can try adding this declaration to your ValveDriverImpl state machine, and see the corresponding error message reported by the Coco Platform.

We are therefore going to declare a variable using slots.

We achieve this by adding the following declaration to our ValveDriverImpl state machine:

    var params : Slot<ValveHAL.ValveParameters>

The next step is to modify the setup(…) transition in the Initial state as follows:

      client.setup(vParms : ValveHAL.ValveParameters) = {
        setNextState(Ready);
        true
      }

Due to the change in ValveHAL, setup(…) will never fail. In order to avoid changing its interface to ValveHALBase, we therefore return true.

Updating the Call to move(…)¶

The call to move(…) needs to be updated to include the valve parameters as an additional parameter, and return a boolean indicating whether or not the call was carried out. To accommodate this, we will start by reorganising the Ready and Moving states.

Currently, the Moving state is as follows:

    state Moving(cmd : ValveHAL.Cmd) {
      entry() = hal.move(cmd)
      client.terminate() = illegal
      periodic(milliseconds(500)) = if (!hal.isMoving()) setNextState(Ready)

      exit() = {
        client.endOfMovement(match (cmd) {
          ValveHAL.Cmd.Open => ValveDriver.ValveStatus.Open;
          ValveHAL.Cmd.Close => ValveDriver.ValveStatus.Closed;
        });
      }
    }

The call to hal.move(…) is made in the entry function. After the changes we made to the ValveHAL port, hal.move(…) can fail to start. We do not want to enter the Moving state unless the move(…) has been accepted, and the movement has started. This means that we must call hal.move(…) in the Ready state instead, and only enter the Moving state if the call has been accepted.

The transition handlers for open() and close() in the Ready state need to be modified to call hal.move(…), check the result, and only enter Moving if the movement has started. Otherwise, they should send the endOfMovement(…) signal indicating the failure and remain in the Ready state. To make this change, we will declare a function in the Ready state called perhapsMove(…) as follows:

      function perhapsMove(cmd : ValveHAL.Cmd) : Nil = {
        if (hal.move(cmd, params)) setNextState(Moving(cmd)) else client.endOfMovement(ValveDriver.ValveStatus.Error)
      }

This function calls hal.move(…). If it is accepted, it changes state to Moving; otherwise it sends the endOfMovement(ValveStatus.Error) signal, and stays in the same state.

The next step is to modify the open() and close() transitions in Ready state to call the new local function as follows:

      client.open() = perhapsMove(ValveHAL.Cmd.Open)
      client.close() = perhapsMove(ValveHAL.Cmd.Close)

The final step is to delete the entry function from the Moving state. After these changes, the ValveDriverImpl state machine should look like the following:

  machine M {
    var params : Slot<ValveHAL.ValveParameters>

    client.terminate() = setNextState(Terminated)

    state Initial {
      client.setup(vParms : ValveHAL.ValveParameters) = {
        setNextState(Ready);
        true
      }
    }
    /// Valve ready to move
    state Ready {
      client.open() = perhapsMove(ValveHAL.Cmd.Open)
      client.close() = perhapsMove(ValveHAL.Cmd.Close)
      function perhapsMove(cmd : ValveHAL.Cmd) : Nil = {
        if (hal.move(cmd, params)) setNextState(Moving(cmd)) else client.endOfMovement(ValveDriver.ValveStatus.Error)
      }
    }
    /// Asynchronously execute the synchronous valve movement
    state Moving(cmd : ValveHAL.Cmd) {
      client.terminate() = illegal
      periodic(milliseconds(500)) = if (!hal.isMoving()) setNextState(Ready)

      exit() = {
        client.endOfMovement(match (cmd) {
          ValveHAL.Cmd.Open => ValveDriver.ValveStatus.Open,
          ValveHAL.Cmd.Close => ValveDriver.ValveStatus.Closed,
        });
      }
    }
  }

The modified Coco for this component is in Example_09C/src/ValveDriverImpl.coco.

Verifying your Changes (Example_09C)¶

The verification finds a runtime error in the ValveDriverImpl component with the following counterexample:

      client.setup(vParms : ValveHAL.ValveParameters) = {
        setNextState(Ready);
        true
      }

Assigning a Value to params¶

To fix this runtime error, we need to modify the setup(…) transition handler to capture the input parameter vParms as follows:

      client.setup(vParms : ValveHAL.ValveParameters) = {
        params = vParms;
        setNextState(Ready);
        true
      }

The modified Coco for this component is in Example_09D/src/ValveDriverImpl.coco.

Verifying your Changes (Example_09D)¶

The verification fails for the assertion that checks whether the ValveHALBase component implements its provided port ValveHAL correctly, and produces the following counterexample:

Verifying your Changes (Example_09E)¶

All of the assertions for the components and ports now pass the verification.