| 1 |
5 |
tbourke |
Author: T. Bourke (CSE/NICTA UNSW)
|
| 2 |
|
|
|
| 3 |
60 |
tbourke |
This software is a prototype only. It most likely contains undiscovered
|
| 4 |
|
|
faults. Caveat Modellor.
|
| 5 |
|
|
|
| 6 |
|
|
One good sanity check is to check trace inclusion of a model with itself,
|
| 7 |
|
|
i.e. given AUTO, construct AUTO' then check:
|
| 8 |
|
|
AUTO || AUTO' |= A[] not AUTO'.Err
|
| 9 |
|
|
A failure can indicate a bug in urpal, or an initial model that is not
|
| 10 |
|
|
deterministic. The sanity check can be passed even if, or because, AUTO'
|
| 11 |
|
|
refuses to participate in an action with AUTO. This should never happen if
|
| 12 |
|
|
the construction is performed correctly; it would indicate a bug in urpal.
|
| 13 |
|
|
Running a simulation can increase confidence in AUTO'.
|
| 14 |
|
|
|
| 15 |
|
|
The layout routines do not give perfect results, but they usually make the
|
| 16 |
|
|
basic structure clear enough so that sense can be made of counter-example
|
| 17 |
|
|
traces, and they are a reasonable starting point for manual rearrangement
|
| 18 |
|
|
of label positions (the transition nails make other changes painful). If the
|
| 19 |
|
|
results are very poor, try:
|
| 20 |
|
|
* using scale() to enlarge the source model before generating the tester
|
| 21 |
|
|
* using tabulate(<tester>, {Err}) to organize labels differently
|
| 22 |
|
|
* try both fdp (graphviz { engine=fdp }) and neato (graphviz { engine=fdp })
|
| 23 |
|
|
|
| 24 |
|
|
The program works best under unix, but it will also function under Cygwin.
|
| 25 |
|
|
|
| 26 |
|
|
Bugs may be reported to tbourke@cse.unsw.edu.au
|
| 27 |
|
|
|
| 28 |
|
|
T. Bourke (CSE/NICTA UNSW).
|
| 29 |
|
|
2007-12-05
|
| 30 |
|
|
|
| 31 |
|
|
Initial Configuration
|
| 32 |
|
|
---------------------
|
| 33 |
|
|
1) Install Graphviz.
|
| 34 |
|
|
The program will work without Graphviz, although it will complain
|
| 35 |
|
|
often and most automatic layout features will be disabled.
|
| 36 |
|
|
|
| 37 |
|
|
Under windows, the program has been tested against the normal version
|
| 38 |
|
|
of Graphviz (not a version specially compiled for Cygwin).
|
| 39 |
|
|
|
| 40 |
|
|
2) Edit two entries in urpalrc:
|
| 41 |
|
|
dtd_path should point to flat-1_1.dtd
|
| 42 |
|
|
graphviz/path should point to the graphviz installation
|
| 43 |
|
|
directory (which has a bin/ subdirectory)
|
| 44 |
|
|
|
| 45 |
|
|
Running the program
|
| 46 |
|
|
-------------------
|
| 47 |
|
|
1) Listing templates in an Uppaal model:
|
| 48 |
|
|
urpal -i limitedbind.xml -e show
|
| 49 |
|
|
|
| 50 |
|
|
2) Creating the testing construction:
|
| 51 |
|
|
urpal -i limitedbind.xml -o test.xml -e 'TEST=maketest(Template)'
|
| 52 |
|
|
|
| 53 |
|
|
3) If the result is hard to read, try variations of:
|
| 54 |
|
|
urpal -i limitedbind.xml -o test.xml -e 'TEST=tabulate(maketest(scale(Template,2.0)),{Err})'
|
| 55 |
|
|
|
| 56 |
|
|
Further commands and options are listed in the included documentation.
|
| 57 |
|
|
|