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
Look & Feel themes, in particular modern
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:
Find/replace dialog via
Replace or press
Find/replace globally via
Automatic parenthesis matching and indentation in
Advanced editor mode:
Coverage highlighting using heat-map intensity colors:
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:
Controller synthesis (using timed games):
Performance optimization using learning:
Query-specific custom engine options:
- Train gate controller synthesis
- Cat and Mouse
- Adaptive Cruise Control
- Newspaper sharing
- Travel through rush hour traffic