-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
155 lines (115 loc) · 5.3 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
libutap, version 0.94
Mini HOWTO
Gerd Behrmann
Marius Mikucionis
1. What is libutap
2. Compiling
3. Simple use
4. Architecture
5. Contact
1. What is libutap
libutap is the Uppaal Timed Automata Parser. Uppaal is an integrated
tool environment for designing, simulating and verifying real time
systems modeled as extended timed automata. libutap is the parser of
Uppaal.
libutap has the ability to parse and type check Uppaal models in any
of the three file formats supported by Uppaal.
libutap is licensed under the LGPL.
2. Compiling
libutap uses automake and autoconf to make compilation on various
platforms easy. You will need gcc 3.3 or newer, GNU make,
libxml2 from http://www.xmlsoft.org (at least version 2.6.10),
libsbml from http://www.sbml.org.
Simply run to compile libutap and use it:
./configure
make
Run the following to install libutap:
make install
Read the INSTALL file in the distribution for more information on
how to compile.
NOTE: if you want to regenerate automatically created files like the
configure script and Makefile, use autoreconf -i. Do *not* run
autoconf directly, it will mess up your Makefile. You need autoconf
version 2.53 or newer and automake.
3. Simple use
There are two ways one can use the library. In its simplest form, one
calls one of the top level parsing functions defined in utap/utap.h,
e.g. example.cpp:
#include <stdio.h>
#include "utap/utap.h"
int main()
{
UTAP::TimedAutomataSystem system;
parseXMLFile("myfile.xml", &system, true);
}
The first argument is the file to read. The second is the output of
the parser and the third is a flag indicating whether we want to use
the new or the old syntax (the old syntax is the one used in Uppaal
3.4, the new is the one that will be used since Uppaal 3.6).
After the call to parseXMLFile, one can access the network of timed
automata in the system variable. Take a look at utap/system.h to see
what kind of structures you can access.
Distribution also includes pretty.cpp for pretty-printing a model files.
See also doxygen API documentation in doc/api/index.html.
Use the following command to compile the example:
g++ example.cpp -o example -lutap -lxml2
If UTAP was configured with --prefix=$MYPATH to install in custom location
then use the following to compile:
g++ -I$MYPATH/include example.cpp -o example -L$MYPATH/lib -lutap -lxml2
4. Architecture
The following ASCII figure shows the initial information flow through
the library.
+----\
| |\
| +-\
| | --> libxml2 --[SAX-interface]--> "xmlreader.cc"
| .xml | |
| | |
+------+ |
|
+----\ |
| |\ |
| +-\ v
| .ta | +--------------------------+
| .xta | -----------------------> | bison parser (parser.yy) |
| | +--------------------------+
+------+ |
|
+------+ |
| | |
| TAS | |
| | +---------------+ |
| | <--- | SystemBuilder |<--[ParserBuilder]--/
| | +---------------+
+------+
The BNF implemented by the bison generated parser is split into
several sections and to some extend duplicated for the old and new
syntax. It can read .ta and .xta files directly. XML files are read
using the libxml2 library. Each text-block in the XML file is then
parser wrt. the BNF for that block (see xmlreader.cpp). For this, the
bison generated parser is reused.
The parser calls methods in the abstract ParserBuilder class. The
methods in the ParserBuilder class are implemented by the
SystemBuilder class which is a subclass of ExpressionBuilder which is
a subclass of AbstractBuilder. The SystemBuilder writes the model to
an instance of the TimedAutomataSystem (TAS) class.
The design abstracts the differences between the .xml, .xta and .ta
input formats and also hides the differences between the 3.4 and
3.6/4.0 formats from any implementation of the ParserBuilder interface
(for equivalent input the parser will call the same methods in the
ParserBuilder class).
A TAS object represents the templates, variables, locations,
transitions and processes of a model. Symbols are represented by
symbol_t objects (see the API documentation). A symbol is a name (a
string) with a type. The type is represented by a type_t
object. Symbols are grouped into frames (represented by frame_t
objects). Frames are used to represent scopes and other collections of
symbols such as records or parameters of templates and functions.
All expressions are represented using a tree structure where the
leaves represent values or variables and the inner nodes represent
operations. Each node is referenced using an expression_t object.
5. Contact
If you have questions or comments to libutap, you can contact me on
the following email address: marius@cs.aau.dk. For a list of known
bugs or for reporting new bugs take a look at the UPPAAL bugzilla
installation at http://www.uppaal.org/.