Examples
Each release includes a few examples which demonstrate various Uppaal TRON features.
Mouse Button Controller
The purpose is to demonstrate a simple input/output behavior where timing is of the most importance.
Train Gate Controller
The goal is to provide some performance estimate via benchmarking experiment on concurrent system with several threads. Experiment files.
Smart Lamp Light Controller
The purpose is to demonstrate TRON on a small realistic example of timed system.
On the left you can see the output from TRON console with testing events and timings (testing is running for 624781615 microseconds -- more than 10 minutes according to time-stamps). On the right you can see LightController simulator with light-level history, light-level bar and lamp with color-encoded level. There is a console window with events at LightController side at the bottom of light-level display. The LightController is an essential component of smart lamp where the level of light is defined by the time interval between consecutive user grasps and releases. TRON is behaving like a smart lamp user by issuing grasps and releases and at the same time observing that the level of light is correct according to the specification of LightController behavior written in Uppaal timed automata modeling language.
At least J2SDK 1.5 (Java 5.0) is required to start the smart lamp application.
Latency Experiments
Latency is everywhere. The goal of this experiment is to examine the TRON simulation capabilities and display a distribution of input-stimuli scheduling latency. There are two additional examples called ticking and ping. In ticking, TRON is required to issue periodic ticks which are recorded by IUT adapter. In ping, TRON is required to issue pong after some time the output ping was generated by the IUT adapter. In both examples, the result is a latency distribution (jitter) scatter plot. Ideally the plotted tick deviation should be zero and pongs should be issued precisely at 200ms and 201ms, but soft real-time scheduler (as most operating systems implement) scatters the timing, see the example figures bellow. You may want to make your own experiment by compiling and running ticking.cc which uses the same scheduling methods.
R environment and gv (Ghost Viewer) need to be installed to generate and display the scatter plots.