Skip to content
/ tlapy Public

Python utilities for working with TLA+ specifications

License

Notifications You must be signed in to change notification settings

johnyf/tlapy

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

About

A collection of Python tools for working with TLA+ specifications:

  • tlapy.proof_graph: convert TLA+ theorems and proofs to a graph
  • tlapy.tla_depends: plot a graph of TLA+ module dependencies
  • tlapy.tla2pdf: typeset TLA+ specifications using tla2tex.TLA
  • tlapy.tla2tex_tex: convert TLA+ to LaTeX using tla2tex.TeX, then extract the result
  • tlapy.utils.balance_hrules: rewrite title and horizontal rules to fill the column width
  • tlapy.utils.join_modules: concatenate PDF files of TLA+ modules
  • tlapy.utils.remove_proofs: remove proofs from a TLA+ file to create a "header"
  • tlapy.utils.renumber_proof_steps: proof step numbering in a TLA+ module so that step numbers are in increasing order
  • tlapy.utils.replace_even_backticks: converts inline Markdown code blocks to TLA inline code blocks

License

BSD-3, see LICENSE file.