CIF 3

CIF explorer

The CIF explorer unfolds the state space expressed by a CIF specification, in an untimed setting. It takes a CIF model and iteratively explores the states using event transitions, unfolding the state space. Available output forms include a CIF automaton of the state space, and a report with details of the found states. Time transitions are never taken. The explorer will return a deadlock state when forced into a time step. Continuous variables are allowed, but behave much like discrete variables due to lack of time steps.

Starting the program

The explorer can be started in Eclipse in the following ways:

  • Right click a .cif file in the Project Explorer or Package Explorer and choose CIF miscellaneous tools ‣ Explore untimed state space....
  • Right click an open text editor for a .cif file and choose CIF miscellaneous tools ‣ Explore untimed state space....
  • Use the cif3explorer tool in a ToolDef 2 script. See the scripting documentation and tools overview page for details.
  • Use the cif3explorer command line tool.

Options

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

  • Input file path: The absolute or relative file system path to the input CIF specification.
  • Enable edge minimization: Enable edge minimization to remove duplicate edges of the state space, before printing statistics, and writing output files. Two edges are duplicates if they have the same source and target states, and the same event. The communication value, if any, is ignored. Enabled by default.
  • Enable statistics: Enable printing of statistics of the resulting state space to the console. Statistics include the number of states and the number of edges of the resulting state space. It is recommended to enable the edge minimization option when printing statistics. Enabled by default.
  • Enable CIF output: Enable output of states and edges as a CIF automaton. Enabled by default.
  • Output file path: The absolute or relative file system path of the output CIF specification with the generated state space as a CIF automaton.
  • Enable report: Enable writing a detailed report on the found states. Disabled by default.
  • Report file path: The absolute or relative file system path of the report file. If specified, option Enable report is implied.
  • Print progress: The number of states to process before printing progress information. Must be a non-negative integer number. May be off to disable progress information. The default is to print progress information after processing 1000 states.

The CIF output file is written if the Enable CIF output option is set, or if a path is supplied with the Output file path option. If the latter is given, its value is used as the path for writing the report file. If only the Enable CIF output option is set, the value of the Input file path option is used, where the .cif extension is removed (if present), and a _statespace.cif suffix is added.

The report file is written if the Enable report option is set, or if a path is supplied with the Report file path option. If the latter is given, its value is used as the path for writing the report file. If only the Enable report option is set, the value of the Input file path option is used, where the .cif extension is removed (if present), and a _report.txt suffix is added.

If both the CIF output and the report file output are disabled, the resulting state space is not outputted at all. In such cases, the state space explorer acts as a verifier for runtime errors, which can make the exploration fail. If exploration completes without errors, the explorer has verified that no runtime errors occur. Runtime errors include failures to compute values, such as division by zero, as well as assignments that assign values to variables that are outside the allowed bounds/ranges of the variables.

Supported specifications

The explorer supports a subset of CIF specifications. The following restrictions apply:

  • Usage of distribution types and distribution standard library functions is not supported.
  • Usage of derivatives is not supported.
  • External user-defined functions are not supported.
  • Input variables are not supported.
  • Specifications with more than 231 - 1 = 2,147,483,647 potential initial states are not supported.

The following information from the specification is ignored:

  • Automaton and invariant supervisory kinds.
  • Controllability of events.

Preprocessing

Prior to exploration, the following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be explored:

In addition it applies the Simplify values (no references, optimized) CIF to CIF transformation to speed up processing.