Download User Manual

12.4. COMMAND LINE OPTIONS
131
-P experimentfilepath
Same as the flat state space generator. For more details, refer to Section 11.3.
-N experimentname
Same as the flat state space generator. For more details, refer to Section 11.3.
-B experimentnumber
Generate the state space for the experiment numbered experimentnumber, with the first
experiment having number 0. For example, use “-B1” to run the second experiment (e.g.,
Experiment 2). Defaults to 0.
-c
Enables the compositional lumping algorithm, which is disabled by default.
-e, -s db entity, db macserver
These are internal options for interaction with the database. You can safely ignore them.
-l trace level[0-1]
Use trace level as the trace level described above. Only applies when you are running the
debug executable.
-t tracefilename
Create a trace file named tracefilename as output. If this option is not specified, output
is directed to the standard output stream.
-d MDD Utable size, union cache size, local exploration cache size,
MxD Utable size, submat cache size, add cache size
These are the different parameters for the symbolic data structures. They should follow the
-d option in the form of a comma-separated list of non-negative numbers. The numbers in
parentheses are the default value and the mininum value enforced by the symbolic SSG.
• MDD Utable size The size of the unique table of the MDD (50,000 and 1,000)
• union cache size The cache size of the union operation of the MDD (10,000 and 500)
• local exploration cache size The cache size of the local state space exploration operation of the MDD (10,000 and 500)
• MxD Utable size The size of the unique table of the MD (10,000 and 500)
• submat cache size The cache size of the submatrix operation of the MD (5,000 and
100)
• add cache size The cache size of the add operation of the MD (5,000 and 100)
This command line option is optional. If it is not given, the default values will be used. If the
option is present and the value for a parameter is zero or not given (i.e., there is no character
between two consecutive commas) the default value for that parameter is used.