Differences

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

--- tla:start [2019/08/26 02:25]
jonathan
+++ tla:start [2019/09/08 19:55] (current)
jonathan
@@ Line 1: / Line 1: @@
-Please download the the latest TLA+ Toolbox or on Prism (and the SEL-VM) invoke ''tla'' from the command line.
+======= TLA+ Home Page for TLA+/TLC=======
-  * [[https://youtu.be/Y11YPmPZB_w|Introductory Tutorial for TLC Modelchecker]].
-    * File: {{ :tla:bank_video.tla.zip |bank_video.tla.zip}}.
-    * Invoke as ''tla160&'' from the command line on EECS servers (or as "tla&").
-      *   [[https://github.com/tlaplus/tlaplus/releases/tag/v1.6.0|TLA 1.6 Release Notes]]
-    * We also use ''tlaplus_repl60'' ([[tla:repl:|instructions]]).
-  * Download [[http://lamport.azurewebsites.net/tla/hyperbook.html|Hyperbook]] documentation on to your own Laptop.
-  * [[http://lamport.azurewebsites.net/video/videos.html|TLA Videos]]. This is a series of video lectures to teach programmers and software engineers how to write their own TLA+ specifications.
+On Prism (or the SEL-VM) invoke ''tla'' from the command line. You can also install the TLA+ Toolbox/IDE on your Laptop.
-    * [[https://lamport.azurewebsites.net/tla/paxos-algorithm.html|Video Paxos Algorithm]]. Videos of two 1.5-hour lectures Leslie Lamport gave summer 2019 on the Paxos consensus algorithm. The algorithm is developed through a sequence of TLA+ specs.  No prior  knowledge of the algorithm or TLA+ is assumed.  The videos constitute a crash course on  TLA+.  Links to the videos, the specs, and accompanying exercises are at the link.
-  * [[http://tla.msr-inria.inria.fr/tlatoolbox/doc/contents.html|TLA Toolbox User's Guide]]
+[[https://www.youtube.com/playlist?list=PLEWQAc3YS7XaULwGamfcKUfPr9HhF2ckk|youtube playlist]] of Introductory Videos for analyzing TLA+ Specifications and checking them for specification error using the TLC modelchecker.
-  * [[https://lamport.azurewebsites.net/tla/book.html|Specifying Systems]] TLA+ Book by Leslie Lamport. {{ :tla:specifying_systems.pdf |PDF}}
-  * [[https://github.com/tlaplus/Examples|TLA Examples]]
-  * [[tla:cl|TLC from the command line]]
-===== More Details ======
-  * [[https://lamport.azurewebsites.net/tla/current-tools.pdf|Current Tools]].This document describes differences between the descriptions of the TLA+ tools in the book Specifying Systems and the currently released versions. References are to the version of the book currently available on the web. The book and this document do not describe the features provided by the TLA+ Toolbox for using the tools. They are described by the Toolbox’s help pages and the TLA+ Hyperbook.
+{{ :tla:tla-summary.pdf |TLA+ Summary}}
 ====== What is TLA+ ======
@@ Line 30: / Line 17: @@
 TLAPS is an interactive proof assistant: you provide a proof of why your system satisfies a property, and TLAPS can check if that proof is logically consistent and complete. It uses different automatic back-ends, including SMT solvers, to check proof steps, but it is still the user who designs and writes the proof. Although the effort is independent of the size of the state space, and also infinite-state systems can be verified in this way, I would not recommend using TLAPS for users who do not have sufficient experience with theorem proving.
+====== Introductory Videos TLA+/TLC ======
+==== A very simple traffic light ====
+[[https://youtu.be/Y11YPmPZB_w|Youtube: Simple Traffic Light]]. TLA+ Specification and TLC modelchecker.
+==== A Bank system with multiple accounts ====
+[[https://youtu.be/NCJYDCzo9yc|Youtube: Bank System]] with multiple accounts. TLA+ Specification and TLC modelchecker.
+  * File: {{ :tla:bank_video.tla.zip |bank_video.tla.zip}}.
+====== TLA+ Toolbox/IDE ======
+  * See [[http://lamport.azurewebsites.net/tla/toolbox.html| TLA+ Toolbox Details]]
+    * Invoke as ''tla160&'' from the command line on EECS servers (or as "tla&").
+    *   [[https://github.com/tlaplus/tlaplus/releases/tag/v1.6.0|TLA 1.6 Release Notes]]
+    * On EECS servers we also use ''tlaplus_repl60'' ([[tla:repl:|instructions]]).
+  * [[http://tla.msr-inria.inria.fr/tlatoolbox/doc/contents.html|TLA Toolbox User's Guide]]
+  * [[https://lamport.azurewebsites.net/tla/book.html|Specifying Systems]] TLA+ Book by Leslie Lamport. {{ :tla:specifying_systems.pdf |PDF}}
+  * [[https://github.com/tlaplus/Examples|TLA Examples]]
+  * [[tla:cl|TLC from the command line]]
+====== Other Videos ======
+  * [[http://lamport.azurewebsites.net/video/videos.html|TLA Videos]]. This is a series of video lectures to teach programmers and software engineers how to write their own TLA+ specifications.
+    * [[https://lamport.azurewebsites.net/tla/paxos-algorithm.html|Video Paxos Algorithm]]. Videos of two 1.5-hour lectures Leslie Lamport gave summer 2019 on the Paxos consensus algorithm. The algorithm is developed through a sequence of TLA+ specs.  No prior  knowledge of the algorithm or TLA+ is assumed.  The videos constitute a crash course on  TLA+.  Links to the videos, the specs, and accompanying exercises are at the link.
+===== More Details ======
+  * [[https://lamport.azurewebsites.net/tla/current-tools.pdf|Current Tools]].This document describes differences between the descriptions of the TLA+ tools in the book Specifying Systems and the currently released versions. References are to the version of the book currently available on the web. The book and this document do not describe the features provided by the TLA+ Toolbox for using the tools. They are described by the Toolbox’s help pages and the TLA+ Hyperbook.

Software Engineering Documentation

User Tools

Site Tools

Differences

Page Tools