Using Uppaal for trace interpretation

Uppaal is a model checking tool for timed automata. When a counterexample is generated by Uppaal, or when a random / manual trace is present in the Simulator, it is able to save the trace in Uppaal’s .xtr format. However, this format is human-unreadable. This article records the steps to compile and use the tracer utility for showing Uppaal traces outside of the GUI. Assuming we are working under the Ubuntu 11.04 environment.

Installing Necessary Packages

The libboost-dev and libxml2-dev packages are needed by the Uppaal Timed Automata Parser Library.

sudo apt-get install libboost-dev libxml2-dev

Compiling the UTAP library

The installation is a simple process as usual.

./configure
make
make check
sudo make install

For some reasons, however, there are errors when compiling the code. Essentially there are three groups of things to fix.

1. #includes in the source sometimes include string, which should be modified to string.h for some functions like strcmp, and strncpy to work.
2. There are missing #includes so that certain functions do not work. E.g., the for_each function is in the algorithm package of Boost but not properly included.
3. Some type definitions are not found, such as int32_t. Changing this to int works fine for the moment.

Once these are fixed, the installation process went through smoothly.

Using the tracer Utility

The tracer utility takes a Uppaal intermediate format and a saved .xtr file as the only two inputs. To get the Uppaal intermediate format for a model in the .xml format, one should use

UPPAAL_COMPILE_ONLY=1 verifyta model.xml - > model.if

The dash here is a placeholder for the query file, which is not necessary for intermediate format generation but helps pass syntax check by verifyta.

With the generated intermediate format, one can reconstruct the trace is a readable format.

tracer model.if trace.xtr

Also, one can use the pretty utility to pretty-print a Uppaal model in a C-like format.

pretty model.xml

Update: Compiling the UTAP library under MacOSX

Under Mac OS X, the boost library is not by default available (if it is installed separately, with MacPorts for example). If this is the case, it is necessary to add options to ./configure as follows.

./configure LDFLAGS=-L/opt/local/lib CXXFLAGS=-I/opt/local/include

Update: Issues with aclocal.m4

For some unknown reasons the aclocal.m4 file changes quite a bit; it even changes from plain text to binary files. This makes the compiling process fail. Just replace it with the pristine version that comes with the libutap library and the compiling should be fine.

Downloading and configuring Java Pathfinder

Downloading and Installing

First install Mercurial.

sudo apt-get install mercurial

Then grab the source for jpf-core and jpf-symbc packages. They are the main files for Java Pathfinder.

hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc

Site Configuration

Create a site configuration file with the name ~/.jpf/site.properties.

# JPF site configuration

jpf-core = ${user.home}/Software/jpf/jpf-core

# numeric extension
jpf-numeric = ${user.home}/Software/jpf/jpf-numeric

# symbolic extension
jpf-symbc = ${user.home}/Software/jpf/jpf-symbc

extensions=${jpf-core},${jpf-numeric},${jpf-symbc}

#... and all your other installed projects

Building Java Pathfinder

cd jpf-core
bin/ant test
cd ../jpf-symbc
bin/ant test
cd ../jpf-numeric
bin/ant test

Installing the Eclipse plugin

Use Eclipse 3.5+ and Java 1.6+, and this update site link: http://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/install/eclipse-plugin/update/
To find out that it is properly installed, see in the preference window if there is a page for Java Pathfinder.

Tips on customizing Windows 7 (to be continued)

• Change Windows Explorer to Open My Computer Instead of Libraries Folder in Windows 7

Configuring a Windows machine with necessary installations

Here is a list of software to install on a new Windows machine.

• Google Chrome
• Firefox (See a list of extensions here)
• CTeX
• Emacs
• Aspell
• GnuWin32
• SecureCRT
• FileZilla
• 7-Zip
• Foxit Reader
• Java SDK
• Eclipse (See a list of plugins here)
• TortoiseSVN
• Python
• Skype
• Dropbox
• VirtualBox
• Notepad++
• Semantic Endpoint Protection
• Microsoft Visual Studio
• Uppaal
• Freemind
• JabRef
• Fonts: Liberation, Ubuntu, BitStream

Must-have firefox extensions

Here is a list of Firefox extensions that I cannot live without.

• Download Status Bar
• Adblock Plus
• Flagfox
• ActiveInbox for Gmail
• Colorful Tabs
• LeechBlock

Additionally, here are some more useful ones. I am not sure they are updated often to come up with Firefox 5 now.

• BBDict
• CHM Reader
• Delicious Bookmarks
• Firebug
• FireGestures
• FireShot
• Google Notebook
• Greasemonkey
• IE Tab
• Speed Dial
• Tab Mix Plus
• Web Developer

Emacs configurations — AucTeX

Here is the setting for working with Emacs and AucTeX under MS Windows.

;;; auctex
;; (add-to-list 'load-path "~/.emacs.d/site-lisp/auctex-11.85")
(load "auctex.el" nil t t)
(require 'latex)
(require 'tex-site)
(require 'tex-mik)

;; Set the default PDF reader to SumatraPDF. The executable should be in PATH
(setq TeX-view-style (quote (("^epsf$" "SumatraPDF.exe %f") ("." "yap -1 %dS %d"))))

(setq TeX-output-view-style 
      (quote 
       (("^dvi$" "^pstricks$\\|^pst-\\|^psfrag$" "dvips %d -o && start %f") 
        ("^dvi$" "." "yap -1 %dS %d") 
        ("^pdf$" "." "SumatraPDF.exe -reuse-instance %o") 
        ("^html?$" "." "start %o"))))

;; Some helpful settings
(setq TeX-auto-untabify t)
(setq TeX-auto-save t)
(setq TeX-parse-self t)
(setq-default TeX-master nil)
(setq TeX-electric-escape t)
(setq-default TeX-PDF-mode t)

(add-to-list 'LaTeX-indent-environment-list '("tikzpicture"))
(add-to-list 'LaTeX-verbatim-environments "comment")

;; Start RefTeX
(add-hook 'LaTeX-mode-hook 'turn-on-reftex)
(add-hook 'latex-mode-hook 'turn-on-reftex)
(setq reftex-plug-into-AUCTeX t)

Compiling Maude 2.5 under Ubuntu 10.04

To compile Maude, a few prior packages need to be installed.

build-essential and related utilities

dpkg -l build-essential
sudo apt-get install build-essential bison flex libncurses5-dev

GNU gmp

First grab the package from its site here. Untar and install.

wget ftp://ftp.gmplib.org/pub/gmp-5.0.1/gmp-5.0.1.tar.bz2
tar xvf gmp-5.0.1.tar.bz2
cd gmp-5.0.1/
./configure --enable-cxx --disable-shared
make check
make
sudo make install

The whole process may take a while.

GNU libsigsegv

sudo apt-get install libsigsegv0 libsigsegv-dev

Tecla

Download from here and do the usual stuff.

wget http://www.astro.caltech.edu/~mcs/tecla/libtecla.tar.gz
tar xvf libtecla.tar.gz
cd libtecla/
./configure CFLAGS="-O2 -D_POSIX_C_SOURCE=1"
make TARGETS=normal TARGET_LIBS=static
sudo make install

BuDDy

Same stuff for BuDDy from SourceForge.

wget "http://sourceforge.net/projects/buddy/files/buddy/BuDDy 2.4/buddy-2.4.tar.gz/download"
tar xvf buddy-2.4.tar.gz
cd buddy-2.4/
./configure --disable-shared
make
sudo make install

Maude

Now it is possible to build Maude from scratch. The steps are similar, but just remember to use the libraries that we just compiled, rather than the ones that (possibly) come by default.

wget http://maude.cs.uiuc.edu/download/current/Maude-2.5.tar.gz
tar xvf Maude-2.5.tar.gz
cd Maude-2.5.tar.gz/
mkdir Build
cd Build/
../configure GMP_LIBS="/usr/local/lib/libgmpxx.a /usr/local/lib/libgmp.a"
make
make check
sudo make install

The make step may take a while, just be patient.

Setting up Emacs Maude mode

After compiling and installing Maude, it may be helpful to set up Emacs so that experiment with Maude is easier. First download the Emacs Maude mode from SourceForge. Put it in your load path, and then add the following to a file maude.el under .emacs.d folder so that it is loaded by Emacs.

(autoload 'maude-mode "maude-mode" "MAUDE mode" nil t)
(setq auto-mode-alist
      (append
       (list (cons "\\.maude$"  'maude-mode)
		     (cons "\\.fm$"     'maude-mode))
       auto-mode-alist))
(setq maude-command "/usr/local/maude/maude.linux")

Defining SSH host aliases for shorter command line typing

Add to (or create) the file ~/.ssh/config the following lines can define alias for ssh hosts.

Host alias
  HostName the.real.host.name
  User yourid

Setting up Apache 2 server on Ubuntu 10.04

This post is from the official page, tailored for personal use. The basic steps are here.

1. Copy the default site settings file /etc/apache2/sites-available/default to a new one at the same place, say testsite.
2. Edit the file with new information. Change the DocumentRoot and the Directory settings.
3. Disable the default one and enable the new one: sudo a2dissite default && sudo a2ensite testsite
4. Restart Apache 2: sudo apache2ctl restart
5. And the index.html or index.php files are good to go.

Now it’s a time to use your imagination for a new site.

Sharing files between Ubuntu machines

Recently I need to reinstall one of my machines so that backing up is a problem. My removable disk is old and unreliable, and the large amount of files cannot fit into any online storage systems (including school Eniac account). The simplest possible solution is to use SSH.

1. Use ifconfig on the host machine to figure out its ip address.
2. On client machine, use the normal Connect to Server… option to connect. The parameters are straightforward.

That’s it! Enjoy!