Differences

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

--- start [2024/09/28 18:15] – fponzi
+++ start [2024/10/21 22:18] (current) – fponzi
@@ Line 1: / Line 1: @@
-====== Welcome to the (unofficial) TLA+ Wiki ======
+====== 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 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 create a PR or an issue.
+INVARIANT HCini
+   \* This statement tells TLC to check that formula HCini is an
-If you want to contribute, please check [[wiki:contributing|Contributing]] page with detailed step by step.
+   \* invariant of the specification--in other words, that the
+   \* specification implies []HCini.
+======================
+</code>
 ==== Contributing ====
-Contribution to the wiki are very welcome!
+Contributions to the wiki are very welcome!
-In order to contribute you will need to register to this website for an account (it only requires username, email and password).
-You can learn the syntax from [[wiki:syntax|here]] (markdown is not supported).
-==== About ====
+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**.
-This wiki is hosted on an Azure VM. The wiki is implemented with the [dokuwiki](https://www.dokuwiki.org/) software. If you have questions, suggestions or feedback **about the wiki**, please reach out to fponzi+tlapluswiki at fponzi.me.
+You can learn the syntax from [[wiki:syntax|here]]. Markdown is not supported.
 ----