Lesson 9: Introducing Slots

The ValveHALBase component is currently specified to receive and store the valve parameters it needs in order to interface with the underlying hardware and carry out its movements. This assumes that the ValveHALBase has sufficient resources to be able to do this. In this lesson, we are going to make the changes needed to support a more primitive ValveHALBase component that does not implement a setParameters(…) function, and cannot store the valve parameters itself. Instead, these parameters will be supplied by its client, ValveHALBase, each time it calls the move functions on ValveHALBase.

To achieve this, we will need to extend the ValveHALBase component to handle and store values that are of an external type, namely of type ValveParameters, which was introduced in earlier lessons. In this lesson, we will introduce the builtin type Slot for this purpose, which can be used to allow some verification to be done on non-verifiable types, such as external types. In particular, slots can be used to check that a non-verified type is accessed correctly by the program, even if the actual value is not available.

Overview of Changes

In this lesson, we will change the ValveHALBase component into one that cannot store the valve parameters, but which requires them to be provided as a parameter on every call to move(…). To do this, we will:

  1. Modify the ValveHAL port to remove the setParameters(…) function, extend the signature of move(…) with an additional parameter of type ValveParameters, and change the return type of move(…) from Nil to Bool. In its state machine, we will update the move(…) transition in state Ready to conform to the new signature, and return a value of type Bool to indicate whether or not the operation started. We assume that if the valve parameters passed to ValveHAL in the move(…) function are incorrect, then the move operation will not start.
  2. Modify the SimulatorImpl component to implement the changes to ValveHAL.
  3. Modify the ValveDriverImpl component to store the ValveParameters using slots, and conform to the new behaviour specified by ValveHAL, which it uses.

The changes to ValveHAL and SimulatorImpl are left as an exercise for you. The modified versions of ValveHAL is in Example_09B/src/ValveHAL.coco, and the modified version of SimulatorImpl is in Example_09B/src/SimulatorImpl.coco. Try to make the changes yourself before referring to these solutions.

We will now go through the changes required to the ValveDriverImpl component on the assumption that the ValveHAL port and SimulatorImpl component have been correctly updated as described above and in Example_09B.

Step 1: Modifying ValveDriverImpl

With the changes already made to the ValveHAL port and SimulatorImpl component above, you will find that your ValveDriverImpl component has two static errors. Firstly, it calls hal.setParameters(…) on its required port, which has been removed from the ValveHAL port. Secondly, it calls hal.move(…) on ValveHAL with the old signature and return type.

There is an additional problem to be addressed: in its current implementation, ValveDriverImpl does not report any errors resulting from a call to move the valve. This is because the previous version of the ValveHAL port assumed that valve movements always succeeded. In the new version of ValveHAL this is no longer the case, as the move(…) function now returns a boolean value to indicate whether the move request succeeded or not depending on the valve parameters it received.

To implement these changes in the ValveDriverImpl component, we will modify its state machine to:

  1. Store the valve parameters it receives from its client (via the setup(…) function), and pass them as parameters on every call to move(…).
  2. Handle the case where the move(…) call can fail, either because the valve parameters are incorrect, or for some other reason, and report these failures on to its client.

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 ValveParameters to store these parameter values when it receives them.

Note

If a variable is declared to be of some type T that does not have an instance of Default, then the variable declaration must either assign an initial value as part of its declaration, or it can be declared as being of type Slot<T>, which means that the verification will check whether the variable is being accessed correctly or not. See variable declaration for further details.

ValveParameters is an external type. By default, this means that it is not verifiable or defaultable. We can specify that a custom external type is defaultable either by labelling it with the @derive attribute, or by declaring an instance of Default. For the purposes of this lesson, we will assume that ValveParameters is not defaultable. 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 valveParameters : 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.

Note

The type Slot<T> can be used to enable some verification even on non-verified types, such as external types. In particular, if a variable is declared to be of type Slot<T>, then the verification will instead check that the slot is only read when a value has been stored in it. It can therefore be used to check that a non-verified type is accessed correctly by the program, even if the actual value is not available.

During verification, Coco stores whether variables of type Slot<T> hold a valid value or not, without knowing or storing the actual value itself. These variables can be set to being valid or invalid via the static constants .Valid and .Invalid respectively. In the generated code, Slot<T> is replaced by T. By default, all instances of Slot<T> are invalid unless specified otherwise. The verification will find any attempts to read or load an invalid value, and provide a counterexample to highlight the error. See Slot for further details.

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

    var valveParameters : Slot<ValveParameters>

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

      client.setup(settings : ValveParameters) = {
        setNextState(Ready);
        return 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(target : ValveHAL.Moves) {
      entry() = hal.move(target)

      var shutdown : Bool

      unused() = {
        shutdown = true;
      }

      periodic(milliseconds(500)) = if (!hal.isMoving()) setNextState(if (shutdown) Terminated else Ready)

      exit() = {
        client.endOfMovement(match (target) {
          .Open => .Opened,
          .Close => .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(target : ValveHAL.Moves) : Nil = {
        if (hal.move(target, valveParameters)) setNextState(Moving(target)) else client.endOfMovement(.Error)
      }

This function calls hal.move(…). If it is accepted, it changes state to Moving; otherwise it sends the endOfMovement(Status.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(.Open)
      client.close() = perhapsMove(.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 {
    var valveParameters : Slot<ValveParameters>

    state Initial {
      client.setup(settings : ValveParameters) = {
        setNextState(Ready);
        return true;
      }
    }

    // Valve ready to move
    state Ready {
      client.open() = perhapsMove(.Open)
      client.close() = perhapsMove(.Close)
      function perhapsMove(target : ValveHAL.Moves) : Nil = {
        if (hal.move(target, valveParameters)) setNextState(Moving(target)) else client.endOfMovement(.Error)
      }
    }

    // Asynchronously execute the synchronous valve movement
    state Moving(target : ValveHAL.Moves) {
      var shutdown : Bool

      unused() = {
        shutdown = true;
      }

      periodic(milliseconds(500)) = if (!hal.isMoving()) setNextState(if (shutdown) Terminated else Ready)

      exit() = {
        client.endOfMovement(match (target) {
          .Open => .Opened,
          .Close => .Closed,
        });
      }
    }
  }

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

Note

Coco is warning us that the variable valveParameters never has a value assigned to it and the parameter to the setup(…) is never used. We are choosing to ignore this in order for the verification to discover that valveParameters had no valid value assigned to it.

Verifying your Changes (Example_09B)

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

User User ValveDriverImpl ValveDriverImpl hal hal setup(<unavailable>) setup(<unavailable>) return true return true open() open() Initial Ready Ready Ready Ready An assertion failed: value was not written to before being loaded. Exception counterexample

Analysis

The counterexample shows the setup(…) function being called on ValveDriverImpl, followed by a call to open(). The open() call generates an error because it is passing valveParameters as an input parameter to the hal.move(…) call without ever having written a value to it. Looking at the state machine, we can indeed see that when the setup(…) function is executed in the Initial state, its argument is not assigned to valveParameters:

      client.setup(settings : ValveParameters) = {
        setNextState(Ready);
        return true;
      }

Therefore, valveParameters does not have a valid value at the point where ValveDriverImpl is attempting to read it when it calls hal.move(…) with the value of valveParameters as its argument. Coco did try to tell us this with the warning that valveParameters is read but never written to!

Assigning a Value to valveParameters

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

      client.setup(settings : ValveParameters) = {
        valveParameters = settings;
        setNextState(Ready);
        return true;
      }

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

Verifying your Changes (Example_09C)

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

client client User User ValveDriverImpl ValveDriverImpl hal hal setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) [nondet ] ValidParameters [nondet ] ValidParameters return true return true return true return true open() open() open() open() move(Moves.Open… <unavailable>) move(Moves.Open, <unavailable>) [nondet ] MoveFailedToStart [nondet ] MoveFailedToStart return false return false endOfMovement(Status.Error) endOfMovement(Status.Error) Initial Initial Ready Initial Ready Ready Ready Ready Moving(Status.Opened) Ready Ready Ready Ready Ready Ready Ready The last event performed by the component was not allowed by the provided port, which expected one of: return nil Trace counterexample

Analysis

The ValveDriverImpl component was called to open() the valve, and in turn calls hal.move(…) on its required port. The hal.move(…) call was rejected for some reason, and returns false. As a result, the ValveDriverImpl synchronously sends the endOfMovement(…) signal, which is not allowed by its provided port, ValveDriver.

Examining ValveDriver, we see the following two issues:

  1. It specifies that the endOfMovement(…) signal must occur after the open() function returns.
  2. .Error is not one of the values allowed in the signal.

To solve this, we need to modify ValveDriver so that both the open() and close() transitions allow the ValveDriverImpl to signal the failure before the functions return to the caller.

Step 2: Modifying ValveDriver

Modify the open() and close() transitions in Ready as follows:

    state Ready {
      open() = nondet {
        OpenMoveStarted: setNextState(Moving(.Opened)),
        OpenMoveFailedToStart: endOfMovement(.Error),
      }
      close() = nondet {
        CloseMoveStarted: setNextState(Moving(.Closed)),
        CloseMoveFailedToStart: endOfMovement(.Error),
      }
    }

Both transitions now make a nondeterministic choice between starting the movement and changing state to Moving, or synchronously signalling a failure and remaining in the Ready state.

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

Verifying your Changes (Example_09D)

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

See also

See the description of slots for further details and examples. Another more complex example using slots can also be found in the verification section.