4mwalk24m(n)                                                                4mwalk24m(n)

1mNAME0m
       walk  - Tina random walk explorer

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



1mSYNOPSIS0m
       1mwalk 22m[-4mh24melp] [-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]



1mDESCRIPTION0m
       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.


1mOPTIONS0m
       -4mh24melp  Recalls options.



       1mMarking paths specification:0m


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


       -R     Path transitions are single net transitions.


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


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


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


       -Zv | -Zi | -Zvi
              The  path  transitions  are steps of the marking graphs built by
              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.


       1mTimed state paths specification:0m


       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  dis-
              crete  transitions) in the -T construction, or a series of state
              classes separated by discrete transitions in the -W and -S  con-
              structions.


       -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 al-
              lowed, 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.


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



       1mPath constraints:0m


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


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


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


       -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  con-
              sidered is the contents of file s.


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



       1mStopping conditions:0m

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


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


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


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


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


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



       1mInput options:0m


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


       -pr    Forget priority constraints in the input net.


       -tc    Forget time constraints in the input net.


       -dt    Forget data processing when reading a tts description.


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




       1mInput format and source:0m


       -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 speci-
              fied by "-", the net is  read on standard  input in the   format
              specified  by  the input flag. If  both an  infile and  some in-
              put 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



       1mOutput format and destination:0m


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



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



       1mDigest destination:0m


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



       1mErrors destination:0m


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


       1mOther flags:0m


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


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




1mEXAMPLES0m
       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



1mSEE ALSO0m
       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), for-
       mats(n), stan(n)


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


Tina Tools                       Version 4.0.0                         4mwalk24m(n)
