A translator from a Circus model to CSP ||b Z in terms of CSP || B. It is used in my research to model check Circus by linking to CSP || B, then use ProB to model check the resultant model.
This translator is developed based on Community Z Tools (CZT).
More information about its usage, its research context, and design can be found on its Wiki.