CIF multi-level splitter

The CIF multi-level splitter is used to split one CIF specification into several smaller co-operating CIF specifications. The behavior of the specified system does not change. If you synchronize the smaller specifications, for example by merging them again, they behave the same as the original specification.

One use of this application is to enable data-based synthesis on large specifications. Synthesizing a large specification directly with data-based synthesis may take a very long time, or synthesis may not have enough memory available to complete its task. By first splitting the specification, performing synthesis on each part and finally merging the results again, you may be able to avoid such problems.

A specification cannot be split in arbitrary parts. In order to preserve the behavior of the specification, some of the automata, input variables and requirements that share certain CIF elements with each other must always be kept together. For example, a requirement using the value of a discrete variable must stay together with that discrete variable, and thus with the automaton that owns the discrete variable.

After creating clusters of such CIF elements, you can perform synthesis on each cluster and construct a local supervisor for it. By taking all local supervisors together, the supervised behavior of the complete specification is obtained. That behavior is the same as the behavior of a supervisor derived from the complete original specification, except that taking the supervisors of all partial specifications together may be blocking. That is, the non-blockingness guarantee still holds for each local supervisor, but it is no longer guaranteed for the complete specification.

In principle, each requirement could be put in a cluster together with its related plants. However, this may lead to a large number of clusters, and a lot of duplicated synthesis work. For instance, if two requirements relate to the same plants, it is more efficient to cluster the two requirements together with those shared plants. On the other hand, clustering everything into a single cluster returns us to the original scalability issues of synthesis on a single, large specification. It is therefore essential to strike a good balance between splitting the large specification into parts (to improve performance) and not splitting too much (to prevent duplicate work).

The multi-level splitter helps with this by automatically clustering the elements of the specification. It keeps together elements that must be kept together, and furthermore tries to find a good clustering that will give good synthesis performance. Intuitively, it clusters strongly related parts of the specification, while keeping less related parts in separate clusters. More concretely, it first finds plant groups that consist of plant elements that must be kept together, and requirement groups that consist of requirement elements that must be kept together. It then relates the plants and requirement groups, putting them into a Domain Mapping Matrix (DMM). From the DMM, a Design Structure Matrix (DSM) is created, that relates plant groups by shared requirements. A DSM clustering algorithm is then used to create a multi-level clustering of the plant groups. The algorithm is heuristic in nature, but generally gives good results, and can be tuned using various settings if needed.

As its result, the multi-level splitter generates a tree of partial specifications, one per cluster in the multi-level clustering. Each partial specification contains the relevant plants and requirements for that cluster. As a service for further processing of the partial specifications, the multi-level splitter also checks whether each partial specification complies with the pre-conditions of data-based synthesis, and it generates a ToolDef script to reduce the effort to synthesize a supervisor from each partial specification.

The multi-level splitter is based on the approach outlined in [Goorden et al. (2020)].

Starting the transformation

The transformation can be started in the following ways:

  • In Eclipse, right click a .cif or .cifx file in the Project Explorer tab or Package Explorer tab and choose CIF synthesis tools  Apply multi-level splitting…​.

  • In Eclipse, right click an open text editor for a .cif or .cifx file and choose CIF synthesis tools  Apply multi-level splitting…​.

  • Use the cifmultilevel tool in a ToolDef script. See the scripting documentation and tools overview page for details.

  • Use the cifmultilevel command-line tool.

Options

Besides the general application options, this application has the following options:

  • Input file: The absolute or relative file system path to the input CIF file.

  • DMM output file: The absolute or relative file system path to which to write information about the generated DMM. This file can be used for further analysis. When no path is specified for the option, the DMM information is not written.

  • Partial specifications output directory: The absolute or relative path to the directory to write all output files. If no path is specified, a path is constructed from the name of the input specification by removing the .cif extension if available, and appending _multilevel. The tool generates several files in the directory: a CIF file for each partial specification, and a ToolDef script to perform data-based synthesis on each of these partial specifications.

Clustering options

The clustering algorithm is heuristic in nature. While theoretically each result is good, practically it may not always suit your purpose. For instance, the automatic clustering could in certain cases result in partial specifications that do not provide good synthesis performance.

The following options allow tuning the resulting split:

  • Evaporation factor: Factor that influences when a node is considered to be part of a cluster. Higher values leads to fewer nodes in a single cluster and thus more (smaller) clusters. The value must be at least 1.0 and at most 10.0. Usually it is between 1.5 and 3.5. The default value is 2.0.

  • Inflation factor: Factor that influences how fast large values increase and small values decrease, where the small values are eventually eliminated. Higher values of the factor speed up the process. The value must be at least 1.0 and at most 4.0. Usually it is between 1.5 and 3.5. The default value is 2.0.

  • Bus detection algorithm: The bus detection algorithm to apply. By default, no bus is detected.

  • Bus factor: Factor that influences when a node is considered to be part of the bus. The actual interpretation of this factor depends on the chosen bus detection algorithm. The default value is 2.

  • Convergence limit: Allowed remaining numerical error before considering termination of the algorithm. Higher values end the computation sooner at the cost of less precision in the results. The value must be between 0 and 1 (where 0 is not achievable, and 1 is not precise enough). The default value is 1e-4.

  • Step count: Number of additional nodes to visit each iteration. The value must be at least 1 and at most 4. The default value is 2. Changing this values is rarely needed.

More details about the clustering algorithm are available as part of the DSM clustering tool documentation.

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:

Supported specifications

The CIF multi-level splitter tool has performed pre-processing before performing the checks below, which means that:

  • All annotations are ignored.

  • I/O declarations are ignored. A warning is printed if the specification contains a CIF/SVG input mapping.

  • Component definitions and instantiates are allowed (they have been eliminated already).

  • Automata references with self are allowed (they have been rewritten).

The CIF multi-level splitter allows a subset of CIF specifications. Many of the restrictions are inherited from the data-based synthesis application. It may be a good idea to consult its documentation of supported specifications when in doubt if something is supported. Note that the CIF multi-level splitter tool checks the data-based synthesis pre-conditions on its generated partial output specifications in an effort to catch problems as early as possible.

  • Regarding automata and invariants:

    • Automata must have exactly one initial location, and it must be possible to determine this statically.

    • Initialization predicates in components, so outside of locations, are not allowed.

    • Marker predicates in locations are only allowed if they can be statically evaluated to either true or false.

    • Marker predicates in components, so outside of locations, are not allowed.

    • Only plant and requirement automata are allowed. Kindless and supervisor automata are not allowed.

      • Only requirement invariants are allowed. Kindsless, plant and supervisor invariants are not allowed.

    • The specification must have at least one input variable or one plant automaton. (An input variable counts as plant in this case.)

    • The specification must have at least one requirement automaton or one requirement invariant.

    • State requirement invariants are not allowed. Only state/event exclusion requirement invariants are allowed.

    • Invariants in locations are not allowed. Only invariants in components are allowed.

  • Regarding events:

    • Events must be either controllable or uncontrollable.

    • Tau events are not allowed.

    • Channels (events with data types) are not allowed.

    • Updates must be simple assignments. Conditional updates (if updates), multi-assignments, and partial assignments are not allowed.

  • Regarding variables:

    • Discrete variables must have one initial value that can be statically computed.

    • Continuous variables are not allowed.

    • Equations are not allowed.

    • Functions in any form are not allowed. This includes both standard library functions and user-defined functions.

  • Regarding data types:

    • The boolean type is allowed.

    • Enumeration types are allowed.

    • Ranged integer types are allowed.

    • All other types are not allowed.

  • Regarding expressions, only operators that take and produce data with a supported type are allowed. For example, regular division is not allowed since it produces a real value, and casting from a string to an integer is not allowed since the string type is not allowed.

Output of the CIF multi-level splitter

As discussed in the general introduction above, the multi-level splitter constructs several partial specifications from a single CIF specification. Each partial specification corresponds to a cluster in the multi-level clustering, and contains a part of the original specification. The partial specifications thus also form a tree.

All partial specifications for the plant groups are at the bottom of the tree, in the leaf nodes. All requirements that only relate to a single plant group are positioned in the same cluster as the corresponding plant group. Each level up in the tree contains clusters and their related partial specifications that cover more global parts of the system. For instance, consider a cluster at the second level that has two children. Then it contains the two plant groups of those children, but also all requirements that only relate to those two children and that weren’t already included at a lower level. All the partial specifications together cover all the plants and requirements of the entire original specification.

Partial specifications do no import their child partial specifications. Instead, their name indicates their place in the tree. The partialSpec.cif specification is at the top (highest level) of the tree. All other specifications have an index number for each level appended in their name. For example partialSpec_2_3.cif means that this file is the third part of the second part of the entire specification.

In addition, the multi-level splitter assists in performing data-based synthesis on the partial specifications. First it checks each partial specification against the pre-conditions of synthesis and reports the findings in a brief manner.

It also generates a ToolDef script to perform data-based synthesis on each of the partial specifications. Inside the script, the partial specifications with problems with respect to the data-based synthesis tool’s pre-conditions are commented out. The problem reports are also included as comment in the script for your convenience. In this way, you can quickly get an overview of the found problems and decide how to proceed. For example, you may want to change the original specification and perform multi-level splitting again.

If you decide to proceed by performing data-based synthesis on the partial specifications, the generated script has room for customizing data-based synthesis settings for each of the partial specifications individually.

Example

Suppose that in a system there are two counters, and the first counter may not increase if it would get bigger than the second counter. The specification is:

plant def Counter():
  controllable c_up, c_down;
  disc int[1..10] counter = 1;

  location:
    initial;
    edge c_up do counter := counter + 1;
    edge c_down do counter := counter - 1;
end

first: Counter();
second: Counter();

requirement first.first_up needs second.counter > first.counter;

Splitting this specification with the multi-level splitter reports:

Partial specification "partialSpec.cif":
    Plants:
        - Plant "first".
        - Plant "second".

    Requirements:
        - Requirement "requirement invariant first.first_up needs second.counter > first.counter".

    Children of the partial specification:
        - Partial specification "partialSpec_1.cif".
        - Partial specification "partialSpec_2.cif".

Partial specification "partialSpec_1.cif":
    Plants:
        - Plant "first".

    Requirements:
        None.

    Children of the partial specification:
        None.

Partial specification "partialSpec_2.cif":
    Plants:
        - Plant "second".

    Requirements:
        None.

    Children of the partial specification:
        None.

As you can see, there are two specifications at the bottom of the tree. They are partialSpec_1.cif and partialSpec_2.cif. Each contains one of the automata.

Above them is the top-level partialSpec.cif that contains the shared requirement. It also contains all parts of the specification needed to compute the requirement. For this small example, that is unfortunately the entire specification.

References

  • [Goorden et al. (2020)] Martijn Goorden, Joanna van de Mortel-Fronczak, Michel Reniers, Wan Fokkink and Jacobus Rooda, "Structuring Multilevel Discrete-Event Systems With Dependence Structure Matrices", IEEE Transactions on Automatic Control, volume 65, issue 4, pages 1625-1639, 2020, doi:10.1109/TAC.2019.2928119