SAL to CDL Translation

User Guide

Author: Tamim Nassar
Last updated: 1/5/2005

In this document:

1. Overview
2. System requirements
3. Download and running instructions
4. Unhandled Translation Cases

Overview

This application is a translator that transforms programs written in SAL to a CDL program. However, due to functionality differences between the two languages, only the modules and variable declarations in SAL will be translated, leaving the assertion statements and function declarations to be translated in future versions.

System requirements

The application is tested to run properly under the following platforms:

1.  Linux/UNIX with Java Runtime Environment v1.4.0 or higher.
2. Windows XP with Java Runtime Environment v1.4.0 or higher.

Download and running instructions

Download the application zip file from the downloads page.

Create a folder where you want to put the application and extract the zip file into it.

To run the application under windows platform follow these steps:

1. In the command line of a terminal/shell, go to the folder where the application is located.
2. Run the translate command as follows:
   • translate [-d] <input file name> <output file name>
     The "-d" flag indicates that debug messages should be printed.

Note that HOLD_PREVIOUS always appears in the result core files.

The application also has a configuration file that defines the location of the sal.dtd, cdl.dtd and xml2cdl.xsl files. The configuration file is called config.xml. It is an xml file that has a root element "configuration" which has three elements: sal_dtd, core_dtd and xml_to_core. Each one of these elements contains information about the path of the specific file and the default path of the file. The default path is used when the file is not found.

Unhandled Translation Cases

Here are some cases that the application doesn't translate correctly:

1. Renaming: The core language does not contain renaming, and the translation problem is yet to be solved.
2. Let Expressions:  The translation problem is yet to be solved.
3. Nested types: Explicit declaration is required in all type declarations including arrays.
   • Array [1..N] OF INTEGER is allowed if N a constant.
   • Array [x:INTEGER | x<N] is not allowed.
4. Multisynchronous/Multiasynchronous composition. A possible solution is to copy the synchronized element several times. However this may not be applicable for a large number of synchronizing.
5. Additional info.
6. Function declarations and complex type (such as lists and trees) declarations cannot be translated. Instead, where a function appears in the SAL code we translate it as an identifier that starts with "F#" followed by the name of the function.
   A possible translation for the functions is to create modules with a many transitions, each executing a command in the function, and where the sequence of the transition execution is guarded by a program counter variable.
7. Constrains on some types are not checked. For example, core does not have non-zero integers. If the SAL program has a non-zero integer, the translator assumes that the values assigned to that variable are correct, and thus the resulting core program does not check the values in the translated variable which is represented as a normal integer.
8. Some types don't exist in core such as the non-zero integer which exists in SAL. We assume that when such a type exists it will have only valid values and therefore the core program will not check the validity of its values.