| 1 |
50 |
tbourke |
$Id$
|
| 2 |
|
|
|
| 3 |
|
|
Test format
|
| 4 |
|
|
-----------
|
| 5 |
|
|
Each test file is an Uppaal model containing a single template named
|
| 6 |
|
|
`Template' (the default for a new model). The global declarations should
|
| 7 |
|
|
begin with a comment of the form:
|
| 8 |
|
|
/*
|
| 9 |
|
|
description: <free form description, may cover multiple lines.>
|
| 10 |
|
|
|
| 11 |
|
|
error: <a non-zero error code if the test is expected to fail>
|
| 12 |
|
|
stderr: <expected messages on stderr>
|
| 13 |
|
|
|
| 14 |
|
|
layout: <a value for the graphviz/engine setting>
|
| 15 |
|
|
scale: <a floating point scaling factor>
|
| 16 |
|
|
tabulate: <yes|no>
|
| 17 |
|
|
|
| 18 |
|
|
author: <author name>
|
| 19 |
|
|
created: <creation date: yyyymmdd>
|
| 20 |
|
|
*/
|
| 21 |
|
|
|
| 22 |
|
|
All fields are optional. Blank lines are ignored.
|
| 23 |
|
|
Fields may cover multiple lines but should not contain any of the field
|
| 24 |
|
|
tags, i.e. the names above including colons.
|
| 25 |
|
|
The closing comment brace `*/` must appear on a line by itself.
|
| 26 |
|
|
|
| 27 |
|
|
Testing Procedure
|
| 28 |
|
|
-----------------
|
| 29 |
|
|
1. The test file is processed by urpal to create a new template: `Test'.
|
| 30 |
|
|
The layout fields are respected.
|
| 31 |
|
|
2. The return code and stderr text are compared with the values given.
|
| 32 |
|
|
3. The system string is set to: system Template, Test;
|
| 33 |
|
|
4. Uppaal attempts to verify the model against: A[] (not Test.Err)
|
| 34 |
|
|
|