Running ZANS

 

ZANS is a system that provides for the direct animation of Z specifications, and provides a means of expressing Z using the ASCII character set. The ability to enter Z specifications using only the keyboard character set is a unique characteristic of ZANS.

 

The ZANS system runs on the CS Linux workstations (not on the HPs). In order to run this system, it is necessary to copy all the files except 'zans' from the directory /opt/zans into the directory containing the specification you wish to analyze/animate -- these are auxiliary files and the software only looks for them in your working directory. Don't forget that you need to include a 'zans.cfg' file in this directory too if you intend to use an ASCII format (sample in the class directory).

 

The documentation for this system is found on its Web site (see our class page) and consists of two PostScript documents. The primary document is the ZANS Tutorial. But you will also need the ZTC Manual. The ZTC (Z Type Checker) software is obsolete, but the Appendix in this document gives the ASCII equivalents for Z that are used in ZANS, while the ZANS Tutorial does not. For convenience, links to PDF versions of the two important Zans documents appear on the class Web page.

 

The /opt/zans directory contains a couple of examples illustrating the input format. Also, our class directory contains the ZSL (box format) version of the Diller PhoneDB specification. Loading a specification into ZANS results in syntax and type checking, and the 'analyze' command and 'execute' command provide useful analysis and testing options.

 

Note that when providing inputs for "basic types", ZANS gives a type error if the value is an integer (a different pre-defined type in ZANS). Therefore, when inputting 'Phone' values with PhoneDB, you must use an identifier such as xxiv (e.g., instead of 24).