 |
Basically, the functionality of the Kit can be stated as follows.
Input:
- A system in one of the available modelling languages.
- A property of the modelled system.
Apart from atomic propositions the syntax of properties is supposed
to be independent of the modelling language.
- A specification which checker should be used for verification.
Output:
- A result (yes/no - property holds/does not hold), and possibly
a witness/counterexample path generated by the selected checker.
In order to make the results meaningful, witness/counterexample
paths should be represented as runs of the modelled system
(i.e. not as runs of its Petri net semantics!).
Examples:
- Input: a Petri net, a formula "P1 and P2 will never be marked at
the same time". Ouput: Yes/No, possibly a sequence of transitions.
- Input: a system of communicating finite automata (CFA), a formula
"eventually, x will hold the value 2". Output: Yes/No, possibly a
sequence of state transitions in the automata.
As you can see, our aim is to hide from the user the necessary translation
of the modelled system into the checker's language. To make this approach
work with all the languages and checkers we need a common intermediary
format of the input data.
In order to integrate a new language into the Kit a new module must be
implemented with three functions:
- one function that returns the modelled system - i.e. by reading its
specification from a file and generating its safe Petri net semantics;
- one function that returns the property in question - i.e. by reading
it from a file and generating a tree representation;
- one function that presents the checker's result (given in terms
of the Petri net semantics) to the user as a run of the modelled system.
For a better understanding of how these interrelate, let us briefly review
the chronological order of events in the execution of the kit:
- Interpretation of command line arguments.
- Obtaining the modelled system.
- Obtaining the property.
- Running the checker.
- Interpretation of the result.
The functions of the new module correspond to items 2, 3, and 5 in this list.
The intermediary format mentioned above places a restriction on the
kinds of input languages we may cover. We decided to allow languages
that can be defined in terms of a safe Petri net semantics.
From this it follows that every system will (internally) be represented
by a state/transition net, more precisely by:
- a list of places;
- a list of transitions;
- a set of directed arcs between pairs of places and transitions;
- an initial marking of the places.
Additionally, we provide a mechanism for storing extra information that
might be useful for at least some checkers (like a partition on the set
of places). However, extra information should be optional - the applicability
of a checker should not depend on whether it understands the information.
In other words, the semantics of the system should be contained completely
within the data mentioned in the previous list.
It is worth noting that the intermediary Petri net format is not
an additional file format; it exists solely as a data structure inside
our program. The first function's task is therefore to construct such
a data structure so that other parts of the program can access it.
In a similar way the representation of formulae (properties) is standardised;
we are looking for a tree whose internal nodes are marked with logical and
temporal operators, and whose leaves are marked with the name of places
(of the intermediary net). A generic formula parser is provided so that
programmers who add a new language just need to implement the translation
of atomic propositions.
The list of input languages supported by the Kit is defined by the array
input_types[] in main.c. Technically, all that
is required to add a new language is to add another entry to this array.
The format of such an entry is explained in detail in formats.h.
Apart from the fields name and suffix there are
three function pointers that demand additional comments. These function
pointers define the three functions mentioned in the
Overview, in that order.
net_t (*readfunc)(char*)
This function is called by main.c. Its argument is the
modelfile given on the command line. The function should return the
intermediary net representing the system modelled in the argument.
The function may return NULL to indicate that an error
has occurred.
The structure net_t is defined in netconv.h.
The file netconv.c contains useful operations on nets,
among them:
- creation of an empty net (
nc_create_net)
- creation of places and transitions
(
nc_create_{place,transition})
- creation of arcs (
nc_create_arc)
Some more general routines are also contained in netconv.c:
nc_print (for printing important information to the screen)
nc_info (for printing information only to be displayed in verbose mode (-v)
nc_error (for printing error messages)
Currently, these functions just print messages to stdout
or stderr, respectively. However, it is encouraged to use
these instead of plain calls to printf in case later versions
of extensions of the program want to redirect/filter the output.
Examples for this kind of function can be found in the
input_types table in main.c, like
read_pep_net, read_sen_net etc.
The inner workings of such a function may vary - it's up to you.
You might want to use some yacc/lex combinations, or even call
external programs. The only important thing is that the function
returns a net for further processing.
tree_t (*formfunc)(char*,net_t,int)
This function takes the following kinds of arguments: The name of the
formula file (as given by the user on the command line), the intermediary
net under consideration and the kind of formula that should be checked.
The third argument can take values of FORM_CTL,
FORM_LTL, or FORM_REACH.
The function should return a formula over the given net, or NULL
if an error has occurred. The formula is expected to be returned as a binary
tree as defined in tree.h.
The syntax of formulae should be uniform across all input languages,
Naturally, the set of atomic propositions may vary between different
languages, but this should be the only difference - e.g., the set of
(temporal and logical) operators and their syntax should be the same.
To this end we provide a generic formula parser (formula.y).
This parser is capable of reading all three kinds of formulae
(CTL, LTL, and reachability), supports macros and can be customized to
support propositions in multiple input languages. Although it is not
a requirement we recommend that this parser be used.
If you use the parser in formula.y, your work is reduced
to coding a parser for atomic propositions. For more details read the
comments in formula.y, and for an example take a look at
read_generic_formula in generic.c.
As stated previously the function should return the formula as a binary
tree (see formula.y for examples how to construct such a
tree). The tree's internal nodes should be inscribed with temporal and
logical operators, and its leaves should be inscribed with pointers to
places in the intermediary net. The meaning of such a leaf should be
"the place inscribed upon this leaf is marked".
tree_t is a data structure defined in tree.h.
Some operations like create_tree or create_leaf
are implemented in tree.c. The constants used for inscriptions
of the nodes are taken from the automatically generated file
formula.h.
void (*outputfunc)(net_t,result_t)
This function is called after the checker has been run and the validity
of the formula has been examined. The arguments given to the function are
the net and the checker's result. The function is expected to present the
result to the user - i.e. in such a way that a statement is made about
the system originally modelled by the user. In other words, sequences
of firing transitions in the intermediary net should be interpreted as
a run of the original system.
The structure result_t is defined and explained in
netconv.h. Its most important data fields are
holds (which assumes either NC_YES or
NC_NO meaning that the formula holds/does not hold)
and example which may hold a sequence of transitions
which, if fired, provide a witness or a counterexample to the result.
Examples for output functions can be found in the table in main.c.
For Petri net languages like PEP, SENIL or APNN, the output function is
trivial; for B(PN)2 and CFA things get more complicated.
The counterexample/witness path is held in a list of type list_t.
This simple, general-purpose list structure is defined in list.h.
Elements of a list can be traversed using the for_list macro.
|
|
cs) |
© University of Stuttgart |
legal notice