Eliminate monitors

This CIF to CIF transformation eliminates monitor events.

Supported specifications

This transformation supports a subset of CIF specifications. The following restrictions apply:

  • Component definitions and component instantiations are not supported.

Preprocessing

No preprocessing is currently performed by this CIF to CIF transformation. To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations (in the given order):

Implementation details

For each monitor event in an automaton, additional self loops are added as needed, to make sure the automaton doesn’t disable the monitor event. Furthermore, all monitors are removed from all automata.

The self loop edges created by this transformation have no communication (no !..., no ?...), no urgency (no now), and no updates (no do ...).

For instance, for the following locations and edges, for monitor event e:

location l1:
  edge e goto l2;
  edge f when x = 2 goto l3;

location l2:
  edge e when x = 1 goto l3;
  edge e when x = 2 goto l1;

location l3;

the result after this transformation is:

location l1:
  edge e goto l2;
  edge f when x = 2 goto l3;

location l2:
  edge e when x = 1 goto l3;
  edge e when x = 2 goto l1;
  edge e when not(x = 1 or x = 2);

location l3:
  edge e;

In location l1, monitor event e is always enabled (no guard implies a true guard), and thus no additional self loop is needed. In location l2, event e is only enabled if x has either value 1 or value 2. A self loop is added for all other cases, to ensure the event is always enabled. In location l3, the event is never enabled (no edges, which essentially means guard false). A self loop is added, to ensure the event is always enabled.

Event f is not a monitor event, and is thus not affected by this transformation.

Renaming

n/a

Size considerations

Since self loop edges may be added by this transformation, the size of the specification may increase.

Optimality

For an edge with guard x = 1, a self loop with guard not (x = 1) may be generated by this transformation. The guard could be simplified to x != 1. However, this transformation does not simplify guards. To further simplify the result, apply additional CIF to CIF transformations, such as Simplify values.

Annotations

This transformation does not process, add, or remove any annotations. The newly added edges do have any annotations.