Urpal subversion repository

To enter: choose a language and click the link below.

The web interface allows the repository to be browsed online. The source code can be examined, logs can be read, and different revisions can be compared with one another. Ready-to-run versions of the software, and the source code for the latest release can be downloaded from the main page.

The web interface should work with most web browsers. Opera and Firefox should both work prefectly. As for IE, the appearance is best under version 7.x or greater, but version 6.x should be functional.

Unfortunately, the server hosting this website does not support WebDAV, so it is not possible to access the repository directly (for checkout or diffs).

This page contains:

• The link above to the source code repository.
• The software required for compilation,
• Instructions for compilation.
• Descriptions of all modules, with potential improvements described.

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

1. Edit unix-path-map, setting the SML_FXP path.
2. cd src
3. make clean
4. 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.

1. cd src
2. Edit the root variable in fxlib.ml.
3. Edit the root variable in smlnj-lib.ml.
4. Edit the root variable in mlyacc.ml.
5. Start Poly/ML (poly).
6. 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. 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.

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.

cmdlang

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

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

This module is specific to Urpal.

config

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

graphviz

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

Types and functions for dot files, including repesentation (dot.sig, dotfn.sml, *_attribute.sig), and pretty-printing (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 subraph attributes.

Types and functions for the plain format, including representation (plain.sig), pretty-printing, and parsing (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.sig, 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 x11_color.sig and structure x11color.sml for manipulating X11 colour names. These files would be in a separate module except that they are only used by the graphviz components.

The multiplication of *-graphviz*.sml and *-signal*.sml structures is unfortunate, but required for compatability across different environments. There is probably a better way to do this; if even to preprocess files.

layout

The beginnings of a generic interface for visual formatting of Uppaal models. More work is needed to make this module generic and reusable.

One good feature would be to reduce the number of nails introduced by Graphviz, particularly by omitting several that occur close together.

lib

Utility functions that do not fit anywhere else. Including a file position abstraction used in the lexers (file_pos.sig, filepos.sml) and some oft-used shortcuts over atoms (symbol.sig and symbol.sml).

maketest

This module implements the testing construction described in this paper.

It has improved greatly over time but another refactoring is probably required to:

• Handle/rename bindings more generically and automatically.
• Remove the redundant routines for the old ‛partitioning’ algorithm (see negatePartitionedTransitions in transitionflipper.sml, see UNSW-CSE-TR-0723). This has not been done before now in case further comparisons of the two approaches are required.
• Rationalise/tidy the functions that handle urgent channels.
• Make clock expressions and associated manipulations a separate and more generic unit, possibly placing them in the uppaal module.

mcs51

Simple-minded routines for parsing MCS51 (aka 8051) assembler and creating rudimentary Uppaal models.

These functions exist more as an example of how the other modules can be combined for useful effect rather than as a proposal for a practical model-checking of assembly programs. The lexer, parser, and data structures may form a good starting point for other programs that manipulate MCS51 assembly code.

uppaalxml

Types and routines for parsing, representing, and manipulating the Uppaal XML file format. These form, together with those in the uppaal module, an alternative in Standard ML to libutap. They could be useful for building other programs that manipulate Uppaal models.

The files nta.sig, nta_output.sig, nta_types.sig, nta_types_output.sig, ntafn.sml, and ntaoutputfn*.sml express and manipulate the basic structure of an Uppaal NTA file. (Unfortunately ntaoutputfn.sml and ntaoutputfn.nj.sml are duplicates but for argument constraints, to work around a flaw in SML/NJ's behaviour.) There are two concrete instantiations: one, textnta.sml, where expressions on transitions, functions, etcetera, are uninterpreted text, and another, parsednta.sml, in the uppaal module in which they have been parsed into datatypes.

The other files interface with the FXP XML parsing library. The flat-1_1.dtd file, which the parser uses to validate its input, is currently read from a local path. Configuration would be simpler if it could be built into the parser, but this does not seem to be possible without modifying the FXP routines. No attempt is currently made to download this file automatically, although FXP supports such a feature.

The files xml_writer.sig and xmlwriter.sml plug into the Basis library I/O routines for escaping certain characters (<, >, &, ", and ') when outputting XML. They are reusable of themselves.

uppaal

Types and routines for parsing, representing, manipulating, and pretty printing the Uppaal command language. There are three main parts: expressions, declarations, and environments. Each has routines for pretty printing *pp.sig/sml and conversion to strings *cvt.sig/sml.

The lexer uppaal.lex and parser uppaal.grm turn uninterpreted Uppaal expressions and commands into expression and declaration types. The files uppaal_parse.sig and uppaalparse.sml perform some semantic analysis─but not full type checking─using an environment environment.sig/sml.

The expression structure has a unresolvedty mechanism for handling array declarations like int A[T] where T could be a typedef, like typedef int[0,3] T, or a constant parameter. The mechanism exists because parsing and semantic analysis are strictly separated. A more principled alternative would be to have two signature/structure pairs: one for parsed expressions, the other for analysed expressions. The shared declarations could be factored out into a functor.

The environment structure requires refactoring.

Other ideas

• Integration with a theorem prover, such as Isabelle to double-check or justify manipulations of automata and expressions.
• Exploit the term-rewriting module of Isabelle or similar.