//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::_part_attributes.asciidoc[]

:leveloffset: -2

[[tools-chapter-cif-explorer]]
== CIF explorer

indexterm:[CIF explorer]
indexterm:[tools,CIF explorer]
indexterm:[single,state space,explorer]
indexterm:[single,state space,generator]
indexterm:[see: explorer,CIF explorer]
The CIF explorer unfolds the <<lang-tut-basics-chapter-synchronizing-events-statespace,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 https://en.wikipedia.org/wiki/DFA_minimization[minimal].
You can minimize it using the <<tools-eventbased-chapter-dfa-minimization,DFA minimizer>>, assuming the state space satisfies that tool's preconditions.

indexterm:[CIF explorer,start]

=== Starting the program

The explorer 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 menu:CIF miscellaneous tools[Explore untimed state space...].

* In Eclipse, right click an open text editor for a `.cif` or `.cifx` file and choose menu:CIF miscellaneous tools[Explore untimed state space...].

* Use the `cifexplorer` tool in a ToolDef script.
See the <<tools-scripting-chapter-intro,scripting documentation>> and <<tools-scripting-chapter-tools,tools overview>> page for details.

* Use the `cifexplorer` command line tool.

indexterm:[CIF explorer,options]

[[tools-chapter-cif-explorer-options]]
=== 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.

[[tools-cif-explorer-remove-duplicate-transitions]]
* _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 https://en.wikipedia.org/wiki/DFA_minimization[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.

[[tools-cif-explorer-enable-cif-output]]
* _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 <<tools-chapter-cif-explorer-output-cif,output as a CIF automaton>>.

[[tools-cif-explorer-add-state-annos]]
* _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 <<tools-chapter-cif-explorer-output-cif,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.

[[tools-cif-explorer-name]]
* _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 <<tools-chapter-cif-explorer-output-cif,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.

indexterm:[CIF explorer,supported specifications]

=== 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 2^31^ - 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 <<tools-cif-explorer-enable-cif-output,enabled>>, the produced model may have annotations.
See for more information the section on <<tools-chapter-cif-explorer-output-cif,output as a CIF automaton>>.

indexterm:[CIF explorer,preprocessing]

=== Preprocessing

Prior to exploration, the following <<tools-cif2cif-chapter-index,CIF to CIF transformations>> are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be explored:

* <<tools-cif2cif-chapter-remove-io-decls>>

* <<tools-cif2cif-chapter-remove-annos>>

* <<tools-cif2cif-chapter-elim-comp-def-inst>>

* <<tools-cif2cif-chapter-elim-self>>

In addition it applies the <<tools-cif2cif-chapter-simplify-values-no-refs-optimized>> CIF to CIF transformation to speed up processing.

[[tools-chapter-cif-explorer-output-cif]]
=== Output as a CIF automaton

If outputting a CIF model is <<tools-cif-explorer-enable-cif-output,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 <<tools-cif-explorer-name,_Name_ option>>.
If the state space is empty, the state space automaton has a single non-initial location.

If adding <<lang-tut-annotations-state,state annotations>> is <<tools-cif-explorer-add-state-annos,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.
