Manual

• Introduction
• Using PGo
  • Installation
  • Execution
  • Annotations
    • Annotating types
    • TLA+ definitions and constants declared outside of the algorithm block (Required)
    • PlusCal procedure return values (Optional)
    • Variable types (Optional)
    • Function signatures
    • Locking (Optional)
• Translation
  • Variable declarations
  • Variable assignment
  • Macros
  • Data types
    • Sets
    • Maps
    • Tuples
  • Predicate operations
  • With
  • Processes
  • Labels
  • Limitations
• Notes on the Go library
  • Maps
  • Sets and predicates
  • Tuples
• Example programs
  • Euclidean algorithm
  • N-Queens problem
  • Dijkstra's mutex algorithm