Skip to main content.

This page’s menu:

Presentations

Tutorials

External Contributions

Frequently Asked Questions

In this section we collect frequently asked questions (and answers) about Uppaal2k.

  1. How do I get started with Uppaal?
    The are some tutorials to get you started. You should also study the examples in the demo directory, created during the installation, and read the documentation available from the Help menu in Uppaal.
  2. How do I run Uppaal 4.0 in compability mode?
    There is a mode for compability with Uppaal 3.4, which can be enabled by defining the environment variable UPPAAL_OLD_SYNTAX. Set the variable to any value, and restart Uppaal for the setting to take effect. Remove the variable from the environment to get back to normal 4.0 operation.
  3. Will I be able to use system descriptions stored in .ta- or .atg-format in Uppaal?
    .ta- and .atg-files are old file formats used in earlier versions of Uppaal. The current file format, used since version 3.2, is based on XML and uses the extension .xml. Version 3.0 included a conversion tool from .atg-files to .xta format used in that version. The current version can open .ta- and .xta-files directly, use Open System in the File menu. Since version 3.4 the standalone verifier verifyta is able to read .ta-, .xta- and .xml-files directly.
  4. Can Uppaal save system descriptions in .ta- or .atg-format.
    No, since version 3.4 there is no support in Uppaal for saving .ta- or .atg-files.
  5. Can system descriptions and system requirements created in GUI be analysed with the stand-alone verifier verifyta?
    Yes, verifyta can handle files in the .ta-, .xta- and .xml-formats as well as the .q-format.
  6. What is the semantics of urgent locations?
    The semantics of an urgent location is the same as: introducing a new clock; reset the new clock on all in-going transitions to the location; and add a conjunct to the location invariant requiring the new clock to be <=0. Intuitively, this forces the process to leave an urgent location without delay.
  7. How do I run the GUI locally connected to a remote verification server?
    Assuming that the verification server is running on machine xxx.yyy.zzz and listening for connection socket 2350, use the command "uppaal2k -serverHost xxx.yyy.zzz -serverPort 2350".
  8. How do I start a verification server that accepts remote connections?
    Run the socketserver with no arguments to start a server that accepts remote connection on socket 2350. Use the command line option -p to configure the server to listen on another socket. The socketserver is only availabe on Linux and SunOS.
    Note: there is no authentication performed, meaning that anybody aware of the running server, can connect to it. The server may also be vulnerable to acodeacks.
  9. When loading a project, I get the error message "Could not connect to server". What's wrong?
    First, check the status log on the verification tab in the GUI. It might contain additional information. If you are using a remote verification server, see the entries about remote servers.
    If you are running with a local verification server check that the GUI can find the server executable and that you have permisson to execute the server binary. If you are using Linux or Solaris you may also try to execute the verification server manually from the command prompt. See the above answers on how to do this. If you use the default port of 2350 and execute the GUI and verification server on the same host, you do not need to add additional options when starting the GUI.
  10. I try to run Uppaal in Windows by clicking on the file uppaal.jar, but WinZip is opened instead. How do I run Uppaal in Windows?
    It seems that winzip has "stolen" the file association for jar files. You can either try to fix the file association for jar files (it should run 'javaw -jar') or simply reinstall java.
  11. How do I produce colored .eps-files of an automaton?
    Normally, Uppaal produces gray-scale eps-files. It is possible to instruct the tool to generate colored eps-files by using the command line option -psColors on.
    To produce an eps-file of a template, use item Save Postscript of the Templates menu. To produce an eps-file of a process (as shown in the simulator), use Save Postscript in the pop-up menu of the process (activate the pop-up menu by right-clicking the process in the simulator).
  12. How do I force Uppaal's GUI to use a specific language?
    • Under Linux (from 4.0.7 & current internal dev version): use LANG=[code] ./uppaal, where code is the language code of a supported language, currently en, zh, ja, da, lt, ru. If the environment defines the LANG variable to follow some standard it will also work, like ja_utf8..
    • Under Windows: make a shortcut to uppaal.jar, edit the command of the shortcut to java -Duser.language=[code] -jar <path to uppaal.jar>.
  13. How do I export and interpret the traces from Uppaal?
    There are three ways of extracting the traces:
    1. Textual format: use command line utility verifyta to produce the trace in human-readable state-transition format. The utility is distributed together with Uppaal and found in a bin-* directory. Type verifyta -h inside shell (cmd.exe on Windows) to see further options.
    2. C++ API: export the trace as .xtr file and then interpret it with tracer utility from UTAP library.
    3. Java API: use model.jar library included in lib directory of the Uppaal distribution. The java-doc is included in lib/model-javadoc.jar and thus can be imported into IDEs such as Eclipse and Netbeans. Uppaal distribution also includes demo/ModelDemo.java code showing how to manipulate the model, import, export traces and how to interact with simulator and model-checking APIs of the engine.
  14. How do I switch to Java 6 on Mac OS X?
    On Mac OS X 10.5 the default Java virtual machine is Java 5. To switch to Java 6, run /Applications/Utilities/Java/Java Preferences.app and select Java 6. From version 4.0.7, Uppaal will not run on Mac OS X 10.4 and Java 6 is not available on that platform.
  15. Running UPPAAL on Mac OS X I get the error java.io.FileNotFoundExceptino: /Volumes/uppaal/UPPAAL.app/Contents/Resources/Java/license.txt (Read-only file system). What is the problem?
    You are probably running UPPAAL from a dmg file. Please move the content of the dmg file to a readable disc, e.g. to your /Applications directory on your system volume, or a directory on your Desktop.
  16. UPPAAL freezes on Mac, what do I do?/
    On Lion or Mountain Lion, the GUI may freeze. Update your Java on this link.
  17. You cannot install UPPAAL on Mac OS Lion or later.
    • Delete the dmg file you downloaded.
    • Open Preferences.
    • Open Security and Privacy.
    • Select "Allow applications downloaded from: " anywhere.
    • Download UPPAAL again and install.
    If you still have problems, consult this link for more help.
  18. How do I use UPPAAL through a proxy?
    If you are using Windows. Locate the installation directory of UPPAAL. Create a shortcut to uppaal.jar and give it the name you want. Edit the shortcut and change the command line used. You should see java -jar "C:\...\uppaal.jar". Change it to

    java -DproxySet=true
    -Dhttp.proxyHost=proxyhostURL
    -Dhttp.proxyPort=proxyPortNumber
    -Dhttp.proxyUser=someUserName
    -Dhttp.proxyPassword=somePassword
    -jar "C:\...\uppaal.jar"
    where you fill in the information concerning your proxy. You need to enter your user name and password only if you need to login on the proxy, otherwise remove the two corresponding definitions.

    If you are using Linux or Mac. Locate the installation directory of UPPAAL. Edit the script uppaal and add

    -DproxySet=true \
    -Dhttp.proxyHost=proxyhostURL \
    -Dhttp.proxyPort=proxyPortNumber \
    -Dhttp.proxyUser=someUserName \
    -Dhttp.proxyPassword=somePassword
    to the JAVA_DEF default option definition at the beginning. The '\' are here to break lines. Do no add any character after '\'. Fill the needed information on your proxy and remove the definitions for user name and password if they are not needed for your proxy.
  19. How do I fix damaged images under Mac OS X Lion?
    Actually the images are not damaged but the application gate keeper on Lion must be setup. Delete the images you have. Configure the gate. Then re-download the images and it will work.
  20. Why does UPPAAL simulator, verifier, server and/or verifyta crash almost immediately?

    Possible cause: UPPAAL cannot access a license in uppaal-version.number/license.txt file, tries to fetch the license over the internet and create a file, but it fails in some step.

    Symptoms:

    • Older 32bit releases (TIGA, ECDAR) are being run on new 64bit Linux host.
    • Verification does not start and brings "server connection lost" instead.
    • verifyta and/or server does not start but says "internet connection required for activation"
    • Diagnostic runs with strace server finish with lots of "file not found" messages upon looking up 32bit libraries like /lib32/libc6.so, /usr/lib/libnss.so and so on.

    Possible fixes:

    • Make sure that the computer has a working internet connection, e.g. check with a command ping bugsy.grid.aau.dk, inspect the network interface (use command ifconfig or ipconfig).
    • Make sure that the installation directory uppaal-version.number has write permissions, e.g. use ls -ld . command to inspect the permissions, touch license.txt should succeed inside the UPPAAL installation directory.
    • On 64bit Linux host, install 32bit libc library to enable networking support for 32bit binaries, e.g. sudo apt-get install libc6:i386 (you may need to enable i386 architecture in /etc/apt/sources.list, sudo apt-get update and then sudo apt-get install libc6:i386).
  21. Attempt to export graphical images results in internal error "org.freehep.graphicsbase.util.export.ExportFileType is not an ImageIO SPI class"

    FreeHEP library is broken since Java 9. A workaround is to install and use Java 8.

  22. Floating point variables and operations are ignored in symbolic queries or the verification of such queries crash the engine

    Floating point operations are not supported by the symbolic analysis (only integers are allowed). The only valid use of floating point operations is when they are used to model dynamical cost and does not influence the behavior of the model, i.e. the floating point operations can be safely abstracted away.

    Dynamical cost can be modeled by hybrid clock variables using floating point operations which have effect in Stratego queries.

  23. When started on a command line, Uppaal produces the following warnings: 
    WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.uppaal.gui.Main (file:/opt/local/uppaal-4.1.24/uppaal.jar) to field sun.awt.X11.XToolkit.awtAppClassName
WARNING: Please consider reporting this to the maintainers of com.uppaal.gui.Main
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release

    The warning is harmless and can be ignored.

    The reason is that Uppaal is trying to set the application name for the Window Manager to display in the application bar, but it is using the internal Java API to achieve it. Java ≥9 implements checks for such access and warns against it because internal API does not have any guarantees for continued support. Unfortunately Java does not provide an alternative way of setting the application name.

Published Material

Incomplete list of publications related to Uppaal.