options

Currently, Cyclone provides a list of options for users to enable/disable features of the compiler.

A list of options

An option is used at the beginning of a Cyclone specification. The list of available options are as follows.

Name	Meaning
option-log	If it is set to true (option-log=true;), Cyclone will log necessary information about a specification and the log file is saved in a directory called log under your current directory. By default, this option is disabled (false).
option-trace	If it is set to true (option-trace=true;), Cyclone will produce a trace file that contains concrete values of each variable in each state/node of the path discovered. If there is no model, no trace file will be generated. By default, this option is disabled (false). The trace of a specification file is stored in directory named trace that normally is under your current directory.
option-debug	If it is set to true (option-debug=true;), Cyclone will enter into debug mode, output internal data structures and values for debugging purpose. By default, this option is disabled (false). The debug information is stored in directory named debug that normally is under your current directory.
option-timeout	This allows users to set a soft timeout for the solver that Cyclone uses. The unit here is second. For example, option-timeout=10; will set a 10 second timeout. By default, no timeout is set.
option-precision	This allows users to set a precision for the real numbers in a specification. By default, the precision is 2 (option-precision=2;). Currently, Cyclone accepts values between 1 and 15 (inclusive).
option-detect	If it is set to true (option-detect=true;), Cyclone will detect invariant inconsistencies that a specification may have. If a specification contains some inconsistencies, the possible cause will be reported. By default, it is disabled (false).
option-output	This allows users to set a specific trace format. The default value is "default" that is a text-based trace file.

An Example:

 option-trace=true;

 option-output="dot";

The above example asks Cyclone to produce a trace (if the spec is satisfied) and the output format of this trace is a "dot" file. The "dot" file can be further generated to a png file. See the following png file as an example for Gate controller specification.