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