Skip to main content.

This page’s menu:

Language Guide

UPPAAL CORA is based on the newest internal development version of UPPAAL. On one hand this means that it contains all the new and exciting features of the next version of UPPAAL, but on the other it also means that it contains many new and untried features, that might change before the final release of UPPAAL. This page describes the new language features compared to the UPPAAL 4.0 series.

Cost Annotation

In LPTA, an implicit continuous monotonic variable called cost is defined. The rate at which this variable grows can be specified in the location invariant as:

cost' == INTEXPR

where INTEXPR is an integer expression. If specified in multible locations, the actual cost rate is the sum of the cost rate specified in the current location of each process. The cost can be incremented on edges using the increment operator +=.

Here is an example of the aircraft landing problem: xta, q.

Remaining Cost Estimation

The performance of UPPAAL CORA can be improved dramatically by annotating the model with an admissible estimate of the remaining cost to reach the goal condition. Admissible means that the estimate is not bigger than the actual cost of reaching the goal, i.e., the estimate provides a lower bound on the remaining cost. The estimate is specified by declaring a meta integer variable named remaining. Specifying a good value for remaining is crucial for good performance.

In previous versions of UPPAAL, remaining had to be a lower bound on the remaining cost from the state and all its delay successors, but this is no longer required. Now remaining must simply be a lower bound on the remaining cost. When computing a successor, UPPAAL automatically adjusts the value of remaining. Thus even when you do not recompute remaining, it will still be a lower bound of the remaining cost. You will probably be able to come up with a better lower bound on the remaining cost, so you should try compute a remaining cost yourself on each edge transition.