Note

You are not reading the most recent version of this documentation. 1.5.1 is the latest version available.

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:

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
  function isMoving() : Bool

  machine M {
    state Initial {
      /// accept or reject valve parameters and return result
      setParameters(_ : ValveParameters) = nondet {
        {
          setNextState(Ready.Idle);
          true
        },
        false,
      }
    }

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

      state Moving {
        @represents("end of movement")
        spontaneous = setNextState(Idle)
        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:

Ambiguously illegal counterexampleinstance1Userinstance2setParameters(<unavailable>)setParameters(<unavailable>)[nondet] τ (index 0)[nondet] τ (index 0)return truereturn truemove(Cmd.Open)move(Cmd.Open)return nilreturn nil[spontaneous] τ...end of movementmove(Cmd.Open)move(Cmd.Open)return nilillegal The last function call was ambiguously illegal: instance1 declared the event as legal instance2 declared the event as illegal

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 Ready.Moving, where move(…) is illegal, or it could have performed the spontaneous transition and changed to the state Ready.Idle where move(…) is allowed. The Coco Platform is warning us that because Ready.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.Idle (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:

Trace counterexampleclientUserSimulatorImplsetParameters(<unavailable>)setParameters(<unavailable>)[nondet] τ (index 0)return truereturn trueisMoving()isMoving()illegal The provided port expected the last function call not to be illegal.

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 M {
    var parmsSet : Bool
    if (!parmsSet) client.setParameters(_ : ValveHAL.ValveParameters) = parmsSet = true
    if (parmsSet) client.move(_ : ValveHAL.Cmd) = chronoSleep(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(_ : ValveHAL.ValveParameters) = {
        setNextState(Ready.Idle);
        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 another new state called Ready with two child states, Idle and Moving. The state machine is in Idle whenever the valve is supposed to be stationary, and Moving when valve movement is being simulated. We declare Idle as follows:

      state Idle {
        client.move(_ : ValveHAL.Cmd) = 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(Idle)
      }

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 Idle, 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 Idle state.

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

  machine M {
    state Initial {
      client.setParameters(_ : ValveHAL.ValveParameters) = {
        setNextState(Ready.Idle);
        true
      }
    }
    state Ready {
      state Idle {
        client.move(_ : ValveHAL.Cmd) = setNextState(Moving)
        client.isMoving() = false
      }

      state Moving {
        after(seconds(10)) = setNextState(Idle)
        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 Idle. The query function returns true in Moving, and false in Idle, 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 chronoSleep(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:

Illegal function call counterexampleUserValveDriverImplhalsetup(<unavailable>)setParameters(<unavailable>)[nondet] τ (index 0)return truereturn trueopen()return nilmove(Cmd.Open)return nilendOfMovement(V...lveStatus.Open)open()return nilmove(Cmd.Open) The last function call was illegal; it could not be handled by hal because no transition matched.

Analysis

After the initialisation sequence, we see that open() or closed() was called on ValveDriverImpl, which in turn called move(…) on its required port ValveHAL leaving it in the Ready.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 Ready.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(cmd : ValveHAL.Cmd) {

Declaring a New Entry Function

Add the following declaration to state Moving:

      entry() = hal.move(cmd)

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 (cmd) {
          ValveHAL.Cmd.Open => ValveDriver.ValveStatus.Open,
          ValveHAL.Cmd.Close => ValveDriver.ValveStatus.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 M {
    client.terminate() = setNextState(Terminated)

    state Initial {
      client.setup(vParms : ValveHAL.ValveParameters) = if (hal.setParameters(vParms)) {
        setNextState(Ready);
        true
      } else false
    }
    /// Valve ready to move
    state Ready {
      client.open() = setNextState(Moving(ValveHAL.Cmd.Open))
      client.close() = setNextState(Moving(ValveHAL.Cmd.Close))
    }
    /// Asynchronously execute the synchronous valve movement
    state Moving(cmd : ValveHAL.Cmd) {
      entry() = hal.move(cmd)

      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 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:

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:

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

      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,
        });
      }

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.

Note

Although ValveDriverImpl is stuck in state Moving going round this cycle with ValveHAL, it remains responsive to client calls, because it is still able to receive function calls from its client in this state. In this particular case, it can receive the function call terminate() from its client, which would execute the matching enabled transition declared in Main, and cause ValveHALBase to change state to Terminated.

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 {
        @represents("end of movement")
        spontaneous = setNextState(Idle)
        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 Idle 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 {
        @represents("end of movement")
        @eventually
        spontaneous = setNextState(Idle)
        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_08E/src/ValveHAL.coco.

Verifying your Changes (Example_08E)

When we rerun the verification, the Coco Platform reports that ValveDriverImpl still fails to implement its provided port correctly, with the following counterexample:

Trace counterexampleclientUserValveDriverImplhalsetup(<unavailable>)setup(<unavailable>)[nondet] τ Para...eters are validsetParameters(<unavailable>)[nondet] τ (index 0)return truereturn truereturn trueclose()close()move(Cmd.Close)return nilreturn nilreturn nilterminate()terminate()endOfMovement(V...eStatus.Closed) The last event performed by the component was not allowed by the provided port, which expected one of: return nil

Analysis

Examining the counterexample, we see that after open() or close() is called on ValveDriverImpl, it calls move(…) on ValveHAL, and changes to the Moving state. In Moving, ValveDriverImpl receives a terminate() call from its client causing a state change from Moving to Terminated. This means that the exit function of Moving is executed, which sends the endOfMovement(…) signal to its client. This is not allowed according to its provided port ValveHAL, which requires the terminate() function to return immediately without sending signals.

There is no requirement for ValveDriverImpl to allow terminate() calls while the valve is moving, and we can fix this issue by modifying both ValveDriver and ValveDriverImpl to prohibit calls to terminate() in this case.

ValveControllerImpl, the only client of ValveDriverImpl, already makes this assumption, and therefore changing ValveDriver should not affect it.

Step 4: Modifying ValveDriver and ValveDriverImpl

To avoid the error reported above, we will change both ValveDriver and ValveDriverImpl to prohibit calls to terminate() while the valve is moving.

Modifying ValveDriver

Add the following transition to state Moving:

      terminate() = illegal

When in Moving state, this overrides the transition defined for terminate() in Main, and specifies that calling terminate() in state Moving is illegal.

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

Modifying ValveDriverImpl

To make the corresponding change to ValveDriverImpl, add the following transition to Moving:

      client.terminate() = illegal

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

Verifying your Changes (Example_09A)

All of our ports and components verify without errors.