CIF 3

Linearize (merge)

This CIF to CIF transformation performs process-algebraic linearization, thereby eliminating parallel composition and event synchronization.

Supported specifications

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

  • Specifications without automata are not supported.

Implementation details

A location pointer variable is introduced for each original automaton, and the use of locations in expressions is eliminated. This is mostly similar to what the Eliminate the use of locations in expressions CIF to CIF transformation does, except that for instance location pointer variables are added for all automata. For nameless locations, name X is used.

One new automaton, named M, is created. If all original automata have the same supervisory kind, the new automaton gets this kind as well. Otherwise, it gets no supervisory kind. The alphabet of this new automaton is the union of alphabets of the original automata, including the events that are used to send or receive in any of the automata.

All declarations from the original automata are moved to the new automaton. They are renamed based on their absolute names. That is, for an automaton a with a constant c, the absolute name of the constant is a.c and the moved constant will be named a_c. Enumeration literals are not given absolute names, and keep their original names if possible.

One location, named L, is added. This location is both initial and marked. All initialization and marker predicates from all the original automata (including ones from locations) are merged together. They are put in the new automaton, and restrict the initialization and marker predicates of location L.

The invariants of the original automata (including ones from locations) are merged together in a similar way as the initialization and marker predicates. The supervisory kinds of the invariants are made explicit, to ensure that the original supervisory kinds inherited from automata are preserved.

For the tau event, a self loop is created per original tau edge. For all other events, the edges are merged, resulting in a single self loop for each non-tau event. By creating single edges per non-tau event, non-deterministic choice may be eliminated, ensuring that the model size of the resulting specification is near-linear compared to the model size of the original specification.

Monitors are taken into account when merging the guards of the edges, resulting in simpler guard predicates. Communication is eliminated altogether, and events no longer have data types after linearization. For edges with receives, the ‘received value’ is replaced (in the updates) by the ‘send value’.

For instance, the following specification:

event e;

plant automaton p:
  disc int x = 1;

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

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

plant automaton q:
  location l1:
    initial;
    edge tau goto l2;

  location l2:
    edge e goto l1;
end

is transformed to the following specification:

event e;
enum E = l1, l2;

plant automaton M:
  alphabet e;

  disc int p_x = 1;
  disc E p = l1;
  disc E q = l1;

  initial p = l1 and true or p = l2 and false,
          q = l1 and true or q = l2 and false;

  marked p = l1 and false or p = l2 and false,
         q = l1 and false or q = l2 and false;

  location L:
    initial;
    marked;

    edge e when (p = l1 and p_x = 1 or p = l2 and p_x = 2) and
                (q = l1 and false or q = l2 and true)
           do if   p = l1 and p_x = 1: p_x := 2, p := l2
              elif p = l2 and p_x = 2: p_x := 1, p := l1
              end,
              q := l1;
    edge tau when q = l1 do q := l2;
end

We see that an enumeration E is added, with literals for all the locations of the original automata. We also see that plant automata p and q are linearized to plant automaton M. Two location pointers, p and q, named after the original automata, are added. The variables are moved. The initialization and marker predicates are linearized. We have one location L, which is initial and marked. For event e, the guards and updates are linearized into a single self loop. Location pointer updates are incorporated as well. For event tau, the single original edge is simply included as a self loop.

Non-determinism

If the original automata have non-determinism, this choice is eliminated as part of this transformation. Non-determinism can be present due to multiple outgoing edges for a single location, for the same event (excluding the tau event), with overlapping guards. Another cause of non-determinism is multiple senders or receivers that are enabled at the same time, for the same channel. In the resulting specification, the first possible transition is always taken, similar to how the simulator chooses, assuming the simulator is configured to always automatically choose the first transition. Linearization eliminates some of the non-determinism in this case, essentially choosing a specific trace through the state space. To ensure the same choices are made, events and automata are sorted in the same order for linearization and simulation.

For instance, the following specification:

automaton p:
  event e;
  disc int x = 0;

  location:
    edge e when x < 5 do x := x + 1;
    edge e when x > 3 do x := x - 1;
end

is transformed to the following specification:

enum E = X;

automaton M:
  alphabet p_e;

  event p_e;

  disc int p_x = 0;
  disc E p in any;

  initial p = X and false;
  marked p = X and false;

  location L:
    initial;
    marked;

    edge p_e when p = X and (p_x < 5 or p_x > 3)
             do if   p = X and p_x < 5: p_x := p_x + 1
                elif p = X and p_x > 3: p_x := p_x - 1
                end;
end

Here, we see that the edge for event e with guard x < 5 and update x := x + 1 is chosen to take precedence over the edge with guard x > 3 with update x := x - 1. This choice is based on the original specification, where the edge with guard x < 5 is listed before the edge with guard x > 3.

Related to this, are dummy updates, which are added to ensure that the correct updates are taken. For instance, the following specification:

automaton p:
  event e;
  disc int x = 0;
  location:
    edge e when x >= 3;
    edge e when x < 3 do x := x + 1;
end

is transformed to the following specification:

enum E = X;

automaton M:
  alphabet p_e;
  event p_e;

  disc int p_x = 0;
  disc E p in any;

  initial p = X and false;
  marked p = X and false;

  location L:
    initial;
    marked;

    edge p_e when p = X and (p_x >= 3 or p_x < 3)
             do if   p = X and p_x >= 3: p := X
                elif p = X and p_x < 3:  p_x := p_x + 1
                end;
end

Here, the edge with guard x >= 3 takes precedence over the edge with guard x < 3. To ensure that no updates are performed when the edge with guard x >= 3 is chosen, a dummy update is added (reassigning the location pointer variable the value it already has). If this update were to be omitted, the update of the other edge would instead be executed, which is undesirable.

Order

If code generation is performed on a linearized version of the specification, it may be a good idea to ensure the same order is used and the same choices are made, both in the generated code and in simulation. Assuming simulation was performed by always automatically choosing the first transition, this should correspond to the output of linearization. The linearized edges are in the same order as the transitions are calculated by the simulator. This is ensured by sorting events and automata in the same order for linearization and simulation. Also, as the Non-determinism section above explains, if non-determinism is eliminated, it is done in a way that preserves that order.

Code should thus be generated in the order of the linearized edges resulting from linearization. Each time the code for an edge is executed, the code should start from the top, to ensure always the first enabled transition is chosen.

Urgency

If the original automata contain urgent locations and/or urgent edges, a discrete boolean variable u is added to the linearized automaton. Initially, it’s value is true, and it must always remain so (plant invariant u;). We add self loops (event tau), with as guard the urgent locations and guards of urgent edges, such that the edge can be taken if the system is in an urgent location, or an urgent edge is enabled (guard wise). However, these edges update u to false, which violates the target location invariant, meaning we can never take these edges in a transition. Since the edge is also urgent, it means that if the edge is enabled guard wise, time may not progress, thus ensuring the urgency behavior of the original urgent locations and edges.

For instance, the following specification:

automaton p:
  event e;

  location l1:
    initial;
    urgent;
    edge e when true goto l2;

  location l2:
    edge e when 1 = 1 now goto l1;
end

is transformed to the following specification:

enum E = l1, l2;

automaton M:
  alphabet p_e;
  event p_e;

  disc E p = l1;
  disc bool u = true;

  initial p = l1 and true or p = l2 and false;
  marked p = l1 and false or p = l2 and false;

  plant invariant u;

  location L:
    initial;
    marked;

    edge p_e when p = l1 and true or p = l2 and 1 = 1
             do if   p = l1 and true:  p := l2
                elif p = l2 and 1 = 1: p := l1
                end;

    edge when p = l1 or p = l2 and 1 = 1 now do u := false;
end

So, if p (the location pointer variable for original automaton p) is equal to l1 (the enumeration literal for original location l1), then the guard of the new urgent edge is enabled, and time may not progress. Similarly, if p is equal to l2 and the guard 1 = 1 of the original urgent edge is enabled, the guard of the new urgent edge is enabled, and time may not progress. This correctly reflects the urgency conditions of the original specification.

To ensure that no additional event transitions are possible, the new urgent edge can never be taken, as it would update u to false, which violates plant invariant u.

Received values and tuple field projections

The following specification:

event tuple(int a, b) e;

automaton s:
  location:
    edge e!(1, 2);
end

automaton r:
  disc int x;
  location:
    edge e? do x := ?[a];
end

is transformed to the following specification:

event e;
enum E = X;

automaton M:
  alphabet e;

  disc E s in any;
  disc int r_x;
  disc E r in any;

  initial s = X and false,
          r = X and false;
  marked s = X and false,
         r = X and false;

  location L:
    initial;
    marked;

    edge e when s = X and true and (r = X and true) do r_x := (1, 2)[0];
end

Observe how event e no longer has a data type, and the communication (send and receive) have been eliminated. In the assignment x := ?[a], received value ? has been replaced by send value (1, 2). Since tuple values don’t have field names, the right hand side (1, 2)[a] has been replaced by (1, 2)[0], using the Eliminate tuple field projections CIF to CIF transformation.

Elimination of communication

Since channel communication is completely eliminated, and channels become regular events after this transformation, it is no longer possible to merge additional senders/receivers with the linearized specification. If you wish to merge another specification with additional communication partners, first perform the merging, and then the linearization.

Renaming

Since declarations are moved/merged, and new names are introduced, renaming may be necessary to ensure unique names within a single scope. In order to reduce the amount of renaming for the enumeration literals introduced for the locations of the original automata, all enumerations are merged together into a single enumeration in the specification, with name E.

If renaming is performed, a warning is printed to the console.

Size considerations

Declarations are moved, so they don’t increase the size of the specification.

The addition of location variables increases the size of the specification, but this is linear in the number of automata and the number of locations.

Assignment are added for the updates to the location pointers. The increase is linear in the number of edges. The additional dummy updates that are added are linear in the number of edges as well.

A single self loop is added for each non-tau event. This does increase the size of the specification. The guards are simply combined using boolean operators, and the increase is therefore linear in the number of guards. Similarly, updates are combined using ‘if’ updates, and the increase is also linear.

For original edges with multiple events however, the guards and updates are duplicated for each event. The duplication is linear in the number of events on those edges.

Since tau edges are essentially just moved, they don’t increase the size of the specification. That is, their size is linear in the number of original tau edges.

The initialization and marker predicates, as well as the invariants are moved. They remain linear in size related to the number of original predicates. The predicates for the locations are also made conditional on the values of the location pointer variable. This size increase is linear in the number of original locations. Predicates are combined using boolean operators, leading to a size increase that is linear in the number of original predicates.

If a single received value is used multiple times in the updates of a single edge, the send value is duplicated for each of those uses. As such, the size increase is linear in the number of uses of the received value.

If multiple senders and multiple receivers (individual send/receive edges, not whole automata) are present for a certain event, then the received value is expanded to all the potential send values, with the conditions under which they are used as send value (using an ‘if’ expression). As such, the received value are expanded into expressions that are linear in the number of senders. If we have only a single sender or a single receiver, this is linear. If we have multiple of both, this becomes quadratic (number of senders times number of receivers).

For urgency, an additional variable and invariant are added. This is a constant increase in size. A self loop is added as well. This self loop duplicates the guards of urgent edges. It also includes predicates for the urgent locations. The size of this edge is linear in the number of urgent locations, and the guards of the urgent edges.

From the above, it should be clear that while the specification may increase in size, it is mostly linear. Practically, the size of the linearized specification is usually linear compared to the size of the input specification.

Optimality

As should be clear from the examples above, this transformation does not try to generate optimized expressions. In fact, often almost all generated expressions can easily be simplified. To further simplify the result, apply additional CIF to CIF transformations, such as Simplify values.

Currently, no effort is made by this transformation to reduce for instance the number of dummy assignments, or the number of replacements of tuple field projections by tuple index projections.