The Z to SAL translator accepts Z marked up as Latex and translates it into the input file(s) for SAL.   In doing this it will assume that the first schema it encounters is the State schema and the second is the Init schema.  

We have tried to accept as many dialects of Latex Z as possible.  A list of the Latex tags we accept is available here.

Please report any errors you find.