print_ardc_options - print information about the ARDC options currently in use

print_ardc_options [-h] [-H]

Prints information about the current ARDC options.

Command options:

-h
Print the command usage.

-H
Print the ARDC set command usage.

Set parameters: The ARDC options are specified with the set command.
ardc_traversal_method <method>
Specify a method for approximate FSM traversal.

method must be one of the following:

0 : MBM (machine by machine).

1 : RFBF(reached frame by frame).

2 : TFBF(to frame by frame).

3 : TMBM(combination of MBM and TFBF).

4 : LMBM(least fixpoint MBM, default).

5 : TLMBM(combination of LMBM and TFBF).

ardc_group_size <size>
Specify the number of latches per group for ARDCS.

size must be a positive integer (default = 8).

ardc_affinity_factor <affinity>
Specify affinity factor to make a group for ARDCs. The available factor is from 0.0(use only correlation) to 1.0(use only dependency).

affinity must be a positive real (default = 0.5).

ardc_max_iteration <iteration>
Specify the maximum iteration count during approximate FSM traversal. Default is 0 which means infinite.

iteration must be a positive integer or zero.

ardc_constrain_target <target>
Specify where image constraining will be applied to.

target must be one of the following:

0 : constrain transition relation (default).

1 : constrain initial states.

2 : constrain both.

ardc_constrain_method <method>
Specify an image constraining method to compute ARDCs.

method must be one of the following:

0 : restrict (default).

1 : constrain

2 : compact (currently supported by only CUDD)

3 : squeeze (currently supported by only CUDD)

ardc_constrain_reorder <method>
Specify whether to enable variable reorderings during consecutive image constraining operations.

method must be one of the following:

yes : allow variable reorderings during consecutive image constraining operations (default)

no : don't allow variable reorderings during consecutive image constraining operations

ardc_abstract_pseudo_input <method>
Specify when to abstract pseudo primary input variables out from transition relation.

method must be one of the following:

0 : do not abstract pseudo input variables

1 : abstract pseudo inputs before image computation (default)

2 : abstract pseudo inputs at every end of image computation

3 : abstract pseudo inputs at the end of approximate traversal

ardc_decompose_flag <method>
Specify whether to use decomposed approximate reachable states or single conjuncted reachable states.

method must be one of the following:

yes : keep decomposed reachable stateses (default)

no : make a conjunction of reachable states of all submachines

ardc_projected_initial_flag <method>
Specify which initial states is going to be used.

method must be one of the following:

yes : use projected initial states for submachine (default)

no : use original initial states for submachine

ardc_image_method <method>
Specify image_mathod during computing reachable states of submachines.

method must be one of the following:

monolithic : use monolithic image computation

iwls95 : use iwls95 image computation (default)

mlp : use mlp image computation

tfm : use tfm image computation

hybrid : use hybrid image computation

ardc_use_high_density <method>
Specify whether to use high density in computing reachable states of submachines.

method must be one of the following:

yes : use High Density for reachable states of submachines

no : use BFS for reachable states of submachines (default)

ardc_reorder_ptr <method>
Specify whether to reorder partitioned transition relation after constraining fanin submachines.

method must be one of the following:

yes : whenever partitioned transition relation changes, reorders partitioned transition relation

no : no reordering of partitioned transition relation (default)

ardc_fanin_constrain_mode <method>
Specify which method will be used in constraining fanin submachines.

method must be one of the following:

0 : constrain w.r.t. the reachable states of fanin submachines (default)

1 : constrain w.r.t. the reachable states of both fanin submachines and itself

ardc_create_pseudo_var_mode <method>
Specify which method will be used to create pseudo input variables of submachines.

method must be one of the following:

0 : makes pseudo input variables with exact support (default)

1 : makes pseudo input variables from all state variables of the other submachines

2 : makes pseudo input variables from all state variables of fanin submachines

ardc_lmbm_initial_mode <method>
Specify which method will be used as initial states in LMBM computation.

method must be one of the following:

0 : use given initial states all the time

1 : use current reached states as initial states (default)

2 : use current frontier as initial states

set ardc_mbm_reuse_tr <method>
Specify whether to reuse already constrained transition relation for next iteratrion in MBM.

method must be one of the following:

yes : use constrained transition relation for next iteration

no : use original transition relation for next iteration (default)

ardc_read_group <filename>
Specify a filename containing grouping information

filename containing grouping information

ardc_write_group <filename>
Specify a filename to write grouping information

filename to write grouping information

ardc_verbosity <verbosity>
Specify the level of printing information during computing ARDCs.

verbosity must be 0 - 3 (default = 0).

The default settings correspond to the fast variants of LMBM and MBM. MBM never produces a more accurate approximation than LMBM for the same state-space decomposition. However, the corresponding statement does not hold for the fast versions. (That is, FastMBM will occasionally outperform FastLMBM.) To get the slower, but more accurate versions of LMBM and MBM use the following settings:
Last updated on 20050519 00h50