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 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 Specify the number of latches per group for ARDCS. size must be a positive integer (default = 8). ardc_affinity_factor 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Specify a filename containing grouping information filename containing grouping information ardc_write_group Specify a filename to write grouping information filename to write grouping information ardc_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: * set ardc_constrain_method 1 * set ardc_constrain_reorder no * set ardc_abstract_pseudo_input 0 _________________________________________________________________ Last updated on 20100410 00h02