source: vis_dev/vis-2.1/share/vis/help/print_guided_search_optionsCmd.txt @ 11

Last change on this file since 11 was 11, checked in by cecile, 13 years ago

Add vis
File size: 3.6 KB
Line 
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
Note: See TracBrowser for help on using the repository browser.