Overview of the translator

Overall Translation Procedure

Basically, the Circus to CSP || Z translator, namely CircusZCSP, is supposed to translate a Circus model in Unicode or the LaTeX markup to a model in CSP || Z. And a CSP || Z model actually consists of two files: one Z specification and one CSP specification. In order to manipulate constructs of a Circus model by our link definition, the first step of the translator is to parse and typecheck the model to find syntax and type errors, and sequentially turn the model in Unicode or LaTeX into an internal abstract syntax tree (AST) if there is no error detected. Then the translator manipulates the internal AST and converts it into internal representations of the target Z model in ZRM and the target CSP model. In the end, these internal Z and CSP models are output from the translator, which results in a final Z model in LaTeX and a CSP model in CSPM. Then they are able to be model-checked by ProB.

The overall translation procedure is illustrated in detail in Figure

Since the parser and typechecker for Circus have been integrated into the CZT project, in order to reuse them, our translator is written in Java and based on CZT as well. In the figure, we use different node shapes to denote input and output files (rectangle with shadow), existing modules in CZT (rectangle with round corners), and newly developed modules (rectangle with round corners and double lines). Each step is described as follows.

• Markups of input Circus models, that the translator can support, rely on the parser and typechecker in CZT. The LaTeX markup is normally used for the input model.
• Then the Circus parser is responsible for the generation of AST from the input LaTeX model.
• Afterwards, the Circus typechecker checks type, scope or naming errors in the AST according to type inference rules, and additionally annotates that AST with section and type environments. The new AST is abbreviated to AST_+.
• The new R_{wrt} module rewrites an AST_+, according to our rewrite rules defined in Section~\ref{sec:link_rewrite}, to an AST_{+R}, a rewritten AST_+. The internal implementation of the R_{wrt} module is displayed in Section~\ref{sec:trans_rewrite}.
• After the rewrite, the AST_{+R} is translated to Z and CSP by \Omega and \Phi separately.
• For the \Phi function, it generates the final CSP model from AST_{+R}. Because CZT is not capable of parsing and typechecking CSP, the output of \Phi is a CSP model (``a_csp.csp'') directly. The detail of the \Phi module is given in Section~\ref{sec:trans_phi}.
• For the \Omega function,
  • it merges the state part of Circus from the input AST_{+R} to form an ASTZ which is an AST for a Z model in ISO Standard Z dialect,
  • this ASTZ is converted to its corresponding LaTeX markup by the Z Pretty Printer in CZT,
  • then the LaTeX markup is fed to the Z Parser and TypeChecker in CZT to check if the translated Z model is correct and free of errors, and at the same time an annotated AST, ASTZ_+, is generated if no error is found,
  • finally the ASTZ_+ along with the LaTeX markup of the Z model from the Pretty Printer are input to \Omega_2 which transforms them into a Z model in ZRM (``a_z.tex'').
  • the \Omega modules are described in Section~\ref{sec:trans_omega}.
• Eventually, a resultant CSP || Z model, which is composed of one CSP model and one Z model, is obtained.