---

Manual Reference Pages  - scan (n)

---

NAME

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.

CONTENTS

Synopsis
Description
Options
Examples
See Also
Authors

scan [-help]

scan ktzfile [(-f|-r|-n) (form|file)] [(-d|-dead)]
[-c | -b | -s | -m] [-limit n] [-script]
[outfile] [errorfile]

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

-help	Recalls options.
Formulas:
(-f|-r[eachable]|-a[bsent]) 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 details).
(-f|-r[eachable]|-n[ever]) file
	Same for the formula form read in file.
(-d|-dead)	Counts states without successor(s).
Output format flags:
-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.
Input source:
ktzfile (or -)
	A ktz file (read on stdin if - and your OS allows reading binary on stdin)
Output destination:
outfile
	Where the results are written (default stdout).
Errors destination:
errorfile
	Where error messages are written (default stderr).

scan -dead ifip.ktz
scan -r "p10 \/ p12" abp.ktz -m
scan -n "p10 \/ p12" abp.ktz -m

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), formats(n)

Bernard Berthomieu, LAAS/CNRS, 2000-2024, Bernard.Berthomieu@laas.fr.