* lisp/tla+-mode.el (tla+-java-path):
(tla+-dot-binary):
remove some default paths that may be not useful or
helpful for other users.
(tla+-run-sany):
(tla+-run-model):
(tla+-run-pluscal):
(tla+-run-tlatex):
(tla+-run-model): add an error check (if the
tla+-tlatools-path is not set, print an error message)
(tla+-run-dot): run dot only when the binary to dot
is given.
* lisp/tla+-mode.el: update URLs, remove
unnecessary comments, cleanup whitespace and
wrap lines.
(tlc-widget-example): if a TLC cfg already
exists, copy it to .old.<seconds>. erase
the buffer then and insert the new TLC
config into the buffer.
Add the current time to the tlc config.
* org/Test.org: add an example org file.
this shows the usage of org-babel-tangle in
combination with TLA+ (it may be used to
further comment on TLA+ specifications).
* lisp/tla+-mode.el (tla+-tlc-depth): tune depth
parameter, default to 1000 now.
(tla+-tlc-workers): tune worker threads (at least
2 threads should be used by default)
(tla+-dot-convert, tla+-dot-binary): dot(1)
customization variables.
(tla+-run-dot): elisp function to run dot(1) and
convert the state graph to a PNG file
(tla+-run-model): automatically generate the PNG
output file, change the window handling. It
seems better to only show the tlc buffer output
once (when it is a newly created buffer). The
user may kill it, or arrange it in such a way
that the output can be read by another tlc model
check run. Also: set the bufffer to readonly.
(tlc-widget-example): remove the cfgname; seems
that the lambda expressions do not see the cfgname
anyway so I have to reconstruct it.
* ChangeLog: add a changelog file
- move documentation to the `describe-mode' section
- implement TLC command line options: for each TLC
config file, there might be a .cfgtlcopt file that
contains an association list for controlling the
parameters when running the TLC model checker.
- add tla+/read-options, tla+/write-options and
tla+/add-option to manipulate the option
- extend the widget to allow selecting various
options.
- use the TLA+ mode for the .cfg file as well; insert
a local variable block for selecting the appropriate
emacs mode.
- compilation output buffers (sany, tlc) store
the name of the TLA+ file.
this can be used to jump back to the buffer
if the tla+/find-error-marks highlights
"line:column" markers.
- use tla+/find-error-marks with the TLC output
- add additional tlc global setting
this commit adds some references to get the
tlatoolbox.jar.
i also changed the behavior of running sany
and tlc slightly: if a new window pops up,
i switch back to the tla buffer. a simple
c-x 1 gets rid of the message buffer.
this commit adds the new keyword
LET..IN as seen in chapter 5. Aditionally, the
tla+-run-tlatex-dvi comment has been clarified
i.e. an explanation for the argument was added
- add comments
- add keybord shortcuts
- add modul operators (from naturals, sequences)
- add functions to mark error messages in the SANY
check buffer.
this commit adds
- more comments,
- change the path to simple binary name. with that, the
$PATH variable may be used. Hard coding the path is
unnecessarily restrictive.
- add dvips and dvipdf convertion (two additional customization
parameters define the path to the dvipdf(1) and dvips(1)
programs
- add action and temporal operators (i.e. functions to insert
those symbols). the help text is the one found on the tla+
cheatsheet.
- more syntax highlighting for more constants and types
goal is to implement a convenient mode to read and write
TLA+ specifications. This commit adds the first few
functions to
- create a new module
- run SANY on a TLA+ module
- run TLaTeX export and create DVI file format
- some bascic font-highlighting
- comments can be created
Christian Barthel
bch