[11] | 1 | |
---|
| 2 | print_guided_search_options - print information about guided_search_options |
---|
| 3 | in use |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | print_guided_search_options [-h] |
---|
| 7 | |
---|
| 8 | Prints information about current Guided Search options. Guided search |
---|
| 9 | is an alternate method to compute fixpoints by modifying the fixpoint |
---|
| 10 | computation with restrictions. It is applicable to the compute_reach, |
---|
| 11 | check_invariant and model_check commands (refer to their help pages on |
---|
| 12 | the use of guided search). See also for details: Ravi and Somenzi, |
---|
| 13 | Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and |
---|
| 14 | Somenzi, Efficient Decision Procedures for Model Checking of Linear |
---|
| 15 | Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic |
---|
| 16 | Guided Search for CTL Model Checking, DAC'00. Not allowed with -A 2 or |
---|
| 17 | -i, and will only work with iwls95 or monolithic image methods. The |
---|
| 18 | description of some options can be found in the help page for set. |
---|
| 19 | |
---|
| 20 | Command options: |
---|
| 21 | |
---|
| 22 | guided_search_hint_type |
---|
| 23 | Choose from local (default) or global. If this flag is set to |
---|
| 24 | local, then every subformula is evaluated to completion, using |
---|
| 25 | all hints in order, before the next subformula is started. For |
---|
| 26 | pure ACTL or pure ECTL formulae, we can also set |
---|
| 27 | guided_search_hint_type to global, in which case the entire |
---|
| 28 | formula is evaluated for one hint before moving on to the next |
---|
| 29 | hint, using underapproximations. |
---|
| 30 | |
---|
| 31 | guided_search_underapprox_minimize_method |
---|
| 32 | Choose from "constrain" and "and" (default). Sets the method |
---|
| 33 | with which the transition relation is minimized when |
---|
| 34 | underapproximations are used. The option constrain is |
---|
| 35 | incompatible with hints that use signals other than inputs. |
---|
| 36 | |
---|
| 37 | guided_search_overapprox_minimize_method |
---|
| 38 | Choose from "squeeze" and "ornot" (default). Sets the method |
---|
| 39 | with which the transition relation is minimized when |
---|
| 40 | underapproximations are used. The option squeeze is |
---|
| 41 | incompatible with hints that use signals other than inputs. |
---|
| 42 | Ornot implies that the transition relation will be disjoined |
---|
| 43 | with the negation of the hint: T' = T + ~h, whereas squeeze |
---|
| 44 | will find a small BDD between T and T'. |
---|
| 45 | |
---|
| 46 | guided_search_sequence |
---|
| 47 | For compute_reach and check_invariant only. Set this flag to a |
---|
| 48 | list of comma-separated integers i1,i2,...,in, with n at most |
---|
| 49 | the number of hints that you specify . The k'th hint will be |
---|
| 50 | used for ik iterations (images). A value of 0 causes the hint |
---|
| 51 | to be applied to convergence. Not setting this option is like |
---|
| 52 | setting it to 0,0,...,0. If length of the specified sequence is |
---|
| 53 | less than the number of hints, the sequence is padded with |
---|
| 54 | zeroes. |
---|
| 55 | |
---|
| 56 | Guided search also uses the High Density traversal options that are |
---|
| 57 | germane to dead-ends. The relevant flags are hd_dead_end, |
---|
| 58 | hd_dead_end_approx_method, hd_frontier_approx_threshold, |
---|
| 59 | hd_approx_quality, hd_approx_bias_quality. Use help on the |
---|
| 60 | print_hd_options command for explanation of these flags. If guided |
---|
| 61 | search is used with HD using the -A 1 options in compute_reach and |
---|
| 62 | check_invariant, the HD options are used by both HD and guided search. |
---|
| 63 | _________________________________________________________________ |
---|
| 64 | |
---|
| 65 | Last updated on 20050519 10h16 |
---|