Differences

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

--- start [2024/10/17 15:17] – fponzi
+++ start [2024/10/21 22:18] (current) – fponzi
@@ Line 2: / Line 2: @@
 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
+=======================
+----- CONFIG HourClock -----
+(***************************************************************************)
+(* This is a TLC configuration file for testing that HCini is an invariant *)
+(* of the specification HC                                                 *)
+(***************************************************************************)
+SPECIFICATION HC
+   \* This statement tells TLC that HC is the specification that it
+   \* should check.
+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 ====