Differences

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

--- start [2024/10/21 22:13] – 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.
-===== TLA+ ======
+===== 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.
+TLC is a model checker for specifications written in TLA+.
 <code>
----------------------- MODULE HourClock ----------------------
+----- MODULE HourClock -----
 EXTENDS Naturals
 VARIABLE hr
@@ Line 11: / Line 13: @@
 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>