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 |
---|