TLX.Emitter.PlusCalP (TLX v0.5.2)

Copy Markdown

Emits a PlusCal algorithm (P-syntax / begin-end) from a compiled TLX.Spec module, wrapped in a valid .tla file compatible with pcal.trans.

Summary

Functions

Generate a PlusCal P-syntax .tla string from a compiled spec module.

Functions

emit(module)

Generate a PlusCal P-syntax .tla string from a compiled spec module.