Download Paper

FP6-7603 – TONES
Thinking ONtologiES
WP3
Figure 11: InstExp window while preparing a counterexample
The translation algorithm from ALCN into Alloy’s Relational Logic is the core of the
DL2 RL translation tool being work in progress. The algorithm has been implemented using a Java library, consisting of the packages dlAST, parser, and utilities. The translation
service may be invoked with two different kinds of input:
• a pair <TBox, ABox>
• text file in .racer format
The output is first obtained as an in-memory string containing the Alloy specification,
which can then be serialized to disk or further processed. These alternatives are provided
for better supporting usage of the tool in different scenarios. For example, in case ALCN
input is available in XML format, parsing using a freely available library can be followed
by instantiating the Abstract Syntax Trees (ASTs) built for input TBox and a (possibly
empty) ABox. From there, translation may proceed. Detailed usage instructions are given
in the next section.
11.2
DL2 RL – How to Use
In order to invoke the DL2 RL translation algorithm taking as input a .racer file, an
java.io.InputStream is to be obtained (for an example see the following Listing and
c
2007/TONES
– March 31, 2007
49/55
TONES-D15 – v.1.1