Skip to main content.

This page’s menu:

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:

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