Lesson 8: Introducing Timers

The ValveHAL port currently models a hardware abstraction layer on which the move(…) function is synchronous; that is, when the function returns, the valve movement has finished. A more realistic interface to a motorised valve would be one in which the hardware command to start the valve movement would execute instantly, and the valve movement would continue in parallel without blocking the caller. On completing its movement, it would simply stop without sending any interrupts or other signals to the calling software. To establish when the valve movement has finished, the ValveHAL interface would need to be polled.

We are going to change ValveHAL to reflect the behaviour of a valve which works asynchronously as described above, and then use verification to drive the resulting changes necessary to any of the other ports or components.

In this lesson, we will be introducing the following new Coco constructs:

Step 1: Modifying ValveHAL

We start by modifying ValveHAL so that the move(…) function returns immediately while the hardware movement takes place in parallel. Also, we will add a query function so that the ValveHAL can be polled to determine when the valve has stopped moving.

Following the usual Coco workflow, we start by extending the provided port ( ValveHAL) of ValveHALBase first, and then use the verification to determine what other changes we need to make as a consequence.

We will make the following changes to the ValveHAL port:

  1. The move(…) command will return immediately to its client.
  2. New states will be added to discriminate between the valve moving versus being stationary.
  3. A spontaneous transition will be used to model the end of the valve movement.
  4. A query function will be added so that the client can poll the valve to determine when it has stopped moving.

Modify your ValveHAL port to look like the following:

external type ValveParameters

port ValveHAL {
  enum Moves {
    case Open
    case Close
  }

  function setParameters(setup : ValveParameters) : Bool
  function move(target : Moves) : Nil
  function isMoving() : Bool

  machine {
    state Initial {
      // Accept or reject valve parameters and remember result
      setParameters(_) = nondet {
        {
          setNextState(Ready);
          return true;
        },
        {
          return false;
        },
      }
    }

    state Ready {
      move(_) = setNextState(Moving)
      isMoving() = false
    }

    state Moving {
      MoveFinished: spontaneous = setNextState(Ready)
      isMoving() = true
    }
  }
}

We have not introduced any new language features in this example.

The Coco for this port is in Example_08B/src/ValveHAL.coco.

Verifying your Changes (Example_08B)

The Coco Platform has found verification errors in assertions for both the ValveDriverImpl and SimulatorImpl components, and also reports a warning for the ValveHAL port.

Following the usual approach after changing a port of making any necessary changes to component providing the port before those requiring it, we will analyse the error found in SimulatorImpl. Before we do that, however, we need to investigate the warning in ValveHAL.

Analysis of Warning in ValveHAL

The Coco Platform gives the following counterexample for the warning in ValveHAL:

instance1 instance1 User User instance2 instance2 setParameters(<unavailable>) setParameters(<unavailable>) setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] setN…extState(Ready) [nondet 0] setNextState(Ready) [nondet 0] setN…extState(Ready) [nondet 0] setNextState(Ready) return true return true return true return true move(Moves.Open) move(Moves.Open) move(Moves.Open) move(Moves.Open) return nil return nil return nil return nil [spontaneous] MoveFinished [spontaneous] MoveFinished move(Moves.Open) move(Moves.Open) move(Moves.Open) move(Moves.Open) return nil return nil illegal illegal Initial Initial Initial Initial Ready Ready Ready Ready Moving Moving Moving Moving Ready Moving Moving Moving The last function call was ambiguously illegal: instance1 declared the event as legal instance2 declared the event as illegal Ambiguously illegal counterexample

The warning is for the assertion that checks whether ValveHAL is potentially unusable as an interface to its clients. This arises when a port is specified in such a way that a client using it might not be able to determine whether a call on that port is legal or illegal. For further details about this verification check, see the verification section for ports in the Coco Language Reference.

The counterexample above shows two execution scenarios, both with the same sequence of visible events between ValveHAL and its client, where in one case the function call move(…) is allowed, and in the other case it is illegal. This occurs because when the second move(…) function is called, the port can either be in the state Moving, where move(…) is illegal, or it could have performed the spontaneous transition and changed to the state Ready where move(…) is allowed. The Coco Platform is warning us that because Moving is unstable, the client might not be sure whether or not move(…) can be called.

When this verification check fails, it is marked as a warning rather than an error, because this characteristic does not always mean that the port is in fact unusable. If we look more closely at ValveHAL, we can see that a client can call another function isMoving() to determine which state ValveHAL is in, and avoid accidentally calling move(…) when it is illegal to do so. If isMoving() returns false, then the client knows that ValveHAL is in Ready (which is stable), and it can safely make another move(…) call.

This warning can be safely ignored in this case and can be suppressed by adding the following attribute to the state machine declaration:

  @ignoreWarning(Warning.Usability)

Analysis of SimulatorImpl error

The Coco Platform detects that the SimulatorImpl component fails to implement its provided port correctly, and produces the following counterexample:

client client User User SimulatorImpl SimulatorImpl setParameters(<unavailable>) setParameters(<unavailable>) setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] setN…extState(Ready) [nondet 0] setNextState(Ready) return true return true return true return true isMoving() isMoving() isMoving() isMoving() illegal illegal Initial Main Initial Main Ready Ready Main Ready Main Main The provided port expected the last function call not to be illegal. Trace counterexample

The verification error is caused by the fact that the query function isMoving() has not yet been implemented in SimulatorImpl.

Step 2: Extending SimulatorImpl

The current version of the SimulatorImpl implements a synchronous move(…) function call by simply sleeping for 10 seconds using the C++ standard library function std::this_thread::sleep_for. However, this does not allow it to be polled while simulating the valve movement, and blocks the component calling it. In order to be able to implement a query function, and a non-blocking version of the move(…) function, the SimulatorImpl must remain responsive to its clients while the valve movement is being simulated.

The solution we are going to implement is to use one of the timers built into Coco. The changes we will make are to:

  1. Introduce separate states to reflect when the valve is moving as opposed to stationary.
  2. Simulate asynchronous valve movement, which stops after 10 seconds, in such a way that the client is not blocked while the valve is moving.
  3. Implement the query function.
  4. Delete the references to the C++ standard library function std::this_thread::sleep_for.

We will be using Coco timers to implement these changes.

Note

Coco implements timer transitions that specify the behaviour resulting from a timer, and are only permitted in component state machines. There are two types of timer expiry events:

  • after(t : Duration) will occur once after the specified duration has passed, providing that the state machine remains in the current state.
  • periodic(t : Duration) will occur repeatedly each time the specified duration has passed while the state machine remains in the current state.

When a timer expires, the corresponding timer transition is executed. Timer transitions cannot be guarded, and multiple timer transitions can be specified in a state. However, timer durations are unverifiable types, which means that the verification will not respect the order in which timer events would occur at runtime.

Further details and examples of timers can be found in the Timer Transition section in the Coco Language Reference.

Adding New States

The current SimulatorImpl component is a stateless implementation as follows:

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

  machine {
    var isSetup : Bool

    if (!isSetup) client.setParameters(_) = isSetup = true
    if (isSetup) client.move(_) = sleep(seconds(10))
  }
}

The new behaviour is more complex than the previous behaviour, and so we will express the new behaviour by adding new states.

We start by declaring the following new state Initial, which describes the state of ValveHALBase before any valve parameters have been set:

    state Initial {
      client.setParameters(_) = {
        setNextState(Ready);
        return true;
      }
    }

In the SimulatorImpl we always assume that the provided parameters are correct. For simplicity, there is no logic provided in the Initial state to verify or reject them.

We then add two new states called Ready and Moving. The state machine is in Ready whenever the valve is supposed to be stationary, and Moving when valve movement is being simulated. We declare Ready as follows:

    state Ready {
      client.move(_) = setNextState(Moving)
      client.isMoving() = false
    }

In this state, the function move(…) is allowed, and changes state to Moving. We declare the new Moving state as follows:

    state Moving {
      after(seconds(10)) = setNextState(Ready)
    }

The timer transition has a timer expiry event with a duration of 10 seconds. When this state is entered, a timer is started. When the timer expires, the state machine changes state to Ready, which simulates the end of a valve movement taking 10 seconds.

Adding the Query Function

The new query function isMoving() specified in Step 1 returns true when the SimulatorImpl is in the Moving state, and false when it is in the Ready state.

Add the necessary transitions to Ready and Moving to implement this behavour. Your modified state machine should look as follows:

  machine {
    state Initial {
      client.setParameters(_) = {
        setNextState(Ready);
        return true;
      }
    }

    state Ready {
      client.move(_) = setNextState(Moving)
      client.isMoving() = false
    }

    state Moving {
      after(seconds(10)) = setNextState(Ready)
      client.isMoving() = true
    }
  }

We now have two distinct states covering the cases where the valve is stationary versus when it is moving. The Moving state specifies a timer transition for a timer with a duration of 10 seconds. When the timer expiry event occurs, it changes to state Ready. The query function returns true in Moving, and false in Ready, thereby allowing its client to poll it to establish when the movement is finished.

Delete the references to std::this_thread::sleep_for

In the previous versions of SimulatorImpl, we used a sleep function from the C++ Standard Library, called std::this_thread::sleep_for, and provided the mapping from Coco to the C++ as it would appear in the generated code. In this version, we are using the built-in timers provided by Coco; therefore, we can remove the references to the sleep function, and delete the related language mappings.

Delete the following lines:

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

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

Verifying your Changes (Example_08C)

The modified SimulatorImpl component now verifies correctly.

However, the verification detects that the ValveDriverImpl does not use its required port correctly, and produces the following counterexample:

User User ValveDriverImpl ValveDriverImpl hal hal setup(<unavailable>) setup(<unavailable>) setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] setN…extState(Ready) [nondet 0] setNextState(Ready) return true return true return true return true open() open() return nil return nil move(Moves.Open) move(Moves.Open) return nil return nil endOfMovement(Status.Opened) endOfMovement(Status.Opened) open() open() return nil return nil move(Moves.Open) move(Moves.Open) Initial Initial Initial Initial Initial Ready Ready Ready Ready Moving(Moves.Open) Moving(Moves.Open) Moving(Moves.Open) Moving Moving(Moves.Open) Moving Ready Moving(Moves.Open) Moving(Moves.Open) The last function call was illegal; it could not be handled by hal because no transition matched. Illegal function call counterexample

Analysis

After the initialisation sequence, we see that open() or close() was called on ValveDriverImpl, which in turn called move(…) on its required port ValveHAL leaving it in the Moving state. ValveDriverImpl, as yet unmodified, assumes the return from move(…) means that the movement is finished, and therefore sends an endOfMovement(…) signal to its client. The client responds by calling open() or close() on ValveDriverImpl, which in turn calls move(…) on ValveHAL. This is not allowed because ValveHAL is still in the Moving state from the earlier open() or close() call.

To fix this error, we need to modify ValveDriverImpl so that it does not assume the valve movement is finished when the move(…) function returns, and instead it polls the valve to find out when it has finished its movement.

Note

When the verification finds an error, the shortest counterexample that results in the error is displayed. In this example, the same error occurs whether the client calls open() or close(), and since their respective counterexamples are the same length, the one displayed may vary between releases.

Step 3: Modifying ValveDriverImpl to Poll ValveHAL

We must make the following changes to ValveDriverImpl:

  1. Change state Moving from an execution state to an event state.
  2. Define a new entry function from which to call move(…).
  3. Add a periodic timer transition to poll the ValveHAL every 500 milliseconds to see if the movement has finished.
  4. Add a new exit function which sends the endOfMovement(…) signal to its client.

Changing the Moving State

We need to change the Moving state from being an execution state to an event state.

This simply requires removing the keyword execution from the state declaration so that it becomes:

    state Moving(target : ValveHAL.Moves) {

Declaring a New Entry Function

Add the following declaration to state Moving:

      entry() = hal.move(target)

This declares an entry function, and calls move(…) each time the Moving state is entered.

Adding a Periodic Timer

Add the following to state Moving:

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

In Step 2, we made use of the one-time after timer expiry event in SimulatorImpl. In ValveDriverImpl, we are making use of the repeating periodic timer expiry event to drive the polling loop. On entry to Moving, the timer is activated for as long as ValveDriverImpl remains in the Moving state, and each time the specified time interval has passed, its handler is executed. When the handler has finished, if the state remains unchanged, the timer is automatically set to the same time period again. This continues until the state is exited.

Declaring a new exit function

Declare a new exit function in the Moving state to send the endOfMovement(…) signal as follows:

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

Your modified ValveDriverImpl component should look like the following:

import unqualified ValveDriver
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveDriverImpl {
  val client : Provided<ValveDriver>
  val hal : Required<ValveHAL>

  machine {
    state Initial {
      client.setup(settings : ValveParameters) = if (hal.setParameters(settings)) {
        setNextState(Ready);
        return true;
      } else {
        return false;
      }
    }

    // Valve ready to move
    state Ready {
      client.open() = setNextState(Moving(.Open))
      client.close() = setNextState(Moving(.Close))
    }

    // Asynchronously execute the synchronous valve movement
    state Moving(target : ValveHAL.Moves) {
      entry() = hal.move(target)

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

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

The complete Coco for this component is in Example_08D/src/ValveDriverImpl.coco.

Verifying your Changes (Example_08D)

When running the verification, the Coco Platform reports that ValveDriverImpl fails to implement its provided port, 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 setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] setN…extState(Ready) [nondet 0] setNextState(Ready) return true return true return true return true return true return true close() close() close() close() move(Moves.Close) move(Moves.Close) return nil return nil return nil return nil return nil return nil [periodic] if (…extState(Ready) [periodic] if (!hal.isMovin…NextState(Ready) isMoving() isMoving() return true return true Initial Initial Initial Initial Initial Ready Initial Initial Ready Ready Ready Ready Ready Moving(Status.Closed) Moving(Moves.Close) Moving(Moves.Close) Moving Moving(Moves.Close) Moving Moving(Status.Closed) Moving(Moves.Close) Moving(Moves.Close) Moving(Moves.Close) Moving Moving(Moves.Close) Moving LOOP The specification expected the component to perform one of the following events: endOfMovement(Status.Error) endOfMovement(Status.Closed) but the component can perform an unbounded sequence of behaviour without sending a signal. Missing signal counterexample

Analysis

The counterexample shows that ValveDriverImpl fails to send any of the signals specified by its provided port, because it can end up getting stuck in a loop calling ValveHAL to query the valve’s status on every timer expiry event. We can see this by looking at the Moving state in ValveDriverImpl:

    state Moving(target : ValveHAL.Moves) {
      entry() = hal.move(target)

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

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

In state Moving, ValveDriverImpl is periodically polling ValveHAL to check whether the valve movement has finished. If it has, it sends an endOfMovement(…) signal, and changes to the Ready state. Otherwise, it remains in the same state, and continues polling ValveHAL without sending any signals.

The counterexample is highlighting an example where ValveDriverImpl can continue to poll ValveHAL, and never receive false in return to indicate that the movement has finished. To understand how this problem arises, we need look at the Moving state that ValveHAL is in when the error occurs:

    state Moving {
      MoveFinished: spontaneous = setNextState(Ready)
      isMoving() = true
    }

In state Moving, ValveHAL can either accept an isMoving() call (and return true), or it can nondeterministically decide to perform a spontaneous transition resulting in a state change to Ready, indicating that the move has finished. Although ValveHAL can choose to perform this spontaneous transition, it is not obliged to do so, and can choose to continue receiving the isMoving() call in the Moving state instead. Therefore, the occurrence of the spontaneous transition is not guaranteed. This means that ValveHAL does not guarantee that the valve will stop moving, which is an assumption that its client ValveHALBase is depending on to correctly implement its provided port.

To fix this error, we will extend our ValveHAL port to specify that the spontaneous transition will eventually occur, reflecting our intended assumption that the valve will eventually stop moving.

Step 4: Fixing ValveHAL to Eventually Stop Moving

The verification error found by the Coco Platform above is caused by the fact that the ValveHAL port does not model the assumption that the valve will eventually stop moving, whereas its client ValveDriverImpl depends upon it doing so.

We can fix this error by labelling the spontaneous transition in the Moving state in ValveHAL with the @eventually attribute as follows:

    state Moving {
      @eventually
      MoveFinished: spontaneous = setNextState(Ready)
      isMoving() = true
    }

This change means that ValveHAL now specifies that the valve is guaranteed to eventually stop moving. It also places a requirement on the component implementing this port that this eventually constraint is satisfied, which is checked by the Coco Platform as part of the verification performed. See the relevant verification section in the Coco Language Reference for further details.

Note

The @eventually attribute can be used to label certain transitions, for example spontaneous transitions as illustrated above, and branches in a port state machine to specify that they will eventually occur. When a spontaneous transition is labelled with the @eventually attribute, if the spontaneous transition is enabled infinitely often, then it will eventually be executed. Further details and examples can be found in the Eventually Attribute section of the Coco Language Reference. This is an ideal point in the tutorial to read through this section!

The modified Coco for this port is in Example_09A/src/ValveHAL.coco.

Step 5: Extending ValveDriverImpl to defer termination

In Step 3 above, the Moving state in the ValveDriverImpl component was changed from an execution state to an event state. This means that this component can now be called to terminate while the valve is moving. To prevent this, we can use the same approach used in the ValveControllerImpl component in Lesson 7: Deferring Termination, where termination is deferred while the valve is moving, and the component immediately terminates upon completion of the movement.

To implement this, extend the Moving state in ValveDriverImpl 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 modified Coco for this component is in Example_09A/src/ValveDriverImpl.coco.

Verifying your Changes (Example_09A)

All of our ports and components verify without errors.