.TH walk n "Version 4.0.0" "Tina Tools"

.SH NAME
walk  \- Tina random walk explorer

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


.SH SYNOPSIS

.B walk
[\-\f2h\f1elp] [-p]
     [-R | -P | -V | -Q | -Z(v|i|vi)]
     [-T[,(min|max|rand)][,(dense|discrete)] | -W | -S]
     [-f form | -dead] [-c n] [-t s] [-b n]
     [-seed] [-loop | -repeat] [-only s] [-favor s] [-avoid s] [-never s]
     [-q | -v] [-NET | -NDR | -TPN | -PNML | -TTS]
     [-inh] [-tc] [-dt] [-pr] [-sw] [-stats] [-trace] 
     [infile] [outfile] [digestfile] [errorfile]


.SH DESCRIPTION

Tool walk allows  to  simulate  net descriptions  in  any of  formats
\&.net,  \&.ndr,  \&.tpn, \&.pnml  or  \&.tts. Its capabilities include
those provided by the play tool except that walk is not interactive and
never stores history. walk is typically much faster than play and provides
more simulation modes; its primary intent is to quickly find counter examples
to reachability properties in a random walk over markings, timed state
markings, or state class markings.

.SH OPTIONS

.TP
\-\f2h\f1elp
Recalls options.


.TP
.B Marking paths specification:

.TP
If there are no time constraints in the input net, then a path is a sequence of net markings separated by net transitions or steps (sets of transitions fired simultaneousy).

.TP
\-R
Path transitions are single net transitions.

.TP
\-P
The path transitions are firing sequence in the partial marking graph built by the persistent set
method.

.TP
\-V
The path transitions are steps in the partial marking graph built by the covering steps method.

.TP
\-Q
The path transitions are steps of the partial marking graph built by the persistent steps
method (combining -P and -V construction, see tina papers for details).

.TP
\-Zv | -Zi | -Zvi
The path transitions are steps of the marking graphs built by three "maximal steps" firing rules:
.br
-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;
.br
-Zi, or -salwicki: a step at m is a maximal set of transitions simultenaously firable at m;
.br
-Zvi, or -slepsalw: a combination of -Zv and -Zi. A step at m is a maximal bag of transitions simultenaously firable at m;
.br
These options remove time constraints. In addition, options -Zi and -Zvi
remove priorities.

.TP
.B Timed state paths specification:

.TP
If the input net is a Time Petri net with nontrivial time constraints, then a path is either a  series of states
separated by  transitions (delay transitions followed by discrete transitions) in the -T construction,
or a series of state classes separated by discrete transitions in the -W and -S constructions.

.TP
\-T[,(min|max|rand)][,(dense|discrete)]
Each path transition is a delay followed by a net transition.
One may specify that delays are the minimum allowed, maximum allowed, or ca be choosen randomly between these.
The semantics of time is either discrete (integer time instants only0 or dense.
If the input net is not timed or all transition delays are trivisl ([0,w[), then -T is silently handed as -R.

.TP
\-W | -S
States are state classes (-W) or strong state classes (-S). Path transitions are net transitions,
time delays are abstracted.


.TP
.B Path constraints:

.TP
\-seed
Initializes the random number generator so that different calls of walk on the same arguments
have a chance to explore different paths (if any).

.TP
\-loop
If the current state is a deadlock and it is not a counter example to the property to be checked,
then the simulation is restarted from the initial state.

.TP
\-repeat
Same as -loop except does not restart on reaching a time or path length limit.

.TP
\-favor s | -avoid s
Whevener possible along the path, pick transitions in s (-favor s), or not in s (-avoid s).
If s is a file, then the set considered is the contents of file s.

.TP
\-only s | -never s
Restrict path to the transitions in s (-only s), or not in s (-never s).
If not possible, then the path is terminated.
If s is a file, then the set considered is the contents of file s.


.TP
.B Stopping conditions:

Flags -f and -dead specify formulas that should be invariant. walk stops along a path if some state
violating the specified formula is found.

.TP
\-f form
Stop with result FALSE if some state does not obey property form; no effects if form=T.
Stops with result OPEN if no counter example was found along the path developped.
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.
If form is a file, then the formula considered is the contents of file form.

As of Version  4.0.0, the input formula  passed by -f may be  a set of formulas,
represented  by a string  (possibly in a file)  in which individual formulas are
separated by a semicolon.
At each  step, all open formulas are evaluated at the  current state.
If some formula is resolved then a suitable message is printed on the fly on stdout.
Formulas in a set are  referred to  by their  index  in the  set description.
walk terminates when  no more  open formula  is left or  by one  of the limit options.

.TP
\-dead
Stop with FALSE if some deadlock state is found; shorthand for -f "-L.dead".

.TP
\-c n
walk stops with result OPEN if the length of the path taken exceeds n (unless -loop passed).

.TP
\-t s
walk stops with result OPEN if more than s seconds elapsed since walk was called.

.TP
\-b n
Stops with FALSE if some marking is found that marks some place with more than n tokens.


.TP
.B Input options:

.TP
\-inh
Forget inhibitor and read arcs in the input net.

.TP
\-pr
Forget priority constraints in the input net.

.TP
\-tc
Forget time constraints in the input net.

.TP
\-dt
Forget data processing when reading a tts description.

.TP
\-sw
Forget stopwatch and stopwatch-inhibitor arcs in the input net.



.TP
.B Input format and source:

.TP
\-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
.ndr format.

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

.nf
file extension		input format
--------------------------------------------------------------
\&.net			net format
\&.ndr			ndr format
\&.tpn			tpn format
\&.pnml			pnml format
\&.tts			tts format
.fi


.TP
.B Output format and destination:

.TP
\-q | -v
Verbosity level, quiet (-q) or verbose (-v).


.TP
outfile
Where results are written. If absent or specified  by "-",
results are written on standard output.


.TP
.B Digest destination:

.TP
digestfile
In addition to (possibly) its results in file outfile, walk may 
prints a summary of results in file digestfile (default stdout).


.TP
.B Errors destination:

.TP
errfile
Where error messages are written. If absent or specified  by "-", error messages are written on standard error.

.TP
.B Other flags:

.TP
\-stats
prints progress information on the fly (path length so far).

.TP
\-trace
prints path transitions on the fly, prefixed by delays if input is timed.



.SH EXAMPLES

.nf
walk -T,min,dense -f L.safe ../nets/ifip.ndr
walk -R -dead AirplaneLD-PT-0010.pnml
walk -W -f -t4 ../nets/ifip.ndr
walk -W -f -p3 ../nets/ifip.ndr
.fi


.SH SEE ALSO

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

.SH AUTHORS
Bernard Berthomieu
LAAS/CNRS,  2000-2026, Bernard.Berthomieu@laas.fr

