Command line interface

The command line interface allows one to run the sanity checker without having to run Uppaal itself.
It is required to have Uppaal installed somewhere though.
Uppaal must be findable by one of the following methods:

• Uppaal.jar is located in the parent directory of the sanity checker, which is the case if the UrPal is installed in the plugins directory.
• The UPPAAL_ROOT environment variable is set according to the readme.

Usage

Usage: application [OPTIONS] INPUT

Options:
  --output PATH                    Output results file
  --checks [deadlock|locations|edges|invariant|declarations]
                                   Selected checks, comma separated. Run all
                                   if absent.
  -h, --help                       Show this message and exit

Arguments:
  INPUT  Input Uppaal model

Example:

java -jar UrPal.jar --output output.csv --checks deadlock,locations,invariant model.xml

Output

The output of the CLI contains the quality of the model according to each check, expressed by a number between 0 (bad model) and 1 (good model):

deadlock, 1.0
locations, 1.0
edges, 0.8461538461538461
invariant, 0.0
declarations, 0.9583333333333334

For any value >0 and <1, the value represents the fraction of visited edges/locations or the used declarations.
Exceptions or timeouts (default 15s) yield a quality of -1.0