CIF explorer

The CIF explorer unfolds the state space expressed by a CIF specification, in an untimed setting. It thereby computes the untimed state space, consisting of all reachable states and the transitions between them.

It takes a CIF model and iteratively explores the states using event transitions, unfolding the state space. 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.

Available output forms include a CIF model with an automaton representing the state space, and a report with details of the found states and transitions.

The statespace is computed in terms of the states of the CIF specification, based on the current locations of its automata and the values of its variables. The resulting statespace automaton is an NFA or a DFA, but is not necessarily minimal. You can minimize it using the DFA minimizer, assuming the state space satisfies that tool’s preconditions.

Starting the program

The explorer can be started in the following ways:

  • In Eclipse, right click a .cif file in the Project Explorer tab or Package Explorer tab and choose CIF miscellaneous tools  Explore untimed state space…​.

  • In Eclipse, right click an open text editor for a .cif file and choose CIF miscellaneous tools  Explore untimed state space…​.

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

  • Use the cifexplorer 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.

  • Remove duplicate transitions: Removes duplicate transitions from the state space, before printing statistics and writing output files. Two transitions are duplicates if they have the same source and target states, and the same event. The communication value, if any, is ignored. Enabling this option removes duplicate transitions from the state space, possibly reducing the state space. But, enabling this option does not guarantee that the resulting state space automaton is minimal. This option is 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 transitions of the resulting state space. It is recommended to enable the option to remove duplicate transitions when printing statistics. This option is enabled by default.

  • Enable CIF output: Enable output as a CIF automaton, with states represented by locations and transitions by edges. This option is enabled by default. See for more information the section on output as a CIF automaton.

  • Add state annotations: Add state annotations to the locations of the CIF automaton in the output CIF specification. This option is enabled by default. See for more information the section on output as a CIF automaton.

  • Output file path: The absolute or relative file system path of the output CIF specification with the generated state space as a CIF automaton.

  • Name: The name of the resulting statespace automaton. If not specified, it defaults to statespace. If the resulting statespace automaton has a name that conflicts with an existing declaration, it is automatically renamed to have a non-conflicting name. See for more information the section on output as a CIF automaton.

  • Enable report: Enable writing a detailed report on the found states. This option is 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 CIF 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. A warning is printed if a requirement automaton or requirement invariant is encountered.

  • Controllability of events.

  • I/O declarations are ignored. A warning is printed if a CIF/SVG input declaration is encountered.

  • Annotations are ignored. If outputting a CIF model is enabled, the produced model may have annotations. See for more information the section on output as a CIF automaton.

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.

Output as a CIF automaton

If outputting a CIF model is enabled, a CIF specification is created and written to a file. The state space is represented by a state space automaton, each state is represented by a location of that state space automaton, and the transitions between states are represented as edges between locations. The state space automaton is named as configured using the Name option. If the state space is empty, the state space automaton has a single non-initial location.

If adding state annotations is enabled each location is annotated with a state annotation. The state annotation indicates the state of the input model represented by the location of the state space automaton. That is, each state annotation indicates the current location of each automaton from the input specification, and the current value of each variable from the input specification. If the state space is empty, the single location in the state space automaton does not have a state annotation, regardless of whether the option to add state annotations is enabled or not. The resulting CIF specification does not have any other annotations on any of its elements.