CIF to CIF transformer

The CIF to CIF transformer can be used to syntactically transform CIF specifications to similar CIF specifications, which behave in the same manner (are semantically equivalent), but are expressed using different language constructs. For example, the CIF to CIF transformation that eliminates constants, replaces all uses of constants by their values, and removes the constants from the specification.

These reusable transformations are primarily used to increase the subset of CIF specifications that can be transformed or processed. Usually, there is no need to apply the CIF to CIF transformations manually. Transformations that work on subsets of the CIF language, automatically apply the necessary CIF to CIF transformations as a preprocessing step, to increase the translatable subset.

The CIF to CIF transformer can also be used as a pretty printer.

Starting the transformation

The transformation can be started from Eclipse in the following ways:

  • Right click a .cif file in the Project Explorer tab or Package Explorer tab and choose CIF miscellaneous tools  Apply CIF to CIF transformations…​.

  • Right click an open text editor for a .cif file and choose CIF miscellaneous tools  Apply CIF to CIF transformations…​.

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

  • Use the cif2cif command line tool.

Options

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

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

  • Output file path: The absolute or relative local file system path to the output CIF specification. If not specified, the output file path defaults to the input file path, where the .cif file extension is removed (if present), and a .transformed.cif file extension is added.

  • Transformations: The CIF to CIF transformations to apply. The transformations are applied in the chosen order. Transformations may be applied multiple times. By default, no transformations are applied, essentially making the CIF to CIF transformer a pretty printer.

    In the option dialog, the available transformations are shown. To add a transformation, double click it, or select it and click the Add button below the list of available transformations. To remove a transformation, double click on it in the list of chosen transformations, or select it in that list and click the Remove button.

    At the command line, specify comma separated transformation names, in the order they should be applied. The names to use are listed below, in the Available transformations section.

Transformation descriptions

The pages describing the available transformations all use the same format. They have the following sections:

  • Introduction: describes the transformation in a few sentences.

  • Supported specifications: describes the subset of CIF specifications to which the transformation can be applied.

  • Preprocessing: specifies the CIF to CIF transformations that are automatically applied as preprocessing, or the CIF to CIF transformations that can be manually applied as preprocessing, to increase the subset of CIF specifications that can be transformed by the transformation.

  • Implementation details: further specifies what the transformation does, how it does it, and what the result of the transformation is. Most transformations also show one or more examples.

  • Renaming: explains if and when renaming may be performed by the transformation.

  • Size considerations: describes whether the transformation reduces or increases the size of the specification. If the specification may increase in size, an estimate of the order of increase is given (linear, exponential, etc). Note that the size is not the file size, but rather the number of objects used to represent the specification (the number of automata, locations, edges, guards, binary operators, etc).

  • Optimality: describes why the transformation result may not be optimal, if applicable. May also explain how to eliminate certain concepts that may be introduced as the result of the transformation.

  • Annotations: describes which specific annotations the transformation processes, as well as whether the transformation adds or removes any annotations.

Available transformations

A whole collection of CIF to CIF transformations is available. The available transformations are listed below, with a link to the information about the transformation, and the name to use for that transformation on the command line.

Pretty printer

If no transformations are applied by the CIF to CIF transformer, the input CIF specification is just read from the input file, validated, and written to the output file. This can be useful, as it essentially turns the CIF to CIF transformer into a CIF pretty printer.

As a side effect of reading the input file and validating it, the model may change slightly. In fact, this occurs not only for the CIF to CIF transformer but for all tools, as they all read input files and validate them, before continuing with their actual task. Examples of such changes include the elimination of imports, the loss of comments, and the evaluation of tuple projection indices.