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

  ltl_model_check - perform LTL model checking on a flattened network
     _________________________________________________________________

   ltl_model_check  [-a  <ltl2aut_algorithm>]  [-b]  [-d <dbg_level>] [-f
   <dbg_file>]    [-h]   [-i]   [-m]   [-s]   [-t   <time_out_period>][-v
   <verbosity_level>]    [-A    <le_method>]    [-D    <dc_level>]    [-L
   <lockstep_mode>] [-S <schedule>] [-F] [-X] [-Y] [-M] <ltl_file>

   Performs  LTL  model  checking  on a flattened network. Before calling
   this  command,  the user should have initialized the design by calling
   the  command  [1]init_verify.  Regardless  of  the  options, no 'false
   positives'  or 'false negatives' will occur: the result is correct for
   the given circuit.

   Properties  to  be  verified should be provided as LTL formulae in the
   file  ltl_file.  Note  that  the  support of any wire referred to in a
   formula  should consist only of latches. For the precise syntax of LTL
   formulas, see the [2]VIS CTL and LTL syntax manual.

   A  formula passes iff it is true for all initial states of the system.
   Therefore,  in  the  presence of multiple initial states, if a formula
   fails, the negation of the formula may also fail.

   If  a  formula does not pass, a (potentially partial) proof of failure
   (referred  to  as  a  debug  trace)  is  demonstrated.  Fair paths are
   represented  by  a  finite  sequence of states (the stem) leading to a
   fair  cycle, i.e. a cycle on which there is a state from each fairness
   condition.  Whether  demostrate the proof or not can be specified (see
   option -d).

   Command options:

   -a <ltl2aut_algorithm>
          Specify  the  algorithm used in LTL formula -> Buechi automaton
          translation.

          ltl2aut_algorithm must be one of the following:

          0: GPVW.

          1: GPVW+.

          2: LTL2AUT.

          3: WRING (default).

   -b
          Use   boolean   minimization   during   the  LTL  to  Automaton
          translation.

   -d <dbg_level>
          Specify  whether  to  demonstrate  a  counter-example  when the
          system fails a formula being checked.

          dbg_level must be one of the following:

          0: No debugging performed. dbg_level=0 is the default.

          1: Generate a counter-example (a path to a fair cycle).

   -f <dbg_file>
          Write the debugger output to dbg_file.

   -h
          Print the command usage.

   -i
          Print  input  values  causing transitions between states during
          debugging. Both primary and pseudo inputs are printed.

   -m
          Pipe debugger output through the UNIX utility more.

   -t <timeOutPeriod>
          Specify  the  time  out  period  (in  seconds)  after which the
          command aborts. By default this option is set to infinity.

   -s
          Print  debug  output  in the format accepted by the [3]simulate
          command.

   -v <verbosity_level>
          Specify  verbosity  level.  This sets the amount of feedback on
          CPU usage and code status.
          verbosity_level must be one of the following:

          0: No feedback provided. This is the default.

          1: Feedback on code location.

          2: Feedback on code location and CPU usage.

   -A <le_method>
          Specify  whether  the  compositional  SCC  analysis  algorithm,
          Divide  and  Compose  (DnC),  is enabled for language emptiness
          checking.  The  DnC  algorithm first enumerates fair SCCs in an
          over-approximated abstract model, and then successively refines
          them  in  the  more concrete models. Since non-fair SCCs can be
          ignored  in  the more concrete models, a potentially large part
          of   the  state  space  are  pruned  away  early  on  when  the
          computations are cheap.

          le_method must be one of the following:

          0 : no use of Divide and Compose (Default).

          1 : use Divide and Compose.

   -D <dc_level>
          Specify  extent  to which don't cares are used to simplify MDDs
          in  model checking. Don't cares are minterms on which the value
          taken   by   functions   does   not   affect  the  computation;
          potentially,  these  minterms  can be used to simplify MDDs and
          reduce the time taken to perform model checking.
          dc_level must be one of the following:

          0 : No don't cares are used.

          1 : Use unreachable states as don't cares. This is the default.

          2  :  Use  unreachable  states  as  don't  cares  and in the EU
          computation, use 'frontiers' for image computation.

          3  : First compute an overapproximation of the reachable states
          (ARDC),  and  use  that  as  the cares set. Use `frontiers' for
          image  computation.  For  help on controlling options for ARDC,
          look  up  help  on the command: [4]print_ardc_options. Refer to
          Moon,  Jang,  Somenzi,  Pixley, Yuan, "Approximate Reachability
          Don't  Cares  for  {CTL}  Model  Checking", ICCAD98, and to two
          papers  by Cho et al, IEEE TCAD December 1996: one is for State
          Space  Decomposition  and  the  other  is  for  Approximate FSM
          Traversal.

   -S <schedule>
          Specify  schedule  for  GSH  algorithm,  which  generalizes the
          Emerson-Lei   algorithm   and   is  used  to  compute  greatest
          fixpoints. The choice of schedule affects the sequence in which
          EX  and  EU  operators  are applied. It makes a difference only
          when fairness constraints are specified.
          <schedule> must be one of the following:

          EL  :  EU  and  EX  operators  strictly  alternate. This is the
          default.

          EL1 : EX is applied once for every application of all EUs.

          EL2  :  EX  is applied repeatedly after each application of all
          EUs.

          budget : a hybrid of EL and EL2

          random  :  enabled  operators  are  applied  in (pseudo-)random
          order.

          off  :  GSH is disabled, and the old algorithm is used instead.
          The  old algorithm uses the EL , but the termination checks are
          less sophisticated than in GSH.

   -F
          Use  forward  analysis  in  the  computation  of  the  greatest
          fixpoint.  This  option is incompatible with -d 1 or higher and
          can only be used with -D 1.

   -L <lockstep_mode>
          Use  the  lockstep  algorithm,  which  is  based  on  fair  SCC
          enumeration.
          <lockstep_mode> must be one of the following:

          off  :  Lockstep  is  disabled.  This  is the default. Language
          emptiness is checked by computing a hull of the fair SCCs.

          on : Lockstep is enabled.

          all : Lockstep is enabled; all fair SCCs are enumerated instead
          of  terminating  as  soon  as one is found. This can be used to
          study  the  SCCs  of a graph, but it is slower than the default
          option.

          n  : (n is a positive integer). Lockstep is enabled and up to n
          fair SCCs are enumerated. This is less expensive than all , but
          still less efficient than on , even when n = 1 .

   -X
          Disable  strength  reduction (use different decision procedures
          for  strong,  weak, and terminal automaton). Strength reduction
          is  the  default.  Refer  to  Bloem,  Ravi, Somenzi, "Efficient
          Decision Procedures for LTL Model Checking," CAV99.

   -Y
          Disable  incremental  construction  of the partition for (MxA).
          Instead,  build  a  new partition from the scratch. Incremental
          construction of the partition is the default.

   -Z
          Add  arcs  into  the  Buechi  automaton  by  direct  simulation
          relation,  to  heuristically  reduce  the  length  of  shortest
          counter-example  in model checking. Refer to Awedh and Somenze,
          "Proving More Properties with Bounded Model Checking," CAV04.

   -M
          Maximize   (adding  arcs  to)  Buechi  automaton  using  Direct
          Simulation.

   <ltl_file>
          File containing LTL formulas to be model checked.

   Related "set" options:

   ltl_change_bracket <yes/no>
          Vl2mv  automatically  converts  "[]"  to  "<>"  in  node names,
          therefore  CTL*  parser  does  the same thing. However, in some
          cases  a  user  does  not  want  to  change  node names in CTL*
          parsing.  Then,  use this set option by giving "no". Default is
          "yes".

          See   also  commands  :  model_check,  approximate_model_check,
          incremental_ctl_verification
            __________________________________________________________

          Last updated on 20050519 10h16

References

   1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html
   2. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html
   3. file://localhost/projects/development/hsv/vis/common/doc/html/simulateCmd.html
   4. file://localhost/projects/development/hsv/vis/common/doc/html/print_ardc_optionsCmd.html