License

Please read the license agreement carefully. The text of the agreement follows:

We (the licensee) understand that UPPAAL includes but is not limited to the programs: uppaal.jar, model.jar, editor.jar, uppaal, server, socketserver, verifyta, atg2ugi, atg2ta, atg2hs2ta, hs2ta, checkta, simta, tron, and that they are supplied "as is", without expressed or implied warranty. We agree on the following:

1. You (the licensers) do not have any obligation to provide any maintenance or consulting help with respect to UPPAAL.
2. You neither have any responsibility for the correctness of systems verified using UPPAAL, nor for the correctness of UPPAAL itself.
3. We will never distribute or modify any part of the UPPAAL code (i.e. the source code and the object code) without a written permission of Wang Yi (Uppsala University) or Kim G. Larsen (Aalborg University).
4. We will only use UPPAAL for non-profit research purposes. This implies that neither UPPAAL nor any part of its code should be used or modified for any commercial software product.

In the event that you should release new versions of UPPAAL to us, we agree that they will also fall under all of these terms.

Requirements

• Operating system: Microsoft Windows or Linux on Intel architecture.
• Graphical frontend needs Oracle Java SE Runtime Environment: version 8 or newer.

Known Limitations

• Stratego pops-up with "$v_gameInfoPlay" message but does not load the strategy into the simulator.

Download Uppaal Stratego

The latest Uppaal Stratego is integrated into Uppaal 5 and is available on the main UPPAAL page in downloads section.

By downloading any version of Uppaal, you agree to the above licensing terms.

• 4.1.20-7 for 32bit Windows and Linux and for 64bit Linux.
• 4.1.20-6 for 32bit Windows and Linux and 64bit Linux.
• 4.1.20-5 for 32bit Windows and Linux and 64bit Linux.
• 4.1.20-4 for 32bit Windows and Linux.
• 4.1.20-3 for 32bit Windows and Linux.
• 4.1.20-2 for 32bit Windows and Linux.
• 4.1.20 for 32bit Windows and Linux.

Installation Instructions

1. Download the distribution archive from the Download section above.
2. Unpack the archive by right-clicking the archive, choosing Extract menu and following the extraction dialog.
3. Visit the extracted directory.
4. Create startup shortcuts in Programs menu and Desktop by launching AddLinks.vbs script.
5. Use the shortcuts from Programs menu or Desktop to start graphical frontend.
6. Alternatively, start the graphical frontend by double-clicking on uppaal.jar (or uppaal startup script in Linux).
7. Alternatively, start the graphical frontend from command line prompt: java -jar uppaal.jar
8. Alternatively, use the command line utility verifyta in either bin-Win32 or bin-Linux.

Version History

The latest Uppaal Stratego is available on the main Uppaal page with version history.

• December 6, 2019. Version 4.1.20-7 released.
  

    - Fixed engine protocol memory bug (server binary was crashing on Windows).
    - Fixed unicode encoding in engine protocol (GUI was showing mangled characters).
  

• October 10, 2019. Version 4.1.20-6 released.
  

    + Integrated Q-learning and M-learning methods.
    + Changed the engine protocol from "dot" format to JSON (the schema is not final).
  

• February 19, 2019. Version 4.1.20-5 released.
  

    + Added C-library functions, including fint() for float to integer conversion.
    + Loading external functions from dynamic library (DLL) into model code
      (papers demonstrating examples and use cases).
    + New simulation-engine for SMC and Stratego queries.
    - Fixed a number of floating point precision bugs.
    + Integration uses more stable Runge-Kutta method (see --truncation-error and --truncation-time-error) 
      bounded by a minimum delta (--discretization)
    + Improved static analysis and derived speedups for non-hybrid models.
    + Major refactor and stabilization of Stratego/Learning.
    + Fine-tuning of search-strategy (see --random-search-limit and --determnistic-search-limit).
    + Strategy output of learned strategies (available for --learning-method 1,3,4 and 5) 
      in JSON format with header describing mapping to system (see --print-strategies).
    + Manual feature-selection using the "{a,b,c}->{d,e,f}"-style notation (examples)
    + New learning algorithms (4+5) utilizing Q and M-learning (paper under review). 
      (options --qlearning-alpha, --split-upper-t, --split-lower-t, --split-ks, 
       --split-filter-rate, --split-filter-val, --discount, --indefference-smoothing 
       and --indefference-scale are unique to these methods)
    + Added layout checking for overlapping elements.
    + Added Dockerfile for MacOS and 64bit Windows (instructions in res/Docker.md).
    - Disabled rare event support via "Reach" and "Rare" queries.
  

  Known issues:

    - Missing strategy import
    - Missing strategy export for symbolic (TIGA) strategies
    - Missing translations/text strings of options and engine output
    - Missing documentation of new features in help-file
  

• November 10, 2016. Version 4.1.20-4 released.
  

    + Rare event support via "Reach" and "Rare" queries.
  

• April 14, 2015. Version 4.1.20 released.
  

    - Fixed symbolic simulator.
    - Canceling verification job preserves strategies.
    + Allow output synchronization on outgoing branches.
  

• November 19, 2014. Version 4.1.20 4th pre-release.
  

    + Enabled the editor to modify "controllable" property of edges.
    + Better default learning parameters.
    - Fixed crashing when loading new model.
  

• November 19, 2014. Version 4.1.20 3rd pre-release.
  

    - Fixed minimization expressions for learned strategies.
  

• November 19, 2014. Version 4.1.20 2nd pre-release.
  

    - Fixed engine options handling.
    + Updated newspaper.xml example with more comments.
  

• October 23, 2014. Version 4.1.20 1st prerelease.