Differences

This shows you the differences between two versions of the page.

--- start [2024/10/04 22:52] – fponzi
+++ start [2025/07/15 17:51] (current) – fponzi
@@ Line 1: / Line 1: @@
 ====== Welcome to the TLA+ Wiki ======
 This wiki is community driven, and aims to become a useful resource for TLA+ users.
-This wiki was created in response to the [[http://discuss.tlapl.us/pdfW4MH5_0fKx.pdf|2024 TLA+ community survey]]. More specifically, it aims to address the following feedbacks:
+===== TLA+ and TLC ======
+TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.  It's based on the idea that the best way to describe things precisely is with simple mathematics.  TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.
-  - **Difficulty in Understanding Existing Codebase and Documentation**: Respondents note challenges in comprehending the existing codebase and documentation. The lack of clear structure and architecture documentation, as well as the complexity of the Java codebase, pose significant obstacles for newcomers.
+TLC is a model checker for specifications written in TLA+.
-  - **Navigation and Documentation**: Navigating the various TLA+ resources and finding relevant documentation is identified as a challenge. Respondents note scattered and sometimes non-existent documentation, making it difficult to find the most relevant resources and assistance.
+<code>
-  - **Documentation and Tooling**: There is a strong consensus on the need for improved documentation, particularly in the form of better organised and comprehensive resources. This includes better documentation for the entire project, better release cycles for all TLA+ tools, and centralised documentation on a website rather than PDFs.
+----- MODULE HourClock -----
+EXTENDS Naturals
+VARIABLE hr
+HCini  ==  hr \in (1 .. 12)
+HCnxt  ==  hr' = IF hr # 12 THEN hr + 1 ELSE 1
+HC  ==  HCini /\ [][HCnxt]_hr
+------------------------
+THEOREM  HC => []HCini
+=======================
-The takeaway also sums up the mission of this wiki well:
+----- CONFIG HourClock -----
+(***************************************************************************)
+(* This is a TLC configuration file for testing that HCini is an invariant *)
+(* of the specification HC                                                 *)
+(***************************************************************************)
-> Streamlining Documentation: There’s a clear demand for better-organised documentation and centralised resources with a more modern interface to cater to users’ preferences for accessible and comprehensive guidance.
+SPECIFICATION HC
+   \* This statement tells TLC that HC is the specification that it
+   \* should check.
-This is a community-backed effort, so if you find errors or suggestions/ideas/feedback, please fix them.
+INVARIANT HCini
+   \* This statement tells TLC to check that formula HCini is an
+   \* invariant of the specification--in other words, that the
+   \* specification implies []HCini.
+======================
+</code>
 ==== Contributing ====
+These are some of the ways you can contribute.
-Contribution to the wiki are very welcome!
+=== Wiki ===
-In order to contribute you will need to register to this website for an account (it only requires username, email and password).
+Contributions to the wiki are very welcome!
+To contribute you will need to register an account on this website (it only requires a username, email and password). Should you need it, TLA+ was created by Leslie **Lamport**.
 You can learn the syntax from [[wiki:syntax|here]]. Markdown is not supported.
+=== Tools ===
+Currently the main areas are the [[codebase:start|TLC model checker]] (java), and the [[using:vscode:start|Visual Studio Extension]].
+If you're looking for some inspiration, be sure to check the monthly development update that usually has good first contribution ideas: [[https://foundation.tlapl.us/blog/index.html]]
 ----