Linearize (product with merge)

> > > >

Linearize (product with merge)

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

This transformation preserves non-determinism, preserving the specification’s full behavior, at the expensive of a possible exponential blow-up of the specification in terms of number of edges. To eliminate non-determinism, resulting in specifications with smaller state spaces, at the expense of not preserving the specification’s full behavior, use the linearize (merge) CIF to CIF transformation instead.

This transformation may introduce conditional updates (if updates). If you want to use the linearized model in tools that do not support conditional updates, use the linearize (product) CIF to CIF transformation instead, at the expense of a potential increase of the possibly-exponential blow-up in the number of linearized edges.

Supported specifications

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

Specifications without automata are not supported.

Preprocessing

The following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be transformed:

Implementation details

A location pointer variable is introduced for each original automaton with at least two locations, 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 with at least two locations.

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.

The structure of the original model is kept intact as much as possible, to allow objects to retain their absolute identities (absolute names). Since all automata are linearized into a single automaton, the original automata are replaced by groups. Each replacement group will contain (as much as possible) all of the declarations, invariants, etc of its original automaton.

All discrete and continuous variables from the original automata are moved to the new automaton, to ensure they can be assigned by the new automaton. Discrete variables must be moved to the single new automaton as they can only be declared in automata. All continuous variables of the original automata are moved to the single new automaton, regardless of whether they are assigned by updates on edges or not. Continuous variables declared outside automata remain where they are. The moved discrete and continuous variables are renamed based on their absolute names. That is, for an automaton a with a discrete variable v, the absolute name of the constant is a.v and the moved variable will be named a_v.

One location, named L, is added to the new automaton. This location is both initial and marked.

All initialization and marker predicates from the locations of the original automata are merged together. They are each put in the group that replaces their respective original automaton. Similarly, the invariants of the locations of the original automata are also each moved to their corresponding groups. And the initialization and marker predicates specified in automata, as well as invariants specified in automata, are moved there as well.

For the tau event, a self loop is created per original tau edge. For all other events, the Cartesian product of all edges is created, combining the edges in all possible combinations. This results in self loops for all non-tau events, where the combination of all self loops preserves all non-deterministic choices of the original specification. Worst case, the model size of the resulting specification compared to the model size of the original specification could blow up exponentially.

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'.

Where possible, exponential blow-up is prevented by merging multiple alternatives, via which an automaton may participate in synchronization, into a single alternative. Essentially, if there is no guard overlap and thus no non-determism, it does something similar to linearize (merge) CIF to CIF transformation instead. For more information, see the section about non-determinism.

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;

group p:
  enum LPE = l1, l2;

  initial M.p = l1 and true or M.p = l2 and false;
  marked M.p = l1 and false or M.p = l2 and false;
end

group q:
  enum LPE = l1, l2;

  initial M.q = l1 and true or M.q = l2 and false;
  marked M.q = l1 and false or M.q = l2 and false;
end

plant automaton M:
  alphabet e;

  disc int p_x = 1;
  disc .p.LPE p = .p.l1;
  disc .q.LPE q = .q.l1;

  location L:
    initial;
    marked;

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

We see that the automata p and q are replaced by groups. They contain 'location pointer enumerations' LPE, with literals for their original locations. They also contain the linearized initialization and marker predicates of the locations. Do note that the transformation simplifies these predicates beyond what is shown in this example, but they are shown here in full, to examplify the construction of such predicates. We further 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 discrete variables are moved. We have one location L, which is initial and marked. For event e, one self loop edge is added. In principle, automaton p has two edges for e and automaton q has one edge for e, leading to 2 * 1 = 2 edges in the product. However, in this case, these two edges can be merged into a single edge, as the originate from different source locations and are thus never enabled at the same time (there is no non-determinism). The guards of the original edges are combined, as are the updates. Location pointer updates are incorporated as well. For event tau, the single original edge is simply included as a self loop. Within M, p refers to the location pointer variable and thus all references to objects in automaton p (now group p) use scope absolute references, e.g. .p.l1.

Non-determinism

If the original automata have non-determinism, this choice is preserved 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, in principle all possible combinations are included as self loops, although some optimizations are performed as we will discuss below. In principle, for a specification with 4 sender automata with two send edges each (8 send edges in total) and 5 receiver automata with two receive edges each (10 receive edges in total) for event e, and also 6 automata with two edges each that synchronize over that event (12 synchronization edges in total), the number of possible combinations for communication with synchronization is 8 * 10 * 12 = 960 possible combinations.

For instance, the following specification:

event e;

automaton p:
  disc int x = 0;

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

automaton q:
  disc int y = 0;

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

is transformed to the following specification:

event e;

group p:
  initial true;
  marked false;
end

group q:
  initial true;
  marked false;
end

automaton M:
  alphabet e;

  disc int p_x = 0;
  disc int q_y = 0;

  location L:
    initial;
    marked;

    edge e when p_x < 5 and q_y < 5 do p_x := p_x + 1, q_y := q_y + 1;
    edge e when p_x < 5 and q_y > 3 do p_x := p_x + 1, q_y := q_y - 1;
    edge e when p_x < 5 and q_y = 4 do p_x := p_x + 1, q_y := q_y - 1;
    edge e when p_x > 3 and q_y < 5 do p_x := p_x - 1, q_y := q_y + 1;
    edge e when p_x > 3 and q_y > 3 do p_x := p_x - 1, q_y := q_y - 1;
    edge e when p_x > 3 and q_y = 4 do p_x := p_x - 1, q_y := q_y - 1;
end

Here, we see that for event e, automaton p has two edges and automaton q has three edges. The linearization result has 2 * 3 = 6 edges.

In certain cases, when it can be statically determined that there is no guard overlap, and thus no non-determinism, edges are merged to prevent blow-ups in the number of linearized edges. Concretely, this transformation merges linearized edges in the following cases:

Merge of single explicit edge in a location with its implicit monitor edge:

An implicit monitor edge, by definition, never has guard overlap with the other edges in the same location. Hence, there is no non-determinism, and we can safely merge the two edges.

Concretely, if an event is monitored in an automaton, and a location of that automaton has exactly one edge for the event, and the edge has a guard, which is not explicitly true, then the implicit monitor edge is merged into the explicit edge, combining the two edges into one edge. Then, there is only one way for the automaton to participate in synchronization for that event, from that location, rather than there being two ways for it to participate. If an edge is labeled multiple times with the same event, then this counts as the location having multiple edges for the event, and the merge is not performed.

As an example, consider an automaton a that monitors event e, and one of its locations g with only the edge:
```
edge e when x > 1 do x := x + 1 goto h;
```
When this explicit edge is combined with the implicit monitor edge, it becomes always enabled in the source location. The updates, so both the explicit one and the one introduced by linearization to update the location pointer variable, are made conditional on the original guard of the explicit edge. This results in a single linearized self-loop edge:
```
edge e when a = g do if x > 1: x := x + 1, a := h end;
```
Merge of single participations from different source locations:

Edges from different source locations of the same automaton can never be enabled at the same time, as the automaton can only be in one location at a time. Hence, there is no non-determinism, and we can safe merge those edges.

Concretely, this transformation combines edges for the same event, with different source locations, from an automaton that synchronizes over the event, if they are the only synchronization options in their source locations. This merges two or more edges into a single edge. If a location has multiple explicit edges for the event, or it has a single edge labeled multiple times with that event, then the location has multiple ways to participate in synchronization and these edges are not merged.

As an example, consider an automaton a that synchronizes over event e and monitors that event:
```
event e;

automaton a:
  monitor e;
  disc int x;

  location g:
    initial;
    edge e when x > 1 do x := x + 1 goto h;

  location h:
    edge e goto i;

  location i:
    edge e when x >  1 goto g;
    edge e when x <= 1 goto h;
end
```
By the merging of the explicit edge in location g with the implicit monitor edge for that location, as explained above, location g has only one way to participate in the synchronization for event e. Location h only has one explicit edge for event e, and does not get an implicit monitor edge as the explicit edge is always enabled. Hence, location h also has only one way to participate in the synchronization for event e. Location i has two explicit edges, and gets an implicit monitor edge, and can thus participate in three ways in the synchronization for event e. We merge the participations for locations g and h, as they both have only a single participation option. We then get four linearized edges, one for the merged participation of locations g and h, and three for the participations of location i. The linearized edges are as follows (simplified a bit for clarity):
```
edge e when a = g or a = h do if   a = g and a_x > 1: a_x := a_x + 1, a := h
                              elif a = h:                             a := i
                              end;
edge e when a = i and a_x >  1 do a := g;
edge e when a = i and a_x <= 1 do a := h;
edge e when a = i and not(a_x > 1) and not(a_x <= 1);
```

In general, if an automaton has n ways to participate in synchronization, and there are m such automata, then the number of linearized edges is n^m. There is thus an exponential blow-up. If the n participation options can be merged into a single participation option, then the number of linearized edges is 1^m = 1 instead, preventing the exponential blow-up altogether. While this transformation prevents such blow-ups in some common cases, it does not prevent all such blow-ups, such as when there are two edges for the same event from the same source location.

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. This 'product with merge' variant of the linearization transformation mostly adheres to the execution scheme defined by the CIF controller properties checker. However, since it may generate multiple linearized edges for the same event, it is better to use the 'merge' variant of the transformation instead, if strict compliance to the execution scheme is desired. This 'product with merge' variant is therefore also not strictly compatible with the CIF simulator’s execution mode.

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:

group p:
  event e;
  enum LPE = l1, l2;

  initial M.p = l1;
  marked false;
end

automaton M:
  alphabet .p.e;

  disc .p.LPE p = .p.l1;
  disc bool u = true;

  plant invariant u;

  location L:
    initial;
    marked;

    edge .p.e when p = .p.l1 or (p = .p.l2 and 1 = 1) do if   p = .p.l1: p := .p.l2
                                                         elif p = .p.l2: p := .p.l1
                                                         end;

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

So, if M.p (the location pointer variable for original automaton p) is equal to p.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 M.p is equal to p.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:
    initial;
    edge e!(1, 2);
end

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

is transformed to the following specification:

event e;

group s:
  initial true and true;
  marked true and false;
end

group r:
  initial true and true;
  marked true and false;
end

automaton M:
  alphabet e;

  disc int r_x;

  location L:
    initial;
    marked;

    edge e when 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. If renaming is performed, a warning is printed to the console.

Size considerations

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

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

Assignments are added for the updates to the location pointers. The increase is linear in the number of 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.

Multiple self loops may be added for non-tau event, and thus may result in an exponential blow up of the number of edges.

The initialization and marker predicates of locations, as well as the invariants of locations are moved. They remain linear in size related to the number of original predicates. The predicates are related to 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.

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 due to the exponential blow up of the edges, linearization results can be significantly larger than the original specifications.

Optimality

This transformation performs some optimization of the generate expressions. However, often the generated expressions allow for additional simplification. 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 replacements of tuple field projections by tuple index projections.

Annotations

This transformation does not process or add any specific annotations. The annotations of the original automata are moved to the enumeration declarations of the newly created location pointer enumerations, but only for automata with at least two locations. Similarly, the annotations of the original locations are moved to the enumeration literals of the newly created location pointer enumerations, but only for automata with at least two locations. For automata with a single location, the annotations of the automata and their locations are removed. The single new automaton and its single new location do not have any annotations, nor do the linearized edges.