10.4.3.3 invariant

Invariants are part of Dezyne language since version 2.19.0. The invariant statement expresses a property on states variable and/or shared state from ports that should hold. It resembles an assert statement known for other languages: whenever the expression of the invariant does not hold, i.e. evaluates to false, an "invariant" error is reported. Invariant statements only have an effect during simulation and verification.

invariant   ::= "invariant" bool-expression

Invariants can be used in the behavior of an interface or component. All invariants are evaluated before processing a trigger, and for a component we have the additional condition that the queue must be empty. For a component, when the queue is not empty, evaluating invariants is skipped; the trigger is processed first.

Note that an invariant statement can be guarded, for example:

[state.Enabled] invariant device.state.On;

Above invariant example for a component expresses that whenever the component is in its Enabled state, the device should be in the On state.

Note that invariants and on statements can be combined:

[state.Enabled]
{
  invariant device.state.On;
  on ctrl.disable (): {device.switch_off; state = state.Disabled;}
}

Note that a guarded invariant can be rewritten to an unguarded invariant using the boolean "implies" (=>) operator. So, for instance, the example could equally well expressed by:

invariant state.Enabled => device.state.On;