glenda.party
term% ls -F
term% cat index.txt
TRACE(1)                    General Commands Manual                   TRACE(1)



NAME
       pret, trace - protocol compiler and analyzer

SYNOPSIS
       pret [ -v ] file

       trace [ -options ] [ arguments ... ]

DESCRIPTION
       Trace  analyzes the consistency of medium-sized data communication pro‐
       tocols.  A protocol is specified in a nondeterministic guarded  command
       language,  `Argos,'  that includes case selection, do-loops, variables,
       procedures, and macros.  The analyzer can be used to  trace  deadlocks,
       unspecified  receptions,  timing problems, errors caused by value pass‐
       ing, and violations of user-specified `assertions.'

       Pret reads the protocol specifications for a set  of  interacting  pro‐
       cesses from the file specified, checks its syntax and completeness, and
       prepares a file pret.out for the analyzer containing a finite state ma‐
       chine description of the protocol.  Under option -v pret lists the num‐
       bers of states in the state machines, reports if  any  states  are  un‐
       reachable, and lists the queue sort for each message queue declared.

       Tracing Options:

       In most cases the options c, f, l, and v will suffice to perform proto‐
       col analyses.  The primary tools for reducing search times  are  m,  q,
       and  x.   Options a, k, and n are for advanced use; i, t, and y are ex‐
       perimental.

       Option flags are listed after a single minus sign, followed by  a  list
       of  zero  or more arguments.  Options that take an argument are matched
       with an argument from the argument list in the order in which they  oc‐
       cur in the option list.

       a      List  all  prefix paths that were explored up to the point where
              they joined a previously analyzed path.  See also option l.

       b      Blast search.  The fastest scan of the  state  space  available.
              At  each  step in the analysis select one and only one execution
              option to be explored.  Will not analyze non-determinism  within
              process descriptions, nor the effect of the arbitrary interleav‐
              ing of process executions.  See also option x.

       c N    Invoke a class N validation, where N can be chosen between 0 and
              5 inclusive.  A class 0 search is fast and very partial; a class
              5 search is not necessarily fast but fairly complete.

       f or F Two different ways to format the  output  sequences.   Option  f
              gives  queue  histories,  in which every bracketed message indi‐
              cates a message sent but not received at the time of the  error.
              F  gives  a time ordered queue history, where each column corre‐
              sponds to a queue, and each line to a time step.

       i      Ignore variables.  Second order state space folding tool.

       j      Find first error sequence and quit.

       k N    Set size of state space cache to 1024*N  (default  N=30).   When
              the  caches  is filled, one state will be deleted for each state
              added.

       l      List execution loops.  Warning, there are usually many, and they
              are hard to interpret.

       m N    Restrict  search  depth to N steps.  By default the search depth
              is restricted to a limit that excludes only pathetic  executions
              (e.g. tenfold overlaps).  The default limit is always printed on
              the standard error file at the start of a run.

       n      Override timeout heuristic.  Override the heuristic that  avoids
              generating  an  abundance of `microsecond' timeouts.  Normally a
              timeout is only considered if it can resolve a pending lockup.

       q N    Restrict the maximum queue size to N slots, for all queues.

       r N    Restrict the runtime to N minutes.  This option cannot  be  used
              in combination with R.

       R N    Report  on  progress  every  N minutes of real time.  By default
              N=2.

       s      Show finite state machine transition tables graphically.  Do not
              perform an analysis.

       t N    Ignore the state of process N in state-matching operations.  The
              value of this mechanism remains  unproven.   Try  other  options
              first.

       v      Verbose.   List execution times, size of the state space, number
              of levels searched, etc. at the end of the run.

       x      Perform a fast partial search.  At each step in the analysis se‐
              lect one process capable of executing and explore all options in
              that one process.  Will not explore all possible interleavings.

       y      Ignore the state of queues in state-matching operations.

SEE ALSO
       G. J. Holzmann, Trace - a protocol analyzer,  AT&T  Bell  Laboratories,
       1984
       G. J. Holzmann, Automated protocol validation in Argos, AT&T Bell Labo‐
       ratories, 1984



                                     arend                            TRACE(1)