man(1) Manual page archive

     TRACE(1)                     (arend)                     TRACE(1)

          pret, trace - protocol compiler and analyzer

          pret [ -v ] file

          trace [ -options ] [ arguments ... ]

          Trace analyzes the consistency of medium-sized data communi-
          cation protocols.  A protocol is specified in a nondetermin-
          istic guarded command language, `Argos,' that includes case
          selection, do-loops, variables, procedures, and macros.  The
          analyzer can be used to trace deadlocks, unspecified recep-
          tions, timing problems, errors caused by value passing, and
          violations of user-specified `assertions.'

          Pret reads the protocol specifications for a set of inter-
          acting processes from the file specified, checks its syntax
          and completeness, and prepares a file pret.out for the ana-
          lyzer containing a finite state machine description of the
          protocol.  Under option -v pret lists the numbers of states
          in the state machines, reports if any states are unreach-
          able, and lists the queue sort for each message queue

          Tracing Options:

          In most cases the options c, f, l, and v will suffice to
          perform protocol 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 experimental.

          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 occur 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 interleaving of process
               executions. See also option x.

          c N  Invoke a class N validation, where N can be chosen

     TRACE(1)                     (arend)                     TRACE(1)

               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 brack-
               eted message indicates a message sent but not received
               at the time of the error.  F gives a time ordered queue
               history, where each column corresponds to a queue, and
               each line to a time step.

          i    Ignore variables.  Second order state space folding

          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

          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 graphi-
               cally.  Do not perform an analysis.

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

          v    Verbose.  List execution times, size of the state

     TRACE(1)                     (arend)                     TRACE(1)

               space, number of levels searched, etc. at the end of
               the run.

          x    Perform a fast partial search. At each step in the
               analysis select 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 opera-

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