CIF 3

Event-based synchronous product

The event-based synchronous product takes one or more plant or requirement automata, and computes the synchronous product. Synchronous product means events on edges can only be taken if all automata with that event in their alphabet can take an edge with the same event at that time. This tool essentially computes the state space.

The tool takes a .cif file containing all automata to combine, and produces a new .cif file with the product automaton. If the kinds of the source automata are all the same, the resulting product automaton is of that kinds as well. Otherwise, the product automaton has unknown kind.

Starting the synchronous product tool

The tool can be started in the following ways:

  • In Eclipse, right click a .cif file in the Project Explorer or Package Explorer and choose CIF synthesis tools ‣ Event-based synthesis tools ‣ Apply synchronous product....
  • In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools ‣ Event-based synthesis tools ‣ Apply synchronous product....
  • Use the cif3prod tool in a ToolDef 2 script. See the scripting documentation and tools overview page for details.
  • Use the cif3prod command line tool.

Options

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

  • Input file: The absolute or relative local file system path to the input CIF specification.
  • Output file: The absolute or relative local file system path to the output CIF specification. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a _product.cif file extension is added. The product part of the default extension depends on the Result name option.
  • Result name: The name to use for the product automaton. If not specified, defaults to product. Also affects the Output file option.