Allows extending an UPPAAL model with annotated blocks and XML blocks, e.g.:
<nta> <declaration> ... // @myAnnotation const int v1 = 1; const int v2 = 2; ... </declaration> ... <queries> ... </queries> ... </nta>
And reads a companion MS Excel file (with the same base name) with tables that describe how to adapt the block following an annotation command, until the next empty line.
For example, with the expression and table below in a sheet called
@myAnnotation, the values 1 and 2 will become 10 and 20.
It is also possible to replace the content of the
<queries> block by introducing a sheet named
<queries> to our spreadsheet with a table like the one below:
||The worker is always Idle|
This concrete table will replace the content of the
<queries> block by two
<query> blocks containing the corresponding formulas and comments from the table.
Supporting multiple configurations
Often we want to experiment with different combinations of values and queries.
Uppex supports the specification of a list of configurations, each producing variations of the values and XML blocks, following principles from Software Product Line Engineering. Uppex generates, for each of the provided configurations, a different instance of the original UPPAAL model and verifies all properties of all instances. We will first see how to define configuration by selecting desired “features”, and then how to enrich the annotations with these “features”.
A special sheet named
@Configurations lists and specifies the configuration in a table similar to the one below:
The names below Configuration identify the set of desired configurations, and every non-empty cell at the right of these selects the feature name at the top of the corresponding column.
In this example we have 3 configurations: Main, Conf2, and Conf3; configuration Conf2 selects Feature1, Conf3 selects Feature2, and Main does not select any feature. Each feature selection in a configuration will modify the annotations, explained below, yielding a different instance of the UPPAAL model.
Enriching annotations with features
Recall that each annotation is described by a table with multiple columns, each with a header identifying a pattern name. A special column named
Features is used to map entries to feature names, such as the ones in the configuration table. Each line of an annotation table is included only if all of its names in the
Features column (separated by commas) are selected in the configuration. In case of entries with the same left-most value, the last one prevails.
For example, using the table below and considering the configuration table above, selecting the configuration Conf3 would produce our original Uppaal model, but selecting Conf2 would instead assign
Build the (fat) jar
- SBT (https://www.scala-sbt.org)
- JVM (>=1.8)
- UPPAAL (optional - https://uppaal.org)
Use the sbt task to build the self-contained jar-file running at the root:
Run the jar
The compiled jar-file can be found in
You can copy it to your working folder, with the UPPAAL and Excel files. To list the possible options run in the command line:
java -jar uppex.jar --help
For example, to apply the default configuration in a file
myfile.xlsx to an UPPAAL model
myfile.xml, you can run the command:
java -jar uppex.jar myfile.xlsx
The file names of the configuration and UPPAAL files must match.
You will be presented with a list of changes applied to the
myfile.xml, this file will be updated, and a copy of the original file will be placed in a
backups folder, which will be created if it does not exist.
To check all properties using UPPAAL of all configurations, you can run the command:
java -jar uppex.jar --runAll myfile.xlsx
This requires the command
verifyta to be available in the
PATH, which can be found in the binaries included by UPPAAL.
Extra options, such as a timeout value, can be defined here, requiring the command
timeout to be available in the
This command will:
- output to the screen the results of verifying each property as they are verified, and
- produce a “report.html” file compiling all the results in a more readable format.
You can find a simple example in folder examples/simple to illustrate the usage of annotations.
It includes a minimalistic Uppaal file, a simple Excel file, and a script
runuppaal.command to call Uppex and Uppaal.
This example includes both annotation and XML blocks; the former are in sheets whose name starts in
@, and the latter are in sheets whose name is surrounded by angular brackets
To run the simple example, first build the fat jar (
Then, using the command line in the folder of the example, type
A variation of this example can be found in folder examples/simple-with-conf that further illustrates how to apply multiple configurations, using the special sheet named