This CIF to CIF transformation eliminates monitor events.
This transformation supports a subset of CIF specifications. The following restrictions apply:
Component definitions and component instantiations are not supported.
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):
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 urgency (no
now), and no updates (no
For instance, for the following locations and edges, for monitor event
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;
l1, monitor event
e is always enabled (no guard implies a
true guard), and thus no additional self loop is needed. In location
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.
f is not a monitor event, and is thus not affected by this transformation.
Since self loop edges may be added by this transformation, the size of the specification may increase.
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.