Adopting changes to the TLA+ language and standard modules #21
Description
Proposing modifications to the TLA+ language
The TLA+ specification language is documented in Part IV of Specifying Systems, together with some extensions, originally introduced as TLA+2.
The TLA+ Foundation is an independent, non-profit organization that fosters adoption of TLA+. In particular, the Foundation's Specification Language Committee (SLC) is in charge of overseeing evolutions of TLA+.
The purpose of this RFC is to describe the process for how proposals for modifications of TLA+ should be formulated, as well as the process for their adoption. It follows the spirit of the document The Future of TLA+.
The scope of the document includes proposals for changes to the TLA+ language and its standard modules, not changes to the functionality or interface of individual tools or changes concerning additional libraries, such as the Community Modules.
Presenting a proposal
A proposed change to the TLA+ language should be publicly presented as an RFC on the TLA+ GitHub site. Changes may include adding or removing language constructs, modifications of existing constructs or changes to the TLA+ Standard Modules.
The proposal must include
- a summary with a short description of the proposed change,
- a rationale for why the change is considered beneficial, together with typical use cases,
- a discussion of its costs in terms of breaking existing specifications or complicating the language,
- an unambiguous description of the proposed changes, including any modifications of the grammar and/or operator definitions,
- a discussion of changes required to the TLA+ Tools, including SANY, TLC, TLAPS or Apalache, and suggestions for how to implement them.
The TLA+ community will discuss the proposed change based on the RFC, and it should be presented at the monthly Community Meetings. The RFC must have a clearly identified champion who serves as the liaison with the SLC.
The role of the Specification Language Committee
The SLC will discuss the merits of proposed changes, following the guidelines laid out in The Future of TLA+, and taking into account the public discussions on GitHub and at the Community Meetings, in which its members may participate. It may contact the champion of the proposal for clarifications and additional details, including a proof-of-concept implementation in a relevant subset of the tools when appropriate.
If a proposed change is considered beneficial and ready for adoption, it will be made official after a formal vote of the SLC members and will be marked as adopted on the TLA+ GitHub site. If the proposal is rejected, the decision will be published on the the same site, together with reasons for rejection.