---

Manual Reference Pages  - sift (n)

---

NAME

sift - high performance state space explorator and checker

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

CONTENTS

Synopsis
Description
Options
Examples
See Also
Authors

sift [-help] [-p]
[-R | -P | -V | -Q | -Z(v|i|vi) |
-D | -F | -F1 |
-W | -M | -H | -S | -E | -G]
[-equal | -incl | -hull]
[-f (form|file) | -dead] [-c n] [-t s] [-b n]
[-q | -k] [-kts | -lts | -ks | -rsf | -rsd | -rs]
[-NET | -NDR | -TPN | -PNML | -TTS]
[-df | -bf | -rf] [-seed] [-tree] [-inh] [-tc] [-pr] [-dt] [-stats]
[infile] [outfile] [digestfile] [errorfile]

sift builds various state space abstractions for extended Time Petri nets. It takes as input descriptions in textual form (.net, .pnml, .tpn formats) or graphical form (.ndr format of files produced by nd, .pnml with graphics), or a Time Transition System description in .tts format.

sift serves similar purposes as the tina tool, with less options but handles large states spaces much more efficiently. sift also allows to check reachability properties on the fly.

-help	Recalls options.
Operating mode options:
-R	Builds the marking reachability graph of a Petri net (untimed, or with temporal information discarded). This option forgets time constraints, it sets flag -tc.
-V	Builds the Covering Step Graph of a Petri net, according to the technique of Vernadat/Azema/Michel. The construction preserves deadlocks. This option forgets time constraints and priorities, it sets flags -tc -pr.
-P	Builds the partial marking graph of a Petri net, according to the persistent sets technique. The heuristic retained is to minimize local branching. This option forgets time constraints and priorities, it sets flags -tc and -pr.
-Q	Builds the partial marking graph of a Petri net. Combine the persistent sets (-P) and covering steps (-V) methods. This option forgets time constraints and priorities, it sets flags -tc and -pr.
-Zv | -Zi | -Zvi
	Builds marking graphs for three "maximal steps" firing rules: -Zv, or -sleptsov: a step at marking m is an enabled transition t fired at its maximum enabledness multiplicity at m; that is a bag t*k, where k is the largest integer such that t is firable k times simultaneously at m; -Zi, or -salwicki: a step at m is a maximal set of transitions simultenaously firable at m; -Zvi, or -slepsalw: a combination of -Zv and -Zi. A step at m is a maximal bag of transitions simultenaously firable at m; These options remove time constraints. In addition, options -Zi and -Zvi remove priorities.
-D	Builds the essential state graph of a Time Petri net, according to the technique of Popova. This graph preserves reachability and linear time temporal properties. Static intervals must be closed or unbounded and left-closed. If no temporal information is specified, or if all transitions bear interval [0,w[, then -D is silently replaced by -R.
-F | -F1	Builds the subgraph of the state graph obtained by firing integer delay transitions (unit delays if -F1) and discrete transitions. This graph strictly includes that obtained by -D and preserves the same properties. Static intervals must be closed or unbounded and left- closed. If no temporal information is specified, or if all transitions bear interval [0,w[, then -F/-F1 is silently replaced by -R.
-W	Builds the linear state class graph of a Time Petri net, according to the technique of Berthomieu/Menasche [IFIP1983]. The linear state class graph preserves marking reachability properties and linear time temporal properties. If no temporal information is specified, or if all transitions bear interval [0,w[, then -W is silently replaced by -R. This option removes priorities, it sets flag -pr.
-M	Option -M computes the set of markings of a TPN. Option -M is typically faster than -W and yields smaller state space abstractions, but it does not preserve firing sequences. ktz files created in mode -M only capture markings and the firable transitions represented as loop transitions on the markings they are firable from.
-H	Option -H computes an overapproximation of the set of markings of a TPN. It is typically much faster than options -M and -W and produces a set of classes with exactly one firing domain associated with each marking. Compared to -W, all classes associated with the same marking are merged into a single class obained from the dbm-hull of their domains (the smallest dbm including all of them). As for mode -M, ktz files created in mode -H only capture markings and the firable transitions.
-S	Builds the strong state class graph, according to the technique of Berthomieu/Vernadat [TACAS2003]. That graph preserves state reachability properties and linear time temporal properties; it is also compatible with priorities. If no temporal information is specified, or if all transitions bear interval [0,w[, then -S is silently replaced by -R.
-E	Option -E computes the set of states of a TPN. Option -E is typically faster than -S and yields smaller state space abstractions, but it does not preserve firing sequences. ktz files created in mode -E only captured markings and the firable transitions, represented as loop transitions on the markings they are firable from.
-G	Option -G computes an overapproximation of the set of states of a TPN. It is typically much faster than options -S and -E and produces a set of strong classes with exactly one clock domain associated with each marking. Compared to -S, all classes associated with the same marking are merged into a single class obained from the dbm-hull of their domains (the smallest dbm including all of them). As for mode -E, ktz files created in mode -G only capture markings and the firable transitions.
-equal	Identify two state classes when they are equal (default). This flag has the effects of -W if no priorities are specified, or of -S otherwise; It is ignored if the net is untimed or if some operating mode is simultaneously set.
-incl	Identify two state classes when one is included in the other. This flag has the effects of -M if no priorities are specified, or of -E otherwise; It is ignored if the net is untimed or if some operating mode is simultaneously set.
-hull	Merge all state classes with same marking into their dbm hull. This flag has the effects of -H if no priorities are specified, or of -G otherwise; It is ignored if the net is untimed or if some operating mode is simultaneously set.
Exploration strategy flags (when meaningful):
-df	Depth-first exploration order
-bf	Breadth-first exploration order (default)
-rf	Random exploration order -seed Initializes the random number generator so that different calls of sift with order -rf on the same arguments may traverse the state space in different orders.
input options:
-inh	Removes inhibitor and read arcs from the input net.
-pr	Removes priority constraints from the input net.
-tc	Removes time constraints from the input net.
-dt	Forgets data processing when reading a tts description.
Storage strategy flags:
-tree	Do not store states; assume any state computed is new.
Stopping conditions:
If some of these conditions fail and the output is ktz, then the ktz file captures a partial state space including the offending state and in which all non fully explored states bear property "sub".
-c n	Stop if the number of state enumerated exceeds n; no effects if n=0.
-t n	Stop if exploration lasts longer than n seconds; no effects if n=0.
-b n	Stops if the marking of some place exceeds n; no effects if n=0. Sift may take advantage of this value for choosing the representation of states.
-f form	Stop if some state does not obey property form; no effects if form=T. Formula form is any modality-free formula accepted by the selt model checker (check man selt for details). In addition, an atomic proposition is provided, "safe" or "L.safe", then asserts that the marking of each place does not exceed 1.
-f file	Equivalent to -f form, for the formula form read in file.
-dead	Stop if some deadlock state is found; shorthand for -f "-L.dead".
Other flags:
-p	Disables state space generation, just parses input net.
-stats	Prints progress information on the fly.
Input format and source:
-NET | -NDR | -PNML | -TPN | -TTS
	Specifies the format of the input net. This flag is necessary when the input net is read on standard input, or read from a file that does not bear the expected extension. By default, the net is assumed in .net or
infile	Where the net is read. The input format is determined by the file type, according to the table below. If absent or specified by "-", the net is read on standard input in the format specified by the input flag. If both an infile and some input flag are present, then the format defined by the input flag supersedes that determined by the infile extension. file extension          input format -------------------------------------------------------------- .net                    net format .ndr                    ndr format .tpn                    tpn format .pnml           pnml format .tts                    tts format
Output format:
-q | -ktz
	Specifies the format of the output. This flag is necessary when output is produced on standard output, or written in a file that does not bear the expected extension. -q means no output is printed, while -k means some output is produced in the .ktz proprietary compressed format.
Ktz output options:
As of Version 3.8.0, these options specify "profiles" for the ktz output. A profile makes precise the information to be recorded into the ktz file. Six profiles are defined; the first three are suitable for model-checking tools selt and muse, while the last three are not and are only suitable for the scan reachability checking tool.
-kts	Kripke Transition System: the ktz records state properties including divergence) and transition properties. This is the default profile.
-lts	Labelled Transition System: Like -kts except state properties are omitted;
-ks	Kripke Structure: Like -kts except transition properties are omitted;
-rsf	Reachability Set + Firable transitions: Like -kts except all transition targets are replaced by the index of the current state. This allows one to check reachability properties, absence of deadlocks and quasi-liveness of transitions, but not LTL nor modal mu-calculus formulas.
-rsd	Reachability Set + Deadlocks: Like -rsf except transition properties are omitted. Allows to check reachability properties and absence of deadlocks.
-rs	Reachability Set: Like -rsd except transitions are omitted. Only allows to check state reachability properties by tool scan.
The main benefit of profiles is to decrease the size of the ktz files when the intended properties of the behavior do not necessitate all the information recorded by the default profile. For instance, if the properties of interest are only about states, then it is not necessary to record in the ktz file information about transitions, what can save a considerable space and speed up the processing on the file.
Alternatively, ktz files can be stripped of undesired information (i.e. have their profile changed) using the ktzio tool (see the ktzio manual page).
Output destination:
outfile
	Where results are written. The output format is determined by the file type, according to the table below. If absent or specified by "-", then results are written on standard output in the format specified by the output format flag. If both an outfile and some output flag are present, then the format defined by the output flag supersedes that determined by the outfile extension. file extension          output format -------------------------------------------------------------- .ktz                    tina binary ktz format any other               textual output
Digest destination:
digestfile
	In addition to (possibly) its results in ktz form in file outfile, sift prints a summary of results in file digestfile (default stdout).
Errors destination:
errorfile
	Where error messages are written. By default, errors are printed on standard error.
Default options:
	Depend upon the features of the input net: If no time constraint: sift -R -c 0 -t 0 -b 0 -f T -q Else, if no priorities: sift -W -c 0 -t 0 -b 0 -f T -q Otherwise: sift -S -c 0 -t 0 -b 0 -f T -q

sift -f "p1 \/ t4" < ifip.ndr
sift -PNML mynet.xml
sift -f safe abp.ndr abp.ktz -stats

nd(n), tina(n), plan(n), struct(n), ktzio(n), ndrio(n), tedd(n), selt(n), muse(n), pathto(n), scan(n), play(n), walk(n), reduce(n), formats(n)

Bernard Berthomieu, with contributions by Alexandre Hamez (expatSML libraries), Didier Le Botlan (polycount), LAAS/CNRS, 2000-2024, Bernard.Berthomieu@laas.fr.