|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
+--------+-------------------------------+
| Symbol | Description |
+========+===============================+
| K | constant |
| x | variable |
| T | simple type |
| G | gate |
| F | function |
| M | macro |
| P | macro parameter |
| E | expression |
| O | offer |
| D | variable declaration |
| RT | result type |
| OP | operator |
| FD | function definition |
| MD | macro definition |
| LI | library inclusion |
| ETD | external type declaration |
| EFD | external function declaration |
| EID | external include directive |
| ELD | external compile directive |
| PG | program |
+--------+-------------------------------+
any | end_def | exists | of |
apply | end_exists | for | on |
assert | end_for | forall | then |
def | end_forall | from | to |
else | end_if | if | use |
else_if | end_let | in | where |
end_assert | end_use | let |
The identifiers are grouped into two classes:
$let) to avoid clashes.
The separators are sequences containing space,
tab, and newline characters, as well as comments, enclosed between (* and
*).
In XTL, functions
can be overloaded, i.e., have the same identifier but different types for
their arguments and/or result. The XTL compiler resolves overloading statically
(i.e., at compile-time) or issues an error message if the context does not
permit to resolve overloading (in such case, the "of" operator can be used
to supply typing information).
In XTL, a function F can be either prefixed, i.e., its calls are written "F (E1, ..., En)", or infixed, i.e., F has two arguments and its calls are written "E1 F E2".
Most predefined functions are infixed,
except "extract" and "replace". For user-defined functions, the prefix or
infix nature is specified when the function is declared.
Also, unary minus
operators must be written in functional notation, i.e., -(1) instead of -1,
-(X) instead of -X, etc.
boolean. The Boolean constants true and false are defined as 0-ary functions.
The table below gives the predefined functions for this type: +----------------------------------------+--------------------------+ | Operator | Meaning | +========================================+==========================+ | true, false : -> boolean | boolean constants | | not : boolean -> boolean | negation | | or, and, implies, | connectors and | | =, <> : boolean, boolean -> boolean | relational operators | | replace : boolean, boolean -> boolean | replacement operator | +----------------------------------------+--------------------------+The "
replace" operator (which is overloaded for all types) takes two
arguments of the same type and returns the second one. It is useful for
use within the "for" expressions (see EXPRESSIONS below).
integer. Integer constants are
noted with a C-like syntax and should be preceded of a sign "+" or "-", e.g.,
-123, +123, +0, etc. The table below gives the predefined functions for this
type: +----------------------------------------+--------------------------+ | Operator | Meaning | +========================================+==========================+ | -, + : integer, integer -> integer | binary minus, plus | | - : integer -> integer | unary minus | | *, div : integer, integer -> integer | multiplication, division | | mod : integer, integer -> integer | modulo | | ** : integer, integer -> integer | power | | integer : real -> integer | real to integer | | integer : character -> integer | character to integer | | <, <=, >, >=, =, <> : | relational operators | | integer, integer -> boolean | | | replace : integer, integer -> integer | replacement operator | +----------------------------------------+--------------------------+
natural. Natural
constants are noted with a C-like syntax and should never be preceded of
a sign, e.g., 123, 0, etc. The table below gives the predefined functions
for this type: +----------------------------------------+--------------------------+ | Operator | Meaning | +========================================+==========================+ | -, + : natural, natural -> natural | binary minus, plus | | *, div : natural, natural -> natural | multiplication, division | | mod : natural, natural -> natural | modulo | | ** : natural, natural -> natural | power | | natural : real -> natural | real to integer | | natural : character -> natural | character to natural | | <, <=, >, >=, =, <> : | relational operators | | natural, natural -> boolean | | | replace : natural, natural -> natural | replacement operator | +----------------------------------------+--------------------------+
By default, an unsigned number 123 denotes either a value of type natural
or a value of type integer. Such overloading can be resolved explicitly
by the user (using an "of" operator) or implicitly by the context (for
instance, in (X + 123), the type of X will determine the type of 123). If
the context does not permit to resolve overloading, then the constant will
ultimately be given the type Natural. To summarize:
- +123 has the integer type.
- -123 has the integer type.
- 123 of integer has the integer type.
- 123 of natural has the natural type.
- 123 has either the natural or integer type (with a final priority for
natural).
real. Real constants are noted with a C-like syntax, e.g., 3.1416, -9.98E-6, etc.
The table below gives the predefined functions for this type: +----------------------------------------+--------------------------+ | Operator | Meaning | +========================================+==========================+ | -, + : real, real -> real | binary minus, plus | | - : real -> real | unary minus | | *, / : real, real -> real | multiplication, division | | ** : real, real -> real | power | | real : integer -> real | integer to real | | <, <=, >, >=, =, <> : | relational operators | | real, real -> boolean | | | replace : real, real -> real | replacement operator | +----------------------------------------+--------------------------+
character. Character
constants are noted with a C-like syntax, e.g., 'a', '\n', '\012', '\x1A', etc. The table
below gives the predefined functions for this type: +----------------------------------------+--------------------------+ | Operator | Meaning | +========================================+==========================+ | -, + : character, integer -> character | subtract, add integer | | character : integer -> character | integer to character | | <, <=, >, >=, =, <> : | relational operators | | character, character -> boolean | | | replace : | | | character, character -> character | replacement operator | +----------------------------------------+--------------------------+
string. String
constants are noted with a C-like syntax, e.g., "abc", "123", "Hello\n", etc.
The table below gives the predefined functions for this type: +----------------------------------------+--------------------------+ | Operator | Meaning | +========================================+==========================+ | null : -> string | empty string | | length : string -> integer | string length | | extract : string, integer -> character | character extraction | | =, <> : string, string -> boolean | relational operators | | replace : string, string -> string | replacement operator | +----------------------------------------+--------------------------+
raw type represents a byte string that denotes
a value of unknown type, i.e., whose type is not one of the other predefined
types. Raw constants are noted with a C-like syntax but using backquotes
rather than double quotes, e.g., `foo`, `CONS (0, NIL)`, or `{0, 1}`, etc. The table
below gives the predefined functions for this type: +----------------------------------------+--------------------------+ | Operator | Meaning | +========================================+==========================+ | null : -> raw | empty raw data | | length : raw -> integer | raw data length | | extract : raw, integer -> character | character extraction | | =, <> : raw, raw -> boolean | relational operators | | replace : raw, raw -> raw | replacement operator | +----------------------------------------+--------------------------+
By default, the string notation "..." denotes either a value of type string
or a value of type raw. Such overloading can be resolved explicitly by the
user (using an "of" operator) or implicitly by the context (for instance,
in (X = "foo"), the type of X will determine the type of "abc"). If the
context does not permit to resolve overloading, then the constant will
ultimately be given the type String. To summarize:
- `foo` has the raw type.
- "foo" of string has the string type.
- "foo" of raw has the raw type.
- "foo" has either the string or raw type (with a final priority for string).
state, label, edge, stateset, labelset,
and edgeset (also called meta-types because they refer to the LTS model
rather than to the objects defined in the source program to be verified)
denote the states, labels, edges, sets of states, sets of labels, and sets
of edges of the LTS, respectively.
The table below gives the predefined
operators over these types ("set" denoting either stateset, labelset, or
edgeset). These operators allow to explore (forward and/or backward) the
transition relation of the LTS, to combine sets of states, labels and edges,
and also to obtain information about the LTS.
+-----------------------------------+-------------------------+ | Operator | Meaning | +===================================+=========================+ | init : -> state | initial state | | succ : state -> stateset | successor states | | pred : state -> stateset | predecessor states | | out : state -> edgeset | successor transitions | | in : state -> edgeset | predecessor transitions | | =, <> : state, state -> boolean | comparison operators | | replace : state, state -> state | replacement operator | +-----------------------------------+-------------------------+ | visible : label -> boolean | visibility test | | string : label -> string | label to string | | =, <> : label, label -> boolean | comparison operators | | replace : label, label -> label | replacement operator | +-----------------------------------+-------------------------+ | source : edge -> state | transition source state | | target : edge -> state | transition target state | | label : edge -> label | transition label | | succ : edge -> edgeset | successor transitions | | pred : edge -> edgeset | predecessor transitions | | =, <> : edge, edge -> boolean | comparison operators | | replace : edge, edge -> edge | replacement operator | +-----------------------------------+-------------------------+ | empty, false : -> set | empty set | | full, true : -> set | full set | | comp, not : set -> set | complementation | | union, or : set, set -> set | union | | inter, and : set, set -> set | intersection | | implies : set, set -> set | implication | | iff : set, set -> set | equivalence | | diff : set, set -> set | difference | | includes : set, set -> boolean | inclusion test | | insert, remove : set, elem -> set | insertion, removal | | among : elem, set -> boolean | membership | | card : set -> number | cardinal | | =, <> : set, set -> boolean | comparison operators | | replace : set, set -> set | replacement operator | +-----------------------------------+-------------------------+For convenience, some of the operators above are overloaded (see FUNCTIONS below). Also, some of the set operators have synonyms (e.g.,
union has the
synonym or) allowing a more intuitive writing of boolean properties.
number
type for the manipulation of state, label, and edge numbers. The table below
gives the predefined operators of type number. +------------------------------------+--------------------------+ | Operator | Meaning | +====================================+==========================+ | number_of_states : -> number | number of states | | number_of_labels : -> number | number of labels | | number_of_edges : -> number | number of edges | | number : state -> number | state number | | number : label -> number | label number | | number : edge -> number | edge number | +------------------------------------+--------------------------+ | -, + : number, number -> number | binary minus, plus | | *, div : number, number -> number | multiplication, division | | mod : number, number -> number | modulo | | ** : number, number -> number | power | | number : character -> number | conversion from/to | | character : number -> character | character | | number : integer -> number | conversion from/to | | integer : number -> integer | integer | | number : real -> number | conversion from/to | | real : number -> real | real | | <, <=, >, >=, =, <> : | relational operators | | number, number -> boolean | | | replace : number, number -> number | replacement operator | +------------------------------------+--------------------------+All arithmetic operators (except unary minus) and relational operators of type
integer are also available for type number. Moreover, the values
belonging to these two types can be freely mixed within arithmetic and
relational expressions. The main difference between these two types concerns
the manipulation of large numbers: the maximum value of type integer is
2^31-1 = 2,147,483,647 on 32-bit machines and 2^63-1 = 9,223,372,036,854,775,807
on 64-bit machines, whereas the maximum value of type number is 2^32-1 = 4,294,967,295
on 32-bit machines and 2^64-1 = 18,446,744,073,709,551,615 on 64-bit machines.
Therefore, for large LTSs, any information concerning the LTS structure
(e.g., cardinality of state/edge/label subsets, depth/breadth of the LTS,
number of breadth-first levels, etc.) should be manipulated using values
of type number instead of type integer in order to avoid overflows.
Conversion
operators between the number type and the types character, integer, and
real are also provided. Constants of type number are written in decimal
notation preceded by a '#' character (e.g., #4294967295). An alternative way
of representing constants of type number that fit in the range of type
integer is by means of the conversion operator from integer to number (e.g.,
the values number(2147483647) and #2147483647 are the same).
action (T may be any type).
The print and
printf operators behave differently on strings: print prints the string
enclosed between double quotes and converts unprintable characters and
escape sequences to three-digit octal notation, whereas printf does not
add double quotes and interprets execute sequences. For instance, print
("Hello!\n") displays "Hello!\012", whereas printf ("Hello!\n") displays Hello!
followed by a line-feed. So, print should be used to display string values
(e.g., label offers of the string type), whereas printf should be used to
display messages.
+--------------------------------+---------------------------+ | Operator | Meaning | +================================+===========================+ | nop : -> action | inaction | | fby : action, action -> action | sequential composition | | print : T -> action | value printing | | printf : string -> action | string formatted printing | +--------------------------------+---------------------------+
O ::= "?" x ":" T
| "!" E
| "_"
An offer "?" x ":" T matches a value v iff v has the type T; in case
of matching, the variable x is also assigned the value v. An offer "!" E
matches a value v iff the expression E evaluates to v. An offer "_" (wildcard)
matches a value v of any type.
RT ::= T
| "(" RT0"," ..."," RTn ")"
These types may occur in variable declarations (see the next paragraph)
as well as in function declarations (see FUNCTIONS below).
D ::= x ":" RT
| "any" RT
| "(" D0"," ..."," Dn ")"
A declaration x ":" RT defines the variable x of type RT. A declaration
"any" RT, which is meaningful only inside a declaration of anonymous tuple
type, defines a placeholder of type RT standing for a field of the tuple.
Declarations of the form "any" RT can occur only in the "let" expressions
(see below). A declaration "(" D0"," ..."," Dn ")" defines a tuple whose fields
are denoted by the variables and placeholders occurring inside D0, ..., Dn.
for" expressions (see below); they
denote calls of binary functions on two arguments. They have the following
syntax: OP ::= F
| "(" OP0"," ..."," OPn ")"
An F operator denotes a call of the binary function F. An "(" OP0"," ...","
OPn ")" operator denotes a call of a binary function on two arguments of
tuple type; the result is a tuple whose fields are the results of the calls
of OP0, ..., OPn on the corresponding fields of the arguments. There is a static
semantics constraint on the operators OP: their left arguments must have
the same types as their results.
The syntax of expressions is given by the following grammar:
E ::= K
| F "(" E0"," ..."," En ")"
| E0 "of" RT
| E0 "->" "[" O0 ... On [ "..." ] [ "where" E1 ] "]"
| "{" E0"," ..."," En "}"
| "(" E0"," ..."," En ")"
| "let" D0 "=" E0"," ..."," Dn "=" En "in"
En+1
"end_let"
| "if" E0 "then" E'0
"else_if" E1 "then" E'1
...
"else_if" En "then" E'n
"else" E'n+1
"end_if"
| "assert" E0"," ..."," En "in"
En+1
"end_assert"
| "use" x0"," ..."," xn "in"
E
"end_use"
| "for" [ x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ] ]
[ "in" D ]
[ "while" E'1 ]
[ "where" E'2 ]
"apply" OP
"from" E'3
"to" E'4
"end_for"
| "forall" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_forall"
| "exists" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_exists"
| "<|" OP "on" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
[ "where" E' ]
"|>" En+1
| "{" x ":" T [ "among" E0 ] "where" E1 "}"
The semantics of expressions is described informally below. K
F "(" E0"," ..."," En ")"
E0 "of" RT
E0 "->" "[" O0 ... On [ "..." ] [ "where" E1 ] "]"
boolean, called matching expression. E0 must
be of type label or edge. The construct between "[" and "]" is called an
label pattern: it allows to match the content of the label denoted by E0
(if E0 is of type label) or by label (E0) (if E0 is of type edge), possibly
extracting the values of its different fields. The optional construct "..."
matches a sequence of zero or more values of any type.
For convenience,
in the verification of LOTOS programs, the first offer O0 (intended to
match a gate) can be simply written G (i.e., without the "!" sign).
The variables
contained in O0, ..., On (if any) are visible in the optional expression E1,
which must be of type boolean.
The XTL compiler examines the labels present in the BCG graph to check if there exist labels that correspond, in the number of fields and types of their fields, to the list of offers O0, ..., On. If no such label is found, then the compiler issues a warning message (this is a form of vacuity checking).
The compiler also uses the types of
field labels to resolve overloading ambiguities (if any) in offers. For
instance, the offer 1 in the label pattern "G !1" will be considered of
integer if only integer values are passed on gate G in the BCG graph on
which the XTL program is evaluated.
A matching expression matches a label
G v1 ... vm iff: m = n if "..." is absent, or m >= n otherwise; O0 matches G;
O1, ..., On match v1, ..., vn; E1, if present, evaluates to true in the context
of the variables assigned in the offers. A matching expression evaluates
to true in case of successful matching of a label (in this case, all the
variables contained in the offers have been initialized) and to false otherwise.
"{" E0"," ..."," En "}"
stateset, labelset,
or edgeset.
"(" E0"," ..."," En ")"
"let" D0 "=" E0"," ..."," Dn "=" En "in"
En+1
"end_let"
let" expression also allows to extract the fields of tuple values
and to assign them to variables.
"if" E0 "then" E'0
"else_if" E1 "then" E'1
...
"else_if" En "then" E'n
"else" E'n+1
"end_if"
boolean, whereas E'0, ..., E'n+1 must be of the same type
(which is also the type of the "if" expression). The evaluation of an "if"
expression proceeds as follows: the conditions Ei are evaluated (for 1
<= i <= n) and the value of the "if" expression is equal to the value of
the first E'i for which Ei is true. If none of the conditions evaluates to
true, the resulting value is given by E'n+1. If a condition Ei is a matching
operator, the variables assigned by the offers inside Ei are visible only
in the corresponding expression E'i.
"assert" E0"," ..."," En "in"
En+1
"end_assert"
boolean. If all the
assertions evaluate to true, the value of the "assert" expression is equal
to the value of En+1; otherwise, the execution of the XTL program is interrupted
and an error message is displayed on the POSIX standard output stream (stdout).
"use" x0"," ..."," xn "in"
E
"end_use"
"for" [ x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ] ]
[ "in" D ]
[ "while" E'1 ]
[ "where" E'2 ]
"apply" OP
"from" E'3
"to" E'4
"end_for"
set of Ti": thus,
iterations over sets of states, labels, or edges are allowed. There is an
exception concerning integer numbers and characters: for these types, domains
of the form "{" E1 "..." E2 "}", meaning all the integers (resp. characters)
between E1 and E2, are also allowed. The variables declared in the "in"
D declaration (if present) are called accumulators. Both iteration variables
and accumulators are visible in the expressions E'1, E'2 (if present), and
E'4, but not in E'3. The expressions E'1 and E'2 must be of type boolean.
Assuming
that all the optional constructs are present, the evaluation of a "for"
expression proceeds as follows. The accumulators are initialized to the
value of E'3. Let us note v the current values of the accumulators (v may
be of type tuple). Then, for each value of the iteration variables in their
corresponding domains, the expression v OP E'4 is evaluated and its result
is stored in the accumulators. The value of the "for" expression is equal
to the value of the accumulators obtained after the last iteration. The
"where" clause allows to perform only those iterations for which the expression
E'2 evaluates to true. The "while" clause allows to stop the iterations when
the expression E'1 becomes false.
Particular cases of "for" expressions may
be obtained by eliminating some (or all) of the optional constructs. If
the iteration variables are absent, the "for" becomes an infinite loop:
in this case, the "while" clause must be present in order to stop the evaluation.
If the "in" declaration is absent, the accumulator is implicit: it is used
internally to store the results of intermediate iterations, but it cannot
be used in E'1, E'2, nor E'4.
The "for" expressions are useful for describing
iterative computations. For instance, the expression below displays on the
standard output the sequence of Fibonacci numbers smaller than 1000:
for
in (xn_plus_1, xn: integer, a:action)
while xn < 1000
apply (replace, replace, fby)
from (1, 1, nop)
to (xn_plus_1 + xn, xn_plus_1,
print (xn) fby printf ("\n"))
end_for
"forall" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_forall"
for"
expression: "for" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"apply" and
"from" true
"to" En+1
"end_for"
The type of En+1 may be either boolean, stateset, labelset, or edgeset.
In the three latter cases, the true and and operators correspond to full
set and set intersection, respectively (see TYPES, FUNCTIONS AND CONSTANTS
above).
"exists" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_exists"
for"
expression: "for" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"apply" or
"from" false
"to" En+1
"end_for"
The type of En+1 may be either boolean, stateset, labelset, or edgeset.
In the three latter cases, the false and or operators correspond to empty
set and set union, respectively (see TYPES, FUNCTIONS AND CONSTANTS above).
"<|" OP "on" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
[ "where" E' ]
"|>" En+1
for" expression, called iterator. It is
equivalent to the following "for" expression: "for" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
[ "where" E' ]
"apply" OP
"from" init_OP
"to" En+1
"end_for"
stateset, labelset, or edgeset). +-----------------------------------+---------------+ | Operator OP | init_OP | +===================================+===============+ | or : boolean, boolean -> boolean | false | | and : boolean, boolean -> boolean | true | | + : integer, integer -> integer | 0 | | * : integer, integer -> integer | 1 | | union, or : set, set -> set | empty, false | | inter, and : set, set -> set | full, true | | diff : set, set -> set | full | | insert : set, elem -> set | empty | | remove : set, elem -> set | full | | fby : action, action -> action | nop | +-----------------------------------+---------------+The iterators allow to express iterative computations in a form close to the mathematical notation. For example, the sum of the integer numbers from 1 to 100 may be computed with the following iterator:
<| + on K:integer among { 1 ... 100 } |> K
Similarly, the number of transitions labelled with "SEND" labels may be
computed as follows: <| + on T:edge where T -> [ SEND ... ] |> 1
"{" x ":" T [ "among" E0 ] "where" E1 "}"
for" expression:
"for" x ":" T [ "among" E0 ]
"where" E1
"apply" union
"from" empty
"to" "{" x "}"
"end_for"
The implicitly defined sets allow to compute sets of states, labels or
transitions in a form close to the mathematical notation. For example, the
set of deadlock states (i.e., states having no successors) can be computed
by the XTL expression below: { S:state where succ (S) = empty }
FD ::= "def" F "(" x1 ":" T1"," ..."," xn ":" Tn ")" ":" RT "="
[ FD1 ... FDm ]
E
[ "where" FDm+1 ... FDm+p ]
"end_def"
| "def" "_" F "_" "(" x1 ":" T1"," x2 ":" T2 ")" ":" RT "="
[ FD1 ... FDm ]
E
[ "where" FDm+1 ... FDm+p ]
"end_def"
The first construct above defines a function F having the parameters
x1, ..., xn of types T1, ..., Tn, the body E, and returning a result of type
RT. The calls of F have the form: F "(" E1"," ..."," En ")"
where the arguments E1, ..., En must be compatible (in number and types)
with the parameters of F. The result of the call is equal to the value of
E computed in a context in which the parameters xi are assigned the values
of Ei for all i between 1 and n. The body of F may also contain definitions
of local functions, placed either before E, or after E and the keyword
"where". These functions are visible only in the expression E. Recursive
functions are allowed. Also, functions can be overloaded: several functions
with the same name, but different profiles, may be defined in the same
scope. In case of ambiguity of the type of a function call, the "of" expression
may be used to precise a unique type (see EXPRESSIONS above).
The second
construct above defines a binary infixed function F having the parameters
x1, x2 of types T1, T2, and returning a result of type RT. The function
F behaves like an ordinary binary function, except that its calls may be
written either in the form F "(" E1"," E2 ")", or in the form E1 F E2. This
kind of functions allow to write expressions involving infixed operators
using a syntax close to the mathematical notation. For example, the predefined
function "+" over integers is in fact an infixed operator: the user may
write either + (1, 2), or 1 + 2. The infixed operators (both predefined
and user-defined) are right-associative: e.g., the expression 1 + 2 + 3 is
parsed as 1 + (2 + 3).
Functions can be, of course, recursive (either directly, or transitively). For example, the recursive function below computes the factorial of an integer number:
def fact (n:integer) : integer =
assert n >= 0 in
if n = 0 then
1
else
n * fact (n - 1)
end_if
end_assert
end_def
This function also checks whether its argument is greater or equal to
0 using an "assert" expression; if this is not the case, the program execution
is aborted with an appropriate error message.
MD ::= "macro" M "(" P1"," ..."," Pn ")" "="
<text>
"end_macro"
The above construct defines a macro M having the parameters P1, ..., Pn
and the body <text>, which is a portion of text built using the characters
allowed by the XTL language (see LEXICAL ELEMENTS above). The calls of M
have the form: M "(" <text1>"," ..."," <textn> ")"
where the arguments <text1>, ..., <textn> are portions of XTL text. The result
of the call is <text> in which all the occurrences of the parameters Pi have
been syntactically substituted with the arguments <texti>, for all i between
1 and n. The following syntactic restriction must be satisfied: the keywords
contained in each <texti> argument must be well-bracketed, i.e., if <texti> contains
a keyword opening an expression (e.g., "for"), then <texti> must also contain
the corresponding keyword closing the expression (e.g., "end_for"). This also
applies to the non-alphabetic keywords such as "(", ")", "[", "]", "{",
"}". A macro is visible from the point of its definition until the end of
the XTL program. The macros may be overloaded: several macros with the same
name, but different arities, may be defined in the same scope.
LI ::= "library" <file0.xtl>"," ..."," <filen.xtl>
"end_library"
At the compilation of the program, the above construct is syntactically
replaced with the contents of the files <file0.xtl>, ..., <filen.xtl>, placed one
after the other in this order. The XTL compiler searches the included files
first in the current directory, then in the directory referenced by $CADP/src/xtl.
Multiple inclusions of the same file are silently discarded, unless the
-warning option is passed to the compiler; in this case, appropriate messages
are issued.
ETD ::= "type" T
[ "!" "implementedby" "<C_type>" ]
[ "!" "comparedby" "<C_compare>" ]
[ "!" "enumeratedby" "<C_iterate>" ]
[ "!" "printedby" "<C_print>" ]
"end_type"
where T is the identifier of the declared type and the optional pragmas
preceded by "!" refer to the C implementation of T: <C_type> is the identifier
of the C type implementing T; <C_compare> is an operator for comparing two
values of type T; <C_iterate> is a macro allowing to iterate over all values
of type T; and <C_print> is a printing function for values of type T. The
C names declared by these pragmas cannot be used directly in the XTL program,
but are used in the C code generated by the XTL compiler. The directive
for an external function declaration has the following syntax: EFD ::= "func" F "(" T1"," ..."," Tn ")" ":" RT
[ "!" "implementedby" "<C_func>" ]
"end_func"
where F is the identifier of the declared function, T1, ..., Tn are the types
of its parameters, and RT is the type of its result. The optional pragma
"implementedby" declares the name <C_func> of the C function implementing
F. This C identifier cannot be used in the XTL program, but is used in the
C code generated by the XTL compiler. The external types and functions declared
using the directives above may be implemented in (one or more) C files
file1.c, ..., filen.c that must be included in the C code generated by the XTL
compiler. This is done using the following external include directive:
EID ::= "include" "<file1>", ..., "<filen>" "end_include"where <file1>, ..., <filen> are the names of the C source files (".c" and/or ".h") that must be included. This directive is translated into corresponding "#include" pre-processor commands in the C code generated by the XTL compiler. The compilation and linkediting of the C modules included may require specific parameters. These can be indicated to the XTL compiler using the following external compile directive:
ELD ::= "flag" "<C_compiler_directives>" "end_flag"where <C_compiler_directives> is a portion of command-line for invoking the C compiler (typically containing "-I", "-L", and "-l" options) that specifies the desired compilation parameters. This portion of command-line is used by the XTL compiler when creating the binary file of the generated C code. As an example, the XTL program below uses the CAESAR_ERROR() function for error handling, which is declared externally in the "caesar_standard.h" file and defined in the OPEN/CAESAR library libcaesar.a. Upon execution, the program will output the error message and stop.
include
"caesar_standard.h"
end_include
flag
"-I/common/Cadp/incl -L/common/Cadp/bin.sun5 -lcaesar"
end_flag
func error (string) : action
! implementedby "CAESAR_ERROR"
end_func
error ("Here occurs a fatal error. Farewell.")
PG ::= [ ( FD1 | ETD1 | EFD1 | EID1 | ELD1 )
...
( FDm | ETDm | EFDm | EIDm | ELDm ) ]
[ MD1 ... MDp ]
[ LI1 ... LIr ]
E
[ "where"
[ MDp+1 ... MDp+q ]
[ LIr+1 ... LIr+s ]
( FDm+1 | ETDm+1 | EFDm+1 | EIDm+1 | ELDm+1 )
...
( FDm+n | ETDm+n | EFDm+n | EIDm+n | ELDm+n ) ]
The expression E is the body of the program. There may also be lists of
function definitions, external directives, macro definitions, and/or library
inclusions, placed in the front of the program or at its end, after the
"where" keyword. The functions defined by FD1, ..., FDm+n are visible in the
body E of the program, as well as in all their bodies.
[GLMS13] H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT), 15(2):89-107, 2013. http://cadp.inria.fr/publications/Garavel-Lang-Mateescu-Serwe-13.html
Additional information is available from the CADP Web page located at http://cadp.inria.fr
Directives for installation are given in files $CADP/INSTALLATION_*.
Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.