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:

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

  • Event participants (event-participants)

    Generates per event declared in the CIF specification, an overview of what elements of the specification participate for the event. This information can be used to understand when the event is enabled. The participants can be spread out over the CIF specification, so the generated overview can be used to find the relevant elements of the specification. Inspecting the overview can potentially also reveal modeling mistakes.

    The information includes which automata participate for the event and in what role, namely as sender, receiver, synchronizer or monitor. It also includes the state/event exclusion invariants that relate to the event. State invariants are not included.

    For each declared event, its non-escaped absolute name is printed, with an indication of whether it is a channel or a regular event. As the tau event is not declared in the specification, nothing is printed for tau events. The events are printed in sorted order. For each event, per relevant category of participation, the participants are listed in sorted order. If for a relevant category there are no participants, this is explicitly indicated as well.