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. 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 automaton of the state space, and a report with details of the found states.
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 is an NFA or a DFA, but is not necessarily minimal, even with the edge minimization option enabled. 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
.ciffile in the Project Explorer tab or Package Explorer tab and choose .In Eclipse, right click an open text editor for a
.ciffile and choose .Use the
cifexplorertool in a ToolDef script. See the scripting documentation and tools overview page for details.Use the
cifexplorercommand 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. 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. 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. 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
offto 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 an automaton, each state is represented by a location of that automaton, and the edges between states are represented as edges between locations. The automaton is named as configured using the Name option. If the state space is empty, the automaton has a single non-initial location.
If adding state annotations is enabled each location is annotated with a state annotation that indicates the current location of each automaton and the current value of each variable. If the state space is empty, the single location in the automaton does not have a state annotation, regardless of whether the option to add state annotations is enabled or not.