# 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.