UPPAAL 5 Features

Uppaal 5 integrates the following features:

• Symbolic model-checking (Uppaal 4.0),
• Controller synthesis using timed games (Uppaal TIGA),
• Performance estimation using statistical model-checking (SMC, since Uppaal 4.1.19),
• Optimization using learning (Stratego).

Most of the new features have been incubated in Uppaal Stratego branch which is about to be phased out.

The following is a list of new features since 4.1.26 release.

Menus and Preferences

Open Example menu to access the demo examples quickly:

Open Recent menu: just like Open Example but remembers the last 15 model files.

JetBrains Mono fonts with code ligatures where <= is displayed as ≤ and --> as ⟶:

Look & Feel themes, in particular modern FlatLaf:

However, light attracts bugs, therefore there are fewer bugs with FlatLaf Dark theme:

Zoom-in and zoom-out plots when using JFreeChart:

Uppaal 5 comes with refactored engine protocol using JSON message format with better error messaging and handling.

Advanced users may want to select an engine running on a remote computer:

Editor

Find/replace dialog via Edit⟶Find/Replace or press Ctrl F / Ctrl R (macOS: ⌘F / ⌘R):

Find/replace globally via Ctrl Shift F / Ctrl Shift R (macOS: ⌘⇧F / ⌘⇧R):

Automatic parenthesis matching and indentation in Advanced editor mode:

Symbolic Simulator

Coverage highlighting using heat-map intensity colors:

Concrete Simulator

Support for dynamical systems (models with ODEs) and variable value trajectories over the simulation trace:

Stochastic simulation which adheres to the model-specified probabilities:

Stochastic simulation using the selected strategy:

Verifier

Controller synthesis (using timed games):

Performance optimization using learning:

Query-specific custom engine options:

Demo Models

Stratego:

• Train gate controller synthesis train-gate-strat
• Cat and Mouse cat-and-mouse
• Adaptive Cruise Control cruise
• Newspaper sharing newspaper
• Travel through rush hour traffic traffic