Monitors¶

Coco can be used to model requirements about event driven systems by using monitors. A monitor observes events sen over ports, and uses a state machine to specify the allowed sequences of events. Typically, the overall system requirements should be modelled as a collection of small simple monitors that focus on specific aspects of the requirements.

A monitor declaration introduces a new type with the name specified by the identifier in the declaration, and is similar to that of components.

declarationMonitor¶

[«visibility»] monitor «identifier» {
  «monitor elements»
}

«monitor element» :=
  «field declaration»
  | «variable declaration»
  | «constructor declaration»
  | «state machine declaration»
  | «static constant declaration»

Like component state machines, each field declaration’s type must be one of the following:

Provided<P> or Array<Provided<P>, size>, which declares that the monitor is observing a provided port instance of type P or an array thereof.
Required<P> or Array<Required<P>, size>, which declares that the monitor is observing a required port instance of type P or an array thereof.

A monitor can have at most one constructor. The main use of the constructor is to utilize the function setAllow to select a subset of the events that are sent over that port, in order to allow the monitor to ignore uninteresting events.

Transitions in monitor state machines are like those in ports and components, except that in monitors the events correspond to the observation of an event occuring elsewhere in the system. Monitors are allowed to use the following observed events to observe the behaviour of other parts of the system.

eventStart Event¶

start(«event source».«identifier»(«patterns»))

A start event matches the function or signal named «identifier» received from a port instance matching «event source». If the event is a function, then the «event source» must refer to a provided port, and if the event is a signal, then «event source» must refer to a required port.

The values of the parameters have to also match «patterns», which is a comma-separated list of zero or more patterns that match the observed event’s parameters. «patterns» has to include one pattern for each parameter of the corresponding function or signal. For functions, if the parameter’s type is of the form &out T, then _ must be used as the pattern.

A start event start(e) matches the start of the event e. Specifically:

If e is a function, then start(e) is triggered when e is called, after any locks have been acquired but before the event is actually processed by the recipient state machine.
If e is a signal, then start(e) is triggered when e is taken off the recipient’s queue, after any locks have been acquired.

eventEnd Event¶

end(«event source».«identifier»(«patterns») [, «return pattern»])

«return pattern» := «pattern»

An end event matches the function or signal named «identifier» received from a port instance matching «event source». If the event is a function, then the «event source» must refer to a provided port, and if the event is a signal, then «event source» must refer to a required port.

The values of the parameters have to also match «patterns», which is a comma-separated list of zero or more patterns that match the observed event’s parameters. «patterns» has to include one pattern for each parameter of the corresponding function or signal. If the parameter’s type is of the form &T or T, then _ must be used as the pattern.

For functions, «return pattern» is a pattern that matches the return value of the function call.

An end event end(e) matches the completion of the event e. Specifically:

If e is a function call, then end(e) is triggered when e has completed, after the recipient has fully processed the event (including processing any entry or exit actions), just before any locks would be released by the recipient state machine.
If e is a signal, then end(e) is triggered when e has been fully processed and the next action is about to be started (e.g. the next queue item is about to be dequeued, or the lock is about to be released).

eventSend Event¶

send(«event source».«identifier»(«patterns»))

A send event matches the signal named «identifier» sent from a port instance matching «event source». The «event source» must refer to a provided port.

The values of the parameters have to also match «patterns», which is a comma-separated list of zero or more patterns that match the observed event’s parameters.

A send event matches the sending of a signal event across the port within which it is declared. It corresponds to the moment where the sending component starts to send the event to all registered recipients.

The following is a simple example of a monitor that observes two events across a single port:

@runtime(.MultiThreaded)
monitor OnOff {
  val top : Provided<Top>

  init() = {
    setAllow(top, .on, .off);
  }

  machine {
    state Off {
      start(top.on()) = {}
      end(top.on(), val status) = if (status) setNextState(On)
    }
    state On {
      start(top.off()) = {}
      end(top.off(), _) = setNextState(Off)
    }
  }
}

This monitor observes the function calls on() and off() across the provided port top. The function on() returns true if successful, and false otherwise, whereas the return type of off() is Nil. The setAllow function is called in its constructor, thereby ignoring all other events that are declared in top.

This monitor specifies that only on() can be called first, denoted by the event start(top.on()), and off() can only occur in the event that on() returns true. The return of on() is observed by the event end(top.on(), val result), where result will be bound to the value returned. In the event the value is true, then the state machine moves to the On state, where it specifies that only off() can be called precisely once before returning to the Off state.

The following is an example of a monitor observing function calls and signals across multiple ports:

@runtime(.MultiThreaded)
monitor CheckStatusSignal {
  val top : Provided<Top>
  val bottom : Required<Resource>

  init() = {
    setAllow(top, .checkStatus);
    setAllow(bottom, .isRunning);
  }

  machine {
    state Idle {
      start(top.checkStatus()) = setNextState(WaitForSignal)
    }

    state WaitForSignal {
      var hasReturned : Bool

      end(top.checkStatus(), _) = {
        hasReturned = true;
      }
      start(bottom.isRunning()) = {}
      end(bottom.isRunning()) = if (hasReturned) setNextState(Idle) else setNextState(WaitForReturn)
    }

    state WaitForReturn {
      end(top.checkStatus(), _) = setNextState(Idle)
    }
  }
}

This monitor observes the function checkStatus() across the provided port top and the signal isRunning() across the required port bottom. It specifies that the signal is only allowed after checkStatus() has been called, denoted by start(top.checkStatus()). The signal is allowed before or after this function returns. However, once it has returned, denoted by end(top.checkStatus(), _), then the state machine moves back to the Idle state, where the signal is no longer allowed.

A monitor state machine can declare functions, for example to factor out common code, in the same way as is allowed in port and component state machines. This is illustrated in the following example of a monitor, which specifies a requirement regarding the initialisation process across multiple ports:

@runtime(.MultiThreaded)
monitor InitialisationPhase {
  val top : Provided<Top>
  val resource1 : Provided<Resource>
  val resource2 : Provided<Resource>

  machine {
    state Idle {
      start(top.initialise()) = setNextState(InitialiseResources)
    }

    state InitialiseResources {
      var resource1Result : Optional<Bool>
      var resource2Result : Optional<Bool>

      function process(requesterStatus : &out Optional<Bool>, result : Bool) : Nil = {
        requesterStatus = .Some(result);
        if (resource1Result.hasValue() && resource2Result.hasValue()) {
          setNextState(WaitForReturn(resource1Result.value() && resource2Result.value()))
        }
      }

      if (!resource1Result.hasValue()) start(resource1.initialise()) = nil
      end(resource1.initialise(), val result) = process(&resource1Result, result)

      if (!resource2Result.hasValue()) start(resource2.initialise()) = nil
      end(resource2.initialise(), val result) = process(&resource2Result, result)
    }

    state WaitForReturn(result : Bool) {
      end(top.initialise(), result) = setNextState(Idle)
    }
  }
}

This example observes the initialisation function calls over the provided port and the two required ports: Following a call on the provided port top to initialise, denoted by start(top.initialise()), the requirement is to call initialise() on resource1 and resource2 synchronously before returning to its callee. Only a single call to initialise can be made on each resource, after which top.initialise() must return the logical conjunction of their return values.