Urpal

Urpal is your pal for Uppaal.

Urpal takes an Uppaal model as input, performs manipulations as described by a simple command language, and writes the resulting model back to a file. Its prime feature is the ability to construct a testing automaton for determining trace inclusion for a restricted class of timed automata. Uppaal can also: duplicate automata; create automata ready to accept all synchronisations on a set of channels; prune transitions based on their action label; conflate, drop and rename locations; and scale the graphical layout of a model. More details are in the manual page.

main website

Descriptions of the testing construction can be found in:

• The thesis of Mariëlle Stoelinga, specifically Chapter 7 and Appendix A. Development on Urpal began from her descriptions at the suggestion of Frits Vaandrager.

• The Scaling up Uppaal paper of Henrik Ejersbo Jensen, Kim Guldstrand Larsen, and Arne Skou. Urpal incorporates their construction for handling urgent locations and shared variables.

• The paper by Arcot Sowmya and me, to be presented at EMSOFT 2008. This paper presents several improvements to the original CSE technical report (UNSE-CSE-TR-0723).

The testing construction cannot be performed on all timed automata, specifically several modelling features are not supported:

• non-deterministic automata (this assumption is not checked),
• non-synchronizing (τ) transitions,
• committed locations,
• process priorities,
• channel priorities,
• inputs on broadcast channels,
• some combinations for forall and select bindings (see this paper).

The software was developed at the The University of NSW and NICTA. It is released under a BSD License. Urpal uses technology developed with the imagination and ideas from NICTA, Australia's ICT Centre of Excellence. The source repository can be browsed online.

This software is provided as a prototype only: use at your own risk! It surely contains faults, please report them.

Graphviz is required to run Urpal. The source code has additional compilation dependencies.

Building Urpal

Software required for Compilation

Urpal relies on several external libraries:

• The Standard ML Basis Library.

• The Fxp XML parser.

• Parts of the SML/NJ libraries as distributed with SML/NJ and MLton, and readily adapted for Poly/ML, including ML-Yacc and ML-Lex.

A compiler or interpreter is also required. Urpal was developed with SML/NJ, but MLton is used to compile the binaries (cross-compiling with mingw for windows). Poly/ML can also be used. Instructions for each of the three systems follow.

Compilation

Compilation interdependencies are specified over various files:

• *.cm: for SML/NJ
• *.mlb: for MLton
• *.ml: use commands for Poly/ML

Compilation has only been tested on Linux and FreeBSD, but I am happy to help getting it to work under Windows.

Both ML-Yacc and ML-Lex are normally required to turn the *.grm and *.lex files into SML code, but the source distribution includes files generated with SML/NJ that also work with Poly/ML. Otherwise, the relevant files can be produced with: make lexfiles grmfiles.

SML/NJ

SML/NJ must be provided with the path to the Fxp sources. One possibility is add a line to $HOME/.smlnj-pathconfig:

fxlib.cm	    /usr/lib/sml-fxp/src

To build an executable: cd src; make.

To load into an interactive session:

cd src;
sml
CM.make "sources.cm";

Only the structures Urpal and Settings, and the signature SETTINGS are imported.

MLton

• Edit src/unix-path-map, setting the SML_FXP path.
• cd src
• make clean
• make withmlton

Note: Compiling first with SML/NJ and then with MLton may fail because the lexer produced by the former is not acceptable to the latter. Running make clean before compilation with MLton fixes the problem.

Poly/ML

~~Urpal cannot currently be compiled in Poly/ML due to an internal error.~~

The ML-Yacc and SML/NJ libraries must be adapted for Poly/ML.

• cd src
• Edit the root variable in src/fxlib.ml.
• Edit the root variable in src/smlnj-lib.ml.
• Edit the root variable in src/mlyacc.ml.
• Start Poly/ML (poly).
• Import Urpal: use "urpal.ml";

Other

The core SML language is standardised and, ignoring implementation flaws, always works as expected across different compilers and interpreters. There are, however, two major obstacles to portability. Several environments were available before the SML Basis Library was finalised, and thus the interfaces of ageing environments do not always comply with the final standard</a>. More problematic is that some library implementations are incomplete, even omitting required signatures and structures. The second obstacle is the existence of several systems for compiling multiple SML files into a single system. For these reasons, Urpal cannot be executed in all environments. Those explicitly not supported are:

• SML.net: lacks functional I/O (TextIO.StreamIO).
• Moscow ML: lacks functional I/O (TextIO.StreamIO), requires filename changes.

Execution has not been attempted with Alice, HaMLet, MLKit, or SML#. Comments or instructions would be gratefully accepted.

Modules

The program is built from several interdependent modules. There is a separate subdirectory in src for each, except main whose files are stored at the root. The modules are listed below with brief descriptions and notes for possible improvement.

There is usually one source file per signature, structure, or functor. The files follow a simple naming pattern:

• cmd_lang.sig contains the definition of the CMD_LANG signature.
• cmdlang.sml contains the structure CmdLang which provides the primary implementation of CMD_LANG.
• plainfn.sml contains the functor PlainFn. All functor names end with Fn.

Module: Main

The main structure that dispatches program options to subroutines is given in urpal.sml; the expression in main.sml invokes the relevant function with arguments from the command line. Command line options are parsed by commands.sml.

The various settings files parse and create urpalrc files, and store global program settings. Currently it is difficult to add new settings; this should be fixed.

The file util.sml contains functions for printing debugging messages, warnings, and errors. It could be better named.

Module: Cmdlang

Implements the expression language used to specify manipulations of Uppaal models. A lexical analyser cmdlang/cmdlang.lex and parser cmdlang/cmdlang.grm are driven by cmdlang/cmdlang.sml.

There are probably many other useful manipulations of Uppaal models that could be implemented.

This module is specific to Urpal.

Module: Config

A generic module for parsing hierarchical configuration files, following the syntax of Reppy's ML-Doc.

Module: Graphviz

Generic functions for interacting with Graphviz. With enhancements, this module would make a good separate library.

Types and functions for dot files, including representation (graphviz/dot.sig, graphviz/dotfn.sml, *_attribute.sig), and pretty-printing (graphviz/dotppfn.sml), but not parsing. There are some limitations: anonymous subgraphs cannot be used in edges (no n1 -> subgraph {...}), and there are no explicit types for cluster or subgraph attributes.

Types and functions for the plain format, including representation (graphviz/plain.sig), pretty-printing, and parsing (graphviz/plainfn.sml). General HTML labels (multiple tags) are not supported.

There is an interface for invoking Graphviz commands as subprocesses and parsing the results: graphviz/graphviz.sig, graphviz/graphvizfn.sml. The functor allows specialisation for Unix or Windows. Support for the latter is fudged because the Basis library Windows structure is not frequently implemented. More fudging is required to handle word size differences between MLton and SML/NJ.

A simple signature graphviz/x11_color.sig and structure graphviz/x11color.sml for manipulating <a href="http://en.wikipedia.org/wiki/X11_color_names">X11 colour names</a>. These files would be in a separate module except that they are only used by the graphviz components.

The multiplication of [*