CIF information generator

The CIF information generator generates information about a CIF specification. The information to produce can be configured. The requested information is collected and written to a text file.

Starting the generator

The generator 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 analysis tools  Generate information….

  • In Eclipse, right click an open text editor for a .cif or .cifx file and choose CIF analysis tools  Generate information….

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

  • Use the cifinfogen 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 information text file. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a .info.txt file extension is added.

Supported specifications

The CIF information generator supports all CIF specifications.

The following CIF to CIF transformations are applied as preprocessing (in the given order), before the information is collected and written to the output file:

Information to produce

The CIF information option can be used to specify which information to produce. By default, all information is produced. In the option dialog, simply select which information to produce. On the command line, specify comma-separated names of information to produce.

Below, the information that can be produced is explained in more detail. For each kind of information, after the name of the information, the command line name of that information is indicated between parentheses.

The following information can be produced:

  • Global event-enablement conditions (event-enablement-conditions)

    Generates per event declared in the CIF specification, a global condition that indicates when the event is enabled. The information that comprises the global condition is generally spread out over the CIF specification, for example in the guards of edges of various synchronizing automata. It can therefore be useful to see it all in one place. Inspecting the conditions allows to double check them and potentially spot modeling mistakes. Furthermore, if the information is produced for a synthesized supervisor, it can give insight into the behavior of the controlled system, taking into account the supervisor’s guards.

    The enablement condition is derived from the automata that participate for the event, whether as a synchronizing automaton, send automaton, receive automaton or monitor automaton. Furthermore, all state/event exclusion invariants for the event are considered. The condition does not consider target state invariants. If the specification has any state invariants, a warning will be included in the output.

    For each declared event, its non-escaped absolute name is printed, followed by a colon and its condition predicate. As the tau event is not declared in the specification, nothing is printed for tau events. The events are printed in sorted order.