-
Notifications
You must be signed in to change notification settings - Fork 1
/
standalone-tools9cfa.html
267 lines (187 loc) · 7.25 KB
/
standalone-tools9cfa.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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
<!DOCTYPE html>
<HTML>
<!-- Mirrored from lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:38:05 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]">
<!-- 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>
<TITLE>Standalone TLA+ Tools</TITLE>
<!-- STYLE type="text/css">
H2 {line-height:45px; margin-bottom:0px; text-align: left; font-size:26px;
color:#000000}
H3 {line-height:10px; margin-bottom:8px; text-align:left; font-size:18px}
body {background-color:#ffffe4; max-width:750px;
font-family:Calibri,Trebuchet MS,Verdana;
font-size:18px;
line-height:22px;
}
</STYLE -->
<title>TLA+ Tools</title>
</HEAD>
<BODY 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>Running the TLA+ Tools Standalone</H1>
<p style="margin-top:-8px; margin-bottom:-18px">
Leslie Lamport<p>
<font size=-1><I> Last modified on 21 November 2018</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>
<h2>The Tools</h2>
The TLA+ tools are described on
<a href="tools.html">the TLA+ Tools web page</a>.
Most users run the TLA+ tools
from the <a href="toolbox.html">TLA+
Toolbox</a>. Instructions for running TLAPS, the TLA+ proof
system, should be found on
<a href="https://tla.msr-inria.inria.fr/tlaps/content/Home.html">its
web site</a>.
This page describes how to run the other tools outside
the Toolbox. Those tools, and their current versions, are: <Pre>
SANY: Version 2.1 of 23 July 2017
TLC: Version 2.13 of 18 July 2018
PlusCal: Version 1.8 of 16 May 2018
TLATeX: Version 1.0 of 20 September 2017
</Pre>
<A NAME="downloading"><H2>Downloading and Installing the Tools</H2></A>
The distribution comes as a zip file or a jar file. They are available
by following the link below.
Please thank Microsoft and HP for the open-source release of the
code by reading the following agreement.
<p>
<b>By installing, copying, or otherwise using this software, you agree
to be bound by the terms of its license. </b>
<!-- A HREF="license.html">Read the license.</A></b -->
<font class = "popup-blue" color="blue" id="license" onclick="popupw('license.html',450,650)"><b>
Read the license.</b></font>
<p>
<A
HREF="https://github.com/tlaplus/tlaplus/releases/latest"><b>-- DOWNLOAD
THE TLA+ TOOLS --</b></A><BR>
<A
HREF="https://tla.msr-inria.inria.fr/tlatoolbox/dist/"><b>-- ALTERNATE DOWNLOAD
SITE --</b></A>
<p>
Separate directions for completing the installation on Windows and on
Unix from the zip file are given below.
<P>
<H3 id="h2windows" class="show-hide"
onclick="showHide('hide-windows','windows')">
Windows
<font id="hide-windows" >
[show]</font></H3>
<DIV id="windows" class = "hidden-div">
Choose (or create) a folder into which you want to put the tools
and unzip the downloaded file into that folder.
Let's suppose that your folder is 
<TT>c:\user\myfolder</TT> .
This will create a subfolder of  <tt>myfolder</tt> 
named  <tt>tla</tt>  that has three subfolders, each
containing one of the tools.
You must then add 
<TT>c:\user\myfolder\tla</TT> 
to your CLASSPATH variable.
To do that, open the  
<EM>Control Panel</EM>  and click on 
<EM>System</EM>.
Click on 
<em>Advanced system settings</em>,  select the
<em>Advanced</em> tab, and then click on
<EM>Environment Variables</EM>.
Look for the CLASSPATH variable. If it exists, append 
<TT>;c:\user\myfolder\tla</TT> 
to the end of it.
If not, create a new CLASSPATH variable whose value is 
<TT>c:\user\myfolder\tla</TT> .
<P>
</DIV>
<H3 id="h2unix" class="show-hide"
onclick="showHide('hide-unix','unix')">Unix
<font id="hide-unix" >
[show]</font></H3>
<DIV id="unix" class = "hidden-div">
Choose (or create) a directory into which you want to put the tools
and unzip the downloaded file into that directory.
Let's suppose that your directory is 
<TT>/udir/user/mydir</TT> .
This will create a subdirectory of  <tt>mydir</tt> 
named  <tt>tla</tt>  that has three subdirectories, each
containing one of the tools.
You must now add  <TT>/udir/user/mydir/tla</TT> 
to the CLASSPATH environment variable.
Assuming you're running the C shell or some derivative, you do this by
typing
<PRE> setenv CLASSPATH /udir/user/mydir/tla</PRE>
However, you'll probably want to have the CLASSPATH variable set
automatically when you login.
To do this, your 
<TT>.login</TT> 
or 
<TT>.csh</TT> 
file must contain a command to set that variable.
If a command
<PRE> setenv CLASSPATH ...</PRE>
already exists in your 
<TT>.login</TT> 
or 
<TT>.csh</TT> 
file, just add the command
<PRE> setenv CLASSPATH $CLASSPATH":/udir/user/mydir/tla"</PRE>
after it.
Otherwise, just add the command
<PRE> setenv CLASSPATH /udir/user/mydir/tla</PRE>
</DIV>
<H2>Running the Tools</H2>
To run the tools, you must have Java installed on your
machine.
If you're running Unix, it is probably already there.
If you're running Windows, you can get Java
<A HREF="https://www.java.com/en/download/manual.jsp">here</A>
or
<A HREF="https://developer.ibm.com/javasdk/downloads/">here</A>.
After installing the tools and Java, you run them in a Windows
<i>Command Prompt</i> window or in a Unix shell by typing the
appropriate one of these commands
<PRE> java tlc2.TLC
java tla2sany.SANY
java pcal.trans
java tla2tex.TLA
</PRE>
followed by the command arguments, which consist of zero or more
switches followed by the name of a <TT>.tla</TT> file.
(The extension <TT>.tla</TT> can be omitted when typing
the file name.)
</td>
</tr>
<!-- Bottom Back button -->
<tr>
<td>
<a class="back-link" style="display:none" href="#">
<p style="margin-top:-50px"><b>Back</b>
</p>
</a>
</td>
</tr>
</table>
</BODY>
<!-- Mirrored from lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:38:05 GMT -->
</HTML>