4mscan24m(n)                                                                4mscan24m(n)

1mNAME0m
       scan   -  filters states in a ktz description obeying some reachability
       property or deadlocked.

       Part of Tina Toolbox for analysis of Petri nets and Time Petri nets.


1mSYNOPSIS0m
       1mscan 22m[-4mh24melp]

       1mscan 22mktzfile [(-f|-r|-n)  (form|file)] [(-d|-dead)]
            [-c | -b | -s | -m] [-limit n] [-script] [-id s]
            [outfile] [errorfile]


1mDESCRIPTION0m
       Given a kripke transition system in a ktz file, counts  the  states  in
       the  file  obeying  the  formula passed by -f, -r or -n (if any) or the
       states without successor(s) if -dead is passed instead. Prints  results
       in the selected output format.

       Note:  For the same formulas, and all output formats, there is an invo-
       cation of the muse tool returning the same result, but  scan  typically
       uses  less space as it does not have to record the full state graph and
       can often instead proceed on the fly while reading the ktz  file.  scan
       is  much  faster  than selt or muse for checking reachability formulas,
       especially if the ktz file has profile rsf, rsd or ra.



1mOPTIONS0m
       -4mh24melp  Recalls options.


       1mFormulas:0m


       (-f|-r[eachable]|-n[ever]) form
              Counts states obeying property form;  none  if  form=F,  all  if
              form=T.   Formula  form is any modality-free formula accepted by
              the muse or selt model checkers (check  man  muse/selt  for  de-
              tails).


       (-f|-r[eachable]|-n[ever]) file
              Same for the formula form read in file.


       (-d|-dead)
              Counts states without successor(s).



       1mOutput format flags:0m


       -c     Prints  the number of states counted. This is the default output
              format.


       -b     If the formula is passed by -f or -r then prints  TRUE  if  some
              state  has  been counted, or FALSE otherwise; the states counted
              are then witnesses for the formula. This amounts  to  check  the
              CTL formula EF f.

              If  the  formula is passed by -n then prints FALSE if some state
              has been counted, or TRUE otherwise; the states counted are then
              counter examples for the formula.  This amounts to check the CTL
              formula AG f.


       -s     Prints the set of states counted as their  indices  in  the  ktz
              file, up to the limit set by -limit.


       -m     Prints the recorded states in clear, as they would be printed by
              program ktzio, up to the limit set by -limit.


       -limit n
              Limits  to  n the number of indices of states printed by options
              -s and -m.  No limit is set if n=0 (default).


       -script
              With boolean output, formulas are  printed  before  their  truth
              values.


       -id s  With  boolean  output  and  script  option  passed, prefixes the
              boolean result by string s instead of the formula verified.


       1mInput source:0m


       ktzfile (or -)
              A ktz file (read on stdin if - and your OS allows reading binary
              on stdin)


       1mOutput destination:0m


       outfile
              Where the results are written (default stdout).


       1mErrors destination:0m


       errorfile
              Where error messages are written (default stderr).



1mEXAMPLES0m
       scan -dead ifip.ktz
       scan -r "p10  p12" abp.ktz -m
       scan -n "p10  p12" abp.ktz -m


1mSEE ALSO0m
       nd(n),  tina(n),  plan(n),  struct(n),  ktzio(n),  ndrio(n),   tedd(n),
       selt(n), sift(n), pathto(n), muse(n), play(n), walk(n), reduce(n), for-
       mats(n), stan(n)


1mAUTHORS0m
       Bernard Berthomieu, LAAS/CNRS, 2000-2026, Bernard.Berthomieu@laas.fr.


Tina Tools                       Version 4.0.0                         4mscan24m(n)
