Next: , Previous: , Up: Defining and Managing Component States   [Contents]


2.3.4 Polling for State

Sometimes a component that sets another component’s state needs to poll (query) for the current state. The below shows how to enable polling through a “getter” function.

In order to support and verify the getState reply below, we have to declare the state enumeration publicly in the interface definition, reference the interface enumeration in the component (not declare it), and replicate at least some of the component’s state behaviour in the interface behaviour.

The interface code below uses the event-first pattern to define its internal behaviour. The rule is, as before, that all states or guards must be handled by the defined behaviour. The getState handler below does the same thing in every state, thus it does not use [] boolean checks.

Exercise: simplify the below interface’s code so that none of the on-event handlers tests the state, instead each on-event handler does the same thing in all states. Answers are at the end of this section.

interface ILED {
  enum State { Off, On };
  in void turnOn();
  in void turnOff();
  in State getState();

  behaviour {
    State state = State.Off;
    on turnOn: {
      [state.Off] state = State.On;
      [state.On] {}
    }
    on turnOff: {
      [state.Off] {}
      [state.On] state = State.Off;
    }
    on getState: { reply(state); }
  }
}

component LED {
  provides ILED iLed;

  behaviour {
    ILED.State state = ILED.State.Off;
    [state.Off] {
      on iLed.turnOn(): state = ILED.State.On;
      on iLed.turnOff(): {}
      on iLed.getState(): reply(state);
    }
    [state.On] {
      on iLed.turnOn(): {}
      on iLed.turnOff(): state = ILED.State.Off;
      on iLed.getState(): reply(state);
    }
  }
}

As noted earlier and shown here again, for state-leading-only logic, every input event (“in” function) must be handled either explicitly or implicitly inside every [state] block, else your model will have unhandled-event verification errors (compliance).

Exercise answers – the first one mixes event-leading and state-leading logic:

component LED {
  provides ILED iLed;

  behaviour {
    ILED.State state = ILED.State.Off;
    // mix event-leading and state-leading
    on iLed.getState(): reply(state);
    [state.Off] {
      on iLed.turnOn(): state = ILED.State.On;
      on iLed.turnOff(): {}
    }
    [state.On] {
      on iLed.turnOn(): {}
      on iLed.turnOff(): state = ILED.State.Off;
    }
  }
}

Exercise second answer, with minimal logic:

component LED {
  provides ILED iLed;

  behaviour {
    ILED.State state = ILED.State.Off;
    // minimal model of equivalent logic
    on iLed.turnOn(): state = ILED.State.On;
    on iLed.turnOff(): state = ILED.State.Off;
    on iLed.getState(): reply(state);
  }
}

Next: , Previous: , Up: Defining and Managing Component States   [Contents]