UNTITLED                             LOCAL                            UNTITLED


NAME

     urpal -- manipulate Uppaal models from the command-line


SYNOPSIS

     urpal [-h -v -t] [-i file] [-o file] [-e commands] [-f scriptfile]
           [-s settings] [-c configfile]
     urpal [-s settings] [-c configfile] [--showconfig]
     urpal [-i file] [-o file] [-s settings] [-c configfile] [--testflip]


DESCRIPTION

     Urpal is your pal for Uppaal.  Urpal parses an XML file containing timed
     automaton templates, performs manipulations specified a simple command
     language, and finally writes the results back to file.  The prime feature
     is the ability to construct a testing automaton for determining trace
     inclusion for a restricted class of timed automata.  Urpal is also able
     to: duplicate automata; create automata to ready to accept all synchroni-
     sations on a set of channels; prune transitions based on synchronising
     action; conflate, drop and rename locations; and scale graphical repre-
     sentations.

     When constructing test automata, most, but not all, modelling features
     are supported.  Automata must be deterministic, the tool does not check
     this assumption, and every transition must be labelled.  Urgent locations
     are expanded by adding an additional clock and invariant constraint.
     Urgent channels and shared variables are addressed using the construc-
     tions of Jensen, Larsen and Skou (refer SEE ALSO).  Committed locations
     and broadcast channels are not handled (warnings are displayed).  Certain
     combinations of universal quantifiers, selection bindings, and channel
     arrays are rejected (refer Bourke and Sowmya, SEE ALSO).

   Settings
     Several tool parameters can be specified via configuration files.  Urpal
     checks for configuration files in order: INSTALLPREFIX/etc/urpalrc,
     $HOME/.urpalrc, and $CWD/urpalrc.  Settings are specified as name=value
     pairs.  Named hierarchical sections are written in the form
           section_name { ... }
     Comments follow the conventions of C, except that they may be nested,
     that is single line comments are written after a // and multi-line com-
     ments between /* and */.  Paths and strings are written between double
     quotes.  The available settings are
     dtd_path
             Path to the flat-1_1.dtd file giving the Uppaal Document Type
             Definition.  If not given, Urpal attempts to fetch the necessary
             information from the network at every run.
     max_label_width
             The wrapping length, as a number of characters, for transition
             labels.
     max_declaration_width
             The wrapping length, as a number of characters, for declarations.
     new_color
             The color, in #RRGGBB format, to use for new locations and tran-
             sitions when there is not a more specific setting.
     error_color
             The color to use for the Err location added by the maketest oper-
             ation, and for transitions to that location.
     urgent_chanloc_color
             The color to use for locations and transitions added by the
             maketest operation when handling urgent channels.
     split_shift_old, split_shift_new
             sections containing x and y entries.  When a location is `split'
             as part of the maketest urgent channel construction, these param-
             eters specify how far to shift the two components from the origi-
             nal location.  By default, the original location is left in place
             and the urgency testing location is positioned automatically, but
             often the result is not very pleasing.
     tabulate_shift
             A section containing x and y entries, specifying where to locate
             the results of tabulate, relative to the transition source loca-
             tion.
     graphviz
             Contains two subentries
             path    Locates the graphviz(7) installation directory, which
                     must contain a bin subdirectory.
             engine  Specifies which layout algorithm to use, either fdp(1) or
                     neato(1).  One will often give a better result than the
                     other for a given automaton.
     debug   Enable debugging output. 0=all, 1=very detailed, 2=detailed,
             3=outline, 4=none.

   Command language
     The environment is a set of name/value pairs.  It is initialized from the
     Uppaal model file, by creating an entry for each template, a channels
     entry containing all of the global channel names, and a variables entry
     containing all of the (non-const, non-clock) global variable names.  When
     command evaluation is complete, all templates in the environment are
     written to the output model file.  Command names cannot be used variable
     identifiers.  Each command must be terminated with a semi-colon.

     The basic commands are
     help    Show a list of expression operators.
     list    Prints out all template names, one per line.
     show    Prints out all variable names and values.
     show id
             Prints out the value of the specified variable.
     id = expr
             Evaluates the expression and assigns the result to the given
             variable.  This command can be used to duplicate templates, by
             assigning them to a new name.
     drop expr
             Removes the given identifier from the environment.
     writegraphics (expr, path, PS | Dot | SVG)
             Rudimentary graphics output.  The expression must evaluate to a
             template, whose depiction will be written to the given path in
             the specified format (Postscript, Graphviz dot, or Scalable Vec-
             tor Graphics format).
     quit    End an interactive terminal session.
     expr          Displays the result of evaluating the expression. Does not
                   alter the environment.

     All expressions have one of these types
     template
             Templates are read from, and written back into, Uppaal model
             files.
     nameset
             Names of locations or channels which are written between braces
             and separated by commas, e.g.  { a, b, c}.  It is not possible to
             specify individual elements of channel arrays, also operators
             like names and channels over approximate by returning the array
             name whenever a single element is referenced.
     actionset
             When naming channels, a limiting input or output direction may be
             specified after a name if the set is enclosed in bar-braces, e.g.
             {| a!, b, c? |}.  Name sets are automatically coerced into action
             sets as required.
     namemap
             Specify functions from names to other names, e.g.  { a -> b, c ->
             a, b <-> d }.  Any name not given is mapped to itself.  A double
             arrow indicates a swap, i.e.  { b <-> d } is shorthand for { b ->
             d, d -> b }.

     actionmap map
             Specify functions from actions to other actions, e.g.  {| a! ->
             b?, a? -> b!, c? <-> c! |}.  Name maps are automatically coerced
             into action maps as required.

     Several operators are available for constructing expressions
     acceptall(actionset)
                       Create an automaton that is always ready to synchronise
                       on the given actions.
     actions(template)
                       Gives an actionset of all actions occurring in the tem-
                       plate.
     channels(template)
                       Gives a nameset of all channels used within the tem-
                       plate (regardless of direction).
     conflate(template, namemap)
                       For each n -> n' in the namemap, all transitions to or
                       from n are shifted to n', and the former is removed.
     drop(template, nameset)
                       Removes all the named locations.
     maketest(template, nameset, nameset)
                       Constructs an automaton for testing trace inclusion
                       against the given set of channel names and variable
                       names respectively.
     maketest(template)
                       Defaults to the channels and globals variables, respec-
                       tively.
     multisecttime(template, factor)
                       Multiply clock comparison expressions in template by
                       factor, which may be either an integer literal or a
                       variable name.
     parameters(template)
                       Returns a nameset of non-const parameter names.
     renamelocs(template, namemap)
                       Simultaneous renaming of locations.
     renametrans(template, actionmap)
                       Simultaneous renaming of action labels.
     scale(template, float)
                       Scale the graphical representation of a template by the
                       given amount.
     setinitial(template, name)
                       Set the initial state.
     split(template, actionmap)
                       For each a -> a' split transitions labelled with a into
                       two transitions connected via a committed location.
                       The second transition will synchronise on a'.  Channel
                       arrays are not supported.
     tabulate(template, nameset)
                       Make a table of labels for all transitions leaving or
                       entering a location in the given set.
     template \ actionset
                   Automaton restriction: removes all transitions labelled by
                   an action in the set, and then any unconnected locations.
     set \ set     Set difference.
     set ++ set    Set union.

   Testflip mode
     The option --testflip exercises the flip function that underlines the
     maketest feature.  It reads an input file containing multiple sections
           1.   A comment section describing the test.
           2.   Declarations in the Uppaal description language.
           3.   Zero or more transitions, each containing three lines:
                1.   selection bindings,
                2.   synchronisation expression (all transitions must synchro-
                     nise on the same channel or array name),
                3.   guard expression.
                Lines should be left blank when empty.
     Sections are separated by a line containing two hyphens `--'.

     e.g.,
           Simple test with selects
           --
           clock c1;
           chan c[5][int[2,10]];
           --
           i : int[0,4], j : int[2,10]
           c[i][j]?
           c1>4
           --
           i : int[0,4], j : int[2,10]
           c[i][j]?
           c1 <= 3


OPTIONS

     -h      Display help for command-line options.

     -v      Show the version number.

     -t      Start an interactive terminal.  This is the default if no other
             commands are given.

     -i file
             Uppaal model file, in xml format, for input.

     -o file
             Path to write the resultant Uppaal model file.

     -e commands
             Given a sequence of commands directly.

     -f scriptfile
             Execute a sequence of commands from a file.

     -s settings
             Specify configuration settings directly.

     -c configfile
             Apply the given configuration file.

     --showconfig
             Show the current configuration options.

     --testflip
             Enter a special mode for executing flip test scripts.
     Command and configuration options are executed in sequence from left to
     right, multiple options may be given.  Only a single input and output
     file may be specified.


EXAMPLES

     List templates:
           urpal -i model.xml -e 'list'

     Construct the test automaton for a template P1:
           urpal -i model.xml -o result.xml -e 'maketest(P1)'

     Likewise, but exclude the a channel and make the result larger:
           urpal -i model.xml -o result.xml -e 'maketest(scale(P1, 2.0))'


SEE ALSO

     Timothy Bourke and Arcot Sowmya, Tool support for verifying trace
     inclusion with Uppaal, UNSW-CSE-TR-0723, Technical Report, November 2007.

     Marielle I.A. Stoelinga, Alea Jacta est: Verification of probabilistic
     real-time and parametric systems, PhD Thesis, Katholieke Universiteit,
     Nijmegen, April 2002.

     Henrik Ejersbo Jensen, Kim Guldstrand Larsen, and Arne Skou, Scaling up
     Uppaal: Automatic verification of real-time systems using
     compositionality and abstraction, Proc. 6th int. sym. Formal Techniques
     for Real-Time and Fault-Tolerance (FTRTFT), Springer-Verlag, 19-30,
     September 2000.

     graphviz(7)


AUTHORS

     Timothy Bourke <tim@tbrk.org>


BUGS

     The program has not yet undergone rigorous testing or review.  It is
     still very much an experimental prototype.

                               October 28, 2007