-
Notifications
You must be signed in to change notification settings - Fork 1
/
learning.html
226 lines (169 loc) · 6.99 KB
/
learning.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
<!DOCTYPE html>
<HTML>
<!-- Mirrored from lamport.azurewebsites.net/tla/learning.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:31:29 GMT -->
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<META NAME="GENERATOR" CONTENT="Mozilla/4.05 [en] (X11; I; OSF1 V4.0 alpha)
[Netscape]">
<!--
%&b&<b>#</b>&
%&c& <b>#</b> &
-->
<!-- The following loads the style sheet for the html files of
the tla web site -->
<link rel="stylesheet" type="text/css" href="tlaweb.css">
<script src="tlaweb.js"> </script>
<SCRIPT>
noLinkName = "Learning";
</SCRIPT>
<title>Learning TLA+</title>
</HEAD>
<BODY BGCOLOR=#ffffe4 onload="initialize()">
<table id="main">
<tr>
<td id="main_leftcolumn" >
</td>
<td id="main_contentcolumn">
<table>
<tr >
<td style="vertical-alight:top">
<div id = "showleftcol"> </div>
<H1>Learning TLA+</H1>
<p style="margin-top:-8px; margin-bottom:-18px">
Leslie Lamport<p>
<font size=-1><I> Last modified on 19 August 2019</I></font>
</td>
<td style="vertical-alight:top;width:auto">
</td>
</tr>
</table>
<HR style="margin-bottom:-5px;margin-top:-11px">
<P style="margin-top:0px"> </P>
<DIV class="hidden-div" style="color:red;margin-bottom:-22px"><b>
You'll miss a lot on this web site unless you enable Javascript
in your browser. </b></DIV>
<H2><a
href="http://lamport.azurewebsites.net/video/videos.html">The
TLA+ Video Course</a></H2>
<DIV>
A series of video lectures on TLA+ that assumes only a basic understanding
of programming concepts.
Most beginners will find this the best way to learn TLA+.
However, it does not discuss PlusCal. Useful TLA+ operators
not described in the video are explained <a href="http://lamport.azurewebsites.net/video/not-in-video.pdf">here</a>.
</DIV>
<H2 style="text-decoration:underline"> Learning PlusCal</a></H2>
<!-- <a href="learning.html"> -->
<DIV>
<!-- H4 style="margin-top:0px;margin-bottom:3px"-->
<H4 id="h2hillel" class="show-hide" onclick="showHide('hide-hillel','hillel')"
style="margin-top:5px;margin-bottom:13px;font-size:22px"><a name="hillel">
Hillel Wayne's Web Site and Book
</a>
<font id="hide-hillel" >[show]</font></H4>
<DIV id="hillel" class = "hidden-div">
<B><a href="https://learntla.com/introduction/">The LearnTLA Web
Site</a></B>
This web site, written and maintained by Hillel Wayne, is a beginning
course in PlusCal. It covers just about all of PlusCal's
programming-like constructs, but not all of the TLA+ mathematical
operators that can be used in PlusCal expressions. There are
currently a number of minor problems with this course, plus one major
one. A PlusCal algorithm can be written in either of two syntaxes;
the book uses the P syntax, while most engineers will prefer
the C syntax. I hope these problems will eventually be corrected.
<p>
<B><a href="practical-tla9020.html?back-link=learning.html#hillel?unhideBut@EQhide-hillel@AMPunhideDiv@EQhillel">Practical
TLA+</a></B>
This links to a web page about a book by Hillel Wayne that
provides a good complete course on PlusCal.
The page contains a link to the book and my detailed comments
on it.
</DIV>
<H4 id="h2manual" class="show-hide" onclick="showHide('hide-manual','manual')"
style="margin-top:15px;margin-bottom:3px;font-size:22px"><a name="manual">The PlusCal Manual</a>
<font id="hide-manual" >[show]</font>
</H4>
<DIV id="manual" class = "hidden-div">
<!-- H4 style="margin-top:15px;margin-bottom:3px">The PlusCal Manual</H4-->
PlusCal has two syntaxes: a C-syntax similar to that of C-based
languages like C# and Java, and a P-syntax similar to that of
older languages like Pascal. Most users will prefer the
C-syntax.
There are
versions of the manual for both:
<blockquote style="margin-top:5px">
<A HREF = c-manual.pdf>C-Version</A>
<A HREF = p-manual.pdf>P-Version</A>
</blockquote>
</DIV>
<!--H4 style="margin-top:15px;margin-bottom:3px">Papers About PlusCal</H4 -->
<H4 id="h2papers" class="show-hide" onclick="showHide('hide-papers','papers')"
style="margin-top:15px;margin-bottom:3px;font-size:22px"><a name="papers">
Papers About PlusCal</a>
<font id="hide-papers" >[show]</font>
</H4>
<DIV id="papers" class = "hidden-div">
<A HREF = "http://lamport.azurewebsites.net/pubs/pubs.html#pluscal">The PlusCal Algorithm Language</A>
<p style="margin-top:5px">
<A HREF = "http://lamport.azurewebsites.net/pubs/pubs.html#dcas">Checking a Multithreaded
Algorithm with +CAL</A>.
</p>
<!-- (Also see <A HREF = "dcas-example.html">this example</A>. -->
</UL>
</DIV>
</DIV>
<H2><a href="book9020.html?back-link=learning.html#book">The TLA+
Book</a> <a name="book"></a></H2>
<DIV>
A book titled <em>Specifying Systems</em>
that you can download. It contains a complete description
of TLA+ and the TLC model checker as of 2002 when it was published,
which was before the Toolbox was developed. There have been
changes to the TLA+ language since then--the major ones being the
addition of recursive operator definitions and of
constructs for writing proofs. All the changes are
described
<a href="tla29020.html?back-link=learning.html#book">here</a>.
A 7-page <A href =
"summary-standalone.pdf">"cheat sheet"</a>
extracted from the book
summarizes the TLA+ language and definitions from its standard
modules.
</DIV>
<H2><A HREF="hyperbook9020.html?back-link=learning.html#hyperbook">The
TLA+ Hyperbook</A> <a name="hyperbook"> </a></H2>
<DIV>
This is a hypertext book that I intended to be the way to learn TLA+
and PlusCal, until I realized that people don't read anymore and I made
the video course. It's unfinished, but it still provides a good
introduction to TLA+, PlusCal, and the TLAPS proof system.
</DIV>
<h2><a name="google-group"><A HREF=
"https://groups.google.com/forum/?fromgroups#!forum/tlaplus">The
TLA+ Google Group</a></a></h2>
You can use this group
to communicate with members of the TLA+ community, including the
maintainers of the tools. Post a message if you have a question, want
to report a bug, or just want to tell us what you're doing with TLA+.
The easiest way to post a message is to send email to
<code>x@googlegroups.com</code> where <code>x</code> should be replaced
by <code>tlaplus</code>.
</td>
</tr>
<!-- Bottom Back button -->
<tr>
<td>
<a class="back-link" style="display:none" href="#">
<p style="margin-top:-30px"><b>Back</b>
</p>
</a>
</td>
</tr>
</table>
</BODY>
<!-- Mirrored from lamport.azurewebsites.net/tla/learning.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:32:27 GMT -->
</HTML>