# New Command Line Options

Below we describe the new options supported by the command line interface of UPPAAL (verifyta). Most of these options are also available from the options menu in the graphical frontend.

## Guiding

A number of different search orders are supported. These can be
selected with the `-o` option:

`-o0`Breadth first.`-o1`Depth first.`-o2`Random depth first.`-o3`Smallest heur first.`-o4`Best first.`-o5`Best depth first.

The first two are well known from previous releases of
UPPAAL. Random depth first search is similar to depth first search,
but it randomises the order in which the successors of a state are
searched. Smallest heur first requires the presence of an
*integer* variable named `heur` in the model. The state
with the smallest value of this variable is always explored next. In
most cases, this variable should be a meta variable. *Best
first* and *best depth first* are used for optimal
reachability, see the next topic.

## Optimal Reachability

UPPAAL CORA has support for finding optimal schedules. Optimality
is defined in terms of a cost variable, see the Language Guide for details. The optimal
trace can be found by using the `-t3` option. With this option,
UPPAAL CORA keeps searching until a trace to a goal state with the
smallest value for the `cost` variable has been
found. Alternatively you can use the `-E` option to find the
optimal cost without generating the trace.

UPPAAL CORA automatically enables the `-o4` option (best
first) when using the `-t3` option. This can be changed by
manually using a different `-o` option *after* the
`-t3` option. In the best first search order, the state with
the smallest value of the `cost` variable is searched next. An
alternative is to use best depth first. This search order performs a
depth first search, but always searches the state with the lowest cost
first. If a remaining cost estimate annotation is provided, the
interpretation of the best first and best depth first is changed to
search the state with the smallest sum of the `cost` variable
and the `remaining` variable next.

## Examples

The jugs example has been updated to the new syntax. You can download it here: jugs2.ta, jugs2.q. You can find the optimal solution like this:

verifyta -E jugs2.ta jugs2.q