====== Welcome to the TLA+ Wiki ======
This wiki is community driven, and aims to become a useful resource for TLA+ users.

===== 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 -----
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 ====

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.

----



<nspages -tree -r -exclude -subns -pagesInNs -h1 -textNs="Browse Topics:" -pregPagesOff="/start/i">