[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
How to exchange high level net annotations
Dear all,
I find it rather difficult to relate some of the last recent chat style
postings to the subject "structuring the discussion".
I suggest that every posting be related to one of the issues discussed so
far. I identified the following topics:
* Which topics require further discussion (so my list is self-extensible!)
* How (and with whom) to proceed in the standardisation process
* How to exchange layout information
* How to exchange high level net inscriptions
* How to cover non-standard net elements and annotations (time etc.)
* How to exchange verification results
* Which kind of strcturing be supported
In the following essay, I approach the problem of exchanging high level
net inscriptions.
SITUATION
---------
There is a lot of tools supporting high level nets, many of which with a
strong modeling and simulation component and some implemented verification
techniques. Some tools integrate third-party tools such as model checkers
etc. for increasing their verification capabilities. For simplifying
things, I concentrate on the core of HL nets (i.e. tokens that carry data)
and ignore issues like time, structuring etc. that, though present in most
HL net tools, relate to topics i'd like to discuss separately.
In a HL net, we typically have
* a global information text where data types, maybe operations on
these data types and other notation can be specified.
Tools use different languages for this purpose (ranging from
tools only offering simple enumeration types to tools invoking
complete programming languages of different paradigms)
* labels that assign a data type to each place, specifying the kind of
data that a token on a place may carry.
This is usually a simple place-to-sort mapping.
* labels that assign patterns of data to each arc.
Through assigning values to variables one specifies data values to
be carried by tokens to be removed or produced.
Tools differ in the kind of patterns they support. Some support just
variables, some support tuples of variables, some support term
expressions (i.e. term structures that evaluate to a single value),
some support multiterm structures (i.e. term structures that evaluate
to a set or multiset of values). In the latter case, the _number_ of
values (and thus the number of tokens to be produced or comsumed)
depends on the particular assignment to the variables. Languages used
for annotating arcs range from simple ones to full programming
languages.
* guards in transitions that specify feasible assignments to the
variables appearing in the arc annotations.
Some tools do not support guards at all, some support simple boolean
expressions, some support involved computations (statement sequences
of programming languages), some do even support queries to external
data bases (and can bind variables to query results) and so on and so
forth.
So, exchanging a HL net between any pair of tools such that the received
net is behaviourally equivalent to the sent one is a rather hopeless
undertaking. Therefore, I focus on ways to exchange HL information such
that the received net is at least an approximation of the sent one
(meaning that at least part of the behaviour can be preserved).
EXCHANGE SCENARIOS AND USEFUL APPROXIMATIONS
--------------------------------------------
For which purpose does it make sense to exchange HL nets, and what kind of
approximation could fit?
* Export to graphical editor
Sometimes, HL net editors have restricted features for drawing nets.
Being able to export HL nets to general graphical editors (or to tools
that can generate input for such tools) gives us the opportunity
to do some follow-up treatment on tool-made pictures before including them
as a figure into some paper or text book or so. For this purpose, the
semantics of HL net inscriptions is irrelevant, and a pure textual
transfer is satisfactory.
* Export to low level net tool
Export from HL nets to LL nets makes sense since LL nets do not suffer so
much from the babel of tongues discussed above. Thus, they are easier to
control from a HL net platform than other HL tools, they are sometimes
specialised to verification, offer a broader range of verification
techniques, and can serve as gateways to third party tools that are not
based on Petri nets (see, for instance, Esparza's model checking kit
project that conncets model checking tools to LL nets).
There are two different ways to generate LL nets from HL nets. The first
one - unfolding - consists of creating a LL net place for every
data value of a HL net place, and a LL net transition for every feasible
variable binding. Creating such a net requires full understanding of the
net inscriptions of the HL net. Thus, this task can only be done by the
exporting HL net tool itself, or a tool that understands the exporting
tool's syntax which just shifts the problem to the exchange between those
two tools. Therefore, I do not see any specific kind of approximating HL
net inscriptions that unfolding to a LL net is specifically supported.
The other way of getting a LL net from a HL net is the so-called sceleton
approach where the LL net is obtained just by ignoring the HL net
annotations. There are some behavioral implicatations between a HL net and
its sceleton (for instance, for reachability in the HL net, reachability
in its sceleton is necessary). Since ignoring information is a rather
natural feature in XML, I suggest to support creating a sceleton just by
reading a HL net file by a LL net tool. The major problem in this context
is the determination of arc multiplicities in the LL net. This number must
be determined through counting the different patterns in the arc
inscriptions. A serious problem occurs when arc patterns are multiset
expressions. For those cases, the sceleton approach does not work.
Still, if some result can be achieved not involving transitions with
multiset terms in their environment, this result is welcome.
Thus, I suggest to use a syntax that easily allows us to count the number
of tokens coded by arc inscriptions, and to detect easily those cases
where that number is unknown or varies depending on the variable bindings.
To my mind, a clear syntactical distinction between simple valued and
multiset valued terms would do sufficiently well.
* Export to other HL net language
There is a lot of reasons to exchange HL nets between different HL net
tools (and thus different inscription languages). I see several
opportunities to exchange full inscription information. All these
opportunities are however based on the assumption that despite of the
richness of all the inscription languages, these languages share some
easily transferrable features that are frequently used. Thus,
behaviourally equivalent export could be granted at least for those
popular features.
Data types
----------
Though there are many different type concepts, we could try to exchange at
least some standard types, such as boolean, naturals (and finite
intervals,...) and some standard schemes of aggregation (like cross
products). I suggest to have a language that
- allows us to specify a data type fitting to the common subset
- contains a special type "other", attributed with a textual
description in the exporting tool's native language.
So, at least data types inside the common base can be exchanged
semantically consistent between a broader community, while for the
remaining types it is easy to detect incompatibility (unless the importing
tool understands the exporting tool's language).
If some exporter finds it too difficult to map its own data types to the
common base, there is no problem to use "other" also for common types,
though the quality of the exchanged file decreases. For nets that stick
partly to the common data types, we can (as already discussed for
sceletons) hope for results not relying on "other" typed net elements.
I do not want to make a distinguished proposal concerning the list of
commonly supported types without getting some oppinions from HL
specialists. However, it should be as large as possible, but small enough
to enable "downgrading" to HL tools with poor type concepts.
Arc annotations and transition guards
-------------------------------------
The exchange of arc and transition annotations should follow the same
principle: define some common base that exporting tools can stick to as
often as possible, and provide some "other" feature for inscriptions that
cannot be mapped onto the common base. The syntactical term representation
as described in the HL net standard (is there still the concept of
syntactical conformance?) could fit as a frame. Those tools that only
support variables (or tuples) and no complex terms as arc inscriptions,
usually can easily transform arc terms to transition guards.
For some operations appearing in terms, we should foresee a fixed meaning
(such as +,-,*,/,AND,OR,=,<, ....). For the remaining symbols, we should
provide the opportunity to optionally specify their meaning in the
exporting tool's native language.
This way,
(a) exclusive use of symbols with fixed meaning leads to full translation.
(b) use of other symbols allows to transfer to
(b.1) tools that understand the exporting tool's language, or to
(b.2) tools that are able to cross-compile that language into their
own one
(c) tools with poor languages can treat some fixed-meaning symbols like
"other" ones
Item (b.2) could become more relevant at some time in the future...
With fixed-meaning expressions I hope to cover most of the
frequently occurring simple side-effect free HL net annotations.
Heavy stuff like extensive computations requires cross-copmpiling
capabilities. Maybe, it is possible for annotations with non-fixed
meaning, to at least specify the range of possible values. So an
importing tool can, for instance, simulate a database query occurring in
the exporting tool, by pure non-determinism. This way, the behaviour can
be preserved at least to some extend.
SUMMARY
-------
I distinguish the following levels of approximation
(1) pure text
(2) ability to count number of tokens (or specify "varies")
(3) fixed meaning subset of data types, arc and transition inscriptions
(4) "other" features in all parts of the inscription, augmented by
additional specifications given in the exporting tool's language,
and some kind of "rough" information such as range of values
(4) any kind of private or bilaterally used information
Every exporting tool can choose to which degree it tries to involve
fixed-meaning terms. The amount of using these subsets determines
the range of exchangeability.
Due to the impossibility of full equivalence between export and import,
large common subsets seam to be the only feasible way to exchange
HL-nets at least partially. We should approach at least some kind of
exchanging HL nets since otherwise the XML exchange format would not be
accepted by a broader community.
Supposed that my rather general proposals find acceptance, the major open
problem is to collect what should be included in the common parts.
In the second XML meeting in Aarhus, we agreed upon not to attempt to
include any HL net exchange beyond level (2) into an early version of an
XML format, so we have plenty of time to discuss the issue carefully.
Best regards
Karsten Schmidt
mail: Karsten Schmidt : phone: (+49)(30) 2093 3083
Humboldt-Universitaet : fax: (+49)(30) 2093 3081
zu Berlin : e-mail: kschmidt@informatik.hu-berlin.de
Institut fuer Informatik : www: http://www2.informatik.hu-berlin.de/~kschmidt
10099 Berlin, Germany : office: 12489 Berlin, Rudower Chaussee 5, R. 4.4.04