//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[tools-cif2cif-chapter-elim-monitors]]
== Eliminate monitors

indexterm:[CIF to CIF transformer,eliminate monitors]
indexterm:[eliminate monitors]
indexterm:[monitor,eliminate]
This CIF to CIF transformation eliminates monitor events.

indexterm:[eliminate monitors,supported specifications]

=== Supported specifications

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

* Component definitions and component instantiations are not supported.

indexterm:[eliminate monitors,preprocessing]

=== 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 <<tools-cif2cif-chapter-index,CIF to CIF transformations>> (in the given order):

* <<tools-cif2cif-chapter-elim-comp-def-inst>>

indexterm:[eliminate monitors,implementation]

=== 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`:

[source, cif]
----
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:

[source, cif]
----
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

indexterm:[eliminate monitors,size considerations]

=== Size considerations

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

indexterm:[eliminate monitors,optimality]

=== 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 <<tools-cif2cif-chapter-simplify-values>>.

=== Annotations

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