Lesson 7: Deferring Termination

Coco supports automatic termination of systems. In the generated code, each component stores the number of clients connected to any of its provided ports. When this reaches zero, a call on unused() is initiated on the component resulting in a call on setNextState(Terminated), thereby automatically shutting down the component. Termination cascades through the system from top to bottom due to the following actions performed upon entry to the Terminated state:

  1. Unsubscribe from all of its required ports;
  2. Unregister from all of its required ports, which means that they will recursively terminate.
  3. Call purge to delete all of the signals from the its queue.

By default, a component state machine can be called to terminate at any time when it is idle, which results in the component immediately transitioning to the Terminated state. This is equivalent to explicitly declaring an unused transition that results in the execution of setNextState(Terminated) at the top level of state Main. See unused transitions, and automatic termination for further details.

In some cases, it may not be desirable to allow the component to immediately terminate in every state, but instead specify that a component can defer termination after it has completed a series of actions, for example to ensure that the overall system is in a safe state before it is shutdown. This can be achieved by explicitly declaring unused() transitions in a component state machine, which specifies the conditions under which the state machine eventually terminates.

Note

When an unused() transition has fired, the component will not receive any further function calls on its provided ports, reflecting the fact that it no longer has any clients. When unused() transitions are explicitly declared in a state machine, then the state machine must eventually transition the Terminated state. The verification checks that this is indeed the case, and gives an error otherwise.

The objective of this lesson is to explore Coco’s automatic termination, and how termination can be deferred by explicitly declaring unused() transitions in a component state machine. We will use the ValveControllerImpl component for this, which currently allows termination to be called in all states, and extend it such that if the valve is moving, then termination will be deferred until it has finished moving.

Step 1: Declaring an unused() transition

The first step is to identify the states in the ValveControllerImpl component where the valve is moving, and therefore any calls to terminate must be deferred until it has finished. There is one such state called Moving, which is currently declared as follows:

    state Moving {
      driver.endOfMovement(result : ValveDriver.Status) = {
        setNextState(match (result) {
          .Opened => Ready.Opened,
          .Closed => Ready.Closed,
          .Error => Ready.Unknown,
          .Unknown => Ready.Unknown,
          .Moving => abort(),
        });
        client.moveEnded(result);
      }
    }

Extend this Moving state with a local boolean variable called shutdown, and an unused() transition, as follows:

    state Moving {
      var shutdown : Bool

      unused() = {
        shutdown = true;
      }

      driver.endOfMovement(result : ValveDriver.Status) = {
        setNextState(match (result) {
          .Opened => Ready.Opened,
          .Closed => Ready.Closed,
          .Error => Ready.Unknown,
          .Unknown => Ready.Unknown,
          .Moving => abort(),
        });
        client.moveEnded(result);
      }
    }

The variable shutdown captures whether the component has been called to terminate in state Moving. Therefore, when the unused transition is executed, shutdown is assigned the value true to reflect the fact that the component has been called to terminate.

The Coco for this component is in Example_07B/src/ValveControllerImpl.coco.

Verifying your Changes (Example_07B)

The responsive assertion for ValveControllerImpl fails the verification with the following counterexample:

User User ValveControllerImpl ValveControllerImpl driver driver setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) [nondet ] ValidParameters [nondet ] ValidParameters return true return true return true return true close() close() close() close() return nil return nil return nil return nil [unused] shutdown = true [unused] shutdown = true [spontaneous] s….Status.Error,} [spontaneous] status = nondet …r.Status.Error,} [nondet ] MoveSucceeded [nondet ] MoveSucceeded (queued): endOf…(Status.Closed) (queued): endOfMovement(Status.Closed) (dequeued): end…(Status.Closed) (dequeued): endOfMovement(Status.Closed) moveEnded(Status.Closed) moveEnded(Status.Closed) Initial Initial Initial Initial Initial Ready Ready.Unknown Ready Ready.Unknown Ready.Unknown Ready.Unknown Moving(Status.Closed) Moving Moving(Status.Closed) Moving Moving Moving(Status.Closed) Moving(Status.Closed) Moving Ready Ready.Closed Ready.Closed The component was expected to terminate following a call to unused() but has deadlocked and is unable to perform any events. Termination deadlock counterexample

Analysis

The counterexample above illustrates how ValveControllerImpl reaches a state where it deadlocks, and is not able to eventually terminate as required following a call on unused().

Following a successful setup, and a call on open(), ValveControllerImpl is in the state Moving. In this state, unused() is called to terminate the component, which results in shutdown being assigned the value true as expected. However, when it receives the endOfMovement(.Error) signal from its required port driver indicating that the move request failed, ValveControllerImpl sends the corresponding moveEnded(.Error) to its client, and transitions to the state Unknown. In this state, it will not receive any further function calls on its provided ports, reflecting the fact that it no longer has any clients, and it is not able to transition to the Terminated state as required.

Note

The Coco Platform will present the shortest counterexample that leads to an error. When there are several errors with the same path length, the counterexample displayed may vary between releases. In this example, the counterexample displayed may vary between calling open() or close() on the ValveControllerImpl component, or between the move request succeeding or failing on its required port driver. All of these paths lead to the same error described here, and is fixed by the solution we present below.

To fix this, we need to extend ValveControllerImpl so that it transitions directly to the Terminated state from Moving when it receives the signal confirming that the move has finished, and has been called to terminate.

Step 2: Extending ValveControllerImpl to terminate

To ensure that the ValveControllerImpl component eventually terminates when unused() is called while the valve is moving, extend the Move state declaration as follows:

    state Moving {
      var shutdown : Bool

      unused() = {
        shutdown = true;
      }

      driver.endOfMovement(result : ValveDriver.Status) = if (shutdown) {
        setNextState(Terminated)
      } else {
        setNextState(match (result) {
          .Opened => Ready.Opened,
          .Closed => Ready.Closed,
          .Error => Ready.Unknown,
          .Unknown => Ready.Unknown,
          .Moving => abort(),
        });
        client.moveEnded(result);
      }
    }

When ValveControllerImpl receives a driver.endOfMovement(…) signal to indicate the completion of the move, if shutdown is true, then the state machine will transition to Terminated, otherwise it will transition to the corresponding state as previously defined.

The Coco for this component is in Example_08A/src/ValveControllerImpl.coco.

Verifying your changes (Example_08A)

All ports and components verify correctly.