State part

According to Figure (Overall translation procedure), after the rewrite stage, the rewritten Circus AST_{+R} is translated to the final Z by \Omega_1 and \Omega_2.

• Step_1: merge state paragraphs from all basic processes into one final state paragraph State, identify all initial schemas and merge them into one final initial paragraph Init, and merge other schemas as well by \Omega_1 Rule~\ref{omega1:rul_st_merge}.
• Step_2: these new state paragraph, initial paragraph, and other schemas form a new ISO Standard Z model which is an AST in ISO Z format, ASTZ.
• Step_3: then use the Z Pretty Printer in CZT to output this model in the \LaTeX\ markup.
• Step_4: after that, the Z \LaTeX\ markup is fed into the Z parser and typechecker in CZT to check whether the model is free of syntax and type errors. If errors are detected, then we need to check the input Circus model and the translation rules to find out the causes.
• Step_5: if no error is found, then a ASTZ_+ in Z is output from the Z typechecker.
• Step_6: finally the \Omega_2 module translates the inputs---ASTZ_+ and the Z \LaTeX\ markup---to the final Z in ZRM \LaTeX\ markup by \Omega_2 Rule~\ref{omega2:rul_struct} to \ref{omega2:boolean_type}.