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