The Z2SAL User Guide

The Z to SAL translator is provided as a Java application with a very simple user interface. Currently, the tool has two operating modes, in which it will either translate a single Z specification for model simulation, or model-checking purposes; or it will translate a pair of Z specifications and a retrieve relation, for refinement checking purposes. The translated output is placed in the same directory as the source. This will consist of one or more SAL output files.

The Z to SAL translator accepts files containing marked up Z, in several possible LaTeX Z styles. We seek to accept as many LaTeX dialects of Z as possible: see the complete list of accepted LaTeX tags. When translating single Z specifications, the translator will always assume by convention that:

• the first Z schema encountered is the state schema; and
• the second Z schema encountered is the INIT-schema

When translating two Z specifications, the same assumption is made for the abstract and concrete specification, but the tool expects that:

• the retrieve relation is supplied as a Z operation schema

The Z to SAL translator outputs context files in the SAL format, which are designed to be used as the input to SRI's Symbolic Analysis Laboratory tool suite. The output typically consists of:

• a main context, containing the automaton for the Z specification
• one or more library contexts, modelling the Z mathematical toolkit

When translating two Z specifications and a retrieve relation, the main context contains the merged automaton from both input specifications. The produced output may be simulated directly in the SAL simulator, or further temporal logic properties may be added by hand, in order to perform model-checking (see Model-Checking Examples).

Starting and Exiting the Translator

The Z2SAL translator may be launched in two ways, depending on how your operating system is set up to run Java. The directory from which you launch the tool is not critical. To launch the tool:

• double-click on the jar-file z2salddmmyy.jar; or
• enter on the command line: java –jar z2salddmmyy.jar

where the ddmmyy denotes the dated release version of the Z2SAL tool (or alternatively, the undated working release is called ztosalrelease.jar). The tool may be exited in two ways:

• click on the large Close Z to SAL Translator button; or
• close the GUI main window, using the window controls

To translate a single Z specification for simulation, or model-checking purposes:

• click on the large Translate Z into SAL button
• navigate to a directory and select the LaTeX source file for the Z
• click on the small OK button to commit

and after the last step, or more output SAL files will then appear in the same directory as the input source. To see how to simulate, or model-check the result, please refer to the Model-Checking Examples.

To translate a pair of Z specifications and a retrieve relation for refinement checking purposes, you repeat the above steps in a given order, for each Z specification:

• click on the large Refine button
• select the LaTeX source file for the abstract Z specification
• click on the small OK button to commit
• select the LaTeX source file for the concrete Z specification
• click on the small OK button to commit
• select the LaTeX source file for the Z schema for the retrieve relation
• click on the small OK button to commit

All Z basic types are converted to SAL symbolic enumerations, which are populated with three elements by default. To change this default value:

• click on the rectangular button Change default cardinality of basic types
• enter the desired cardinality in the pop-up dialog box
• click on the small OK button

If the Z2SAL translator encounters any LaTeX expression that it cannot recognise, or otherwise fails due to exceeding buffer limits, it will output an error log file, in the same directory as the input source. The name of the error log file is derived from the input file. The error log indicates at what point in the input the fault was detected in the input source.