handling of TLC config files
* 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).
This commit is contained in:
Christian Barthel
parent
6ba78769a5
commit
6d84767a52
|
|
@ -503,9 +503,9 @@ Configuration:
|
|||
M-x describe-variable <variablename>
|
||||
|
||||
Getting, and Using the tlatoolbox:
|
||||
[1] https://tla.msr-inria.inria.fr/tlatoolbox/dist/
|
||||
[2] https://lamport.azurewebsites.net/tla/tools.html
|
||||
[3] https://lamport.azurewebsites.net/tla/standalone-tools.html
|
||||
[1] <https://tla.msr-inria.inria.fr/tlatoolbox/dist/>
|
||||
[2] <https://lamport.azurewebsites.net/tla/tools.html>
|
||||
[3] <https://lamport.azurewebsites.net/tla/standalone-tools.html>
|
||||
\\{tla+-mode-map}
|
||||
Turning on Text mode runs the normal hook `text-mode-hook'."
|
||||
(setq-local font-lock-defaults
|
||||
|
|
@ -789,11 +789,7 @@ The function executes one or two shell commands synchronously."
|
|||
((eq type 'ps)
|
||||
(shell-command convert2ps)))
|
||||
type)))
|
||||
;; (save-excursion
|
||||
;; (split-window-below)
|
||||
;; (other-window 1)
|
||||
;; (switch-to-buffer sanybuffer)
|
||||
;; (insert output))))
|
||||
|
||||
|
||||
(defun tla+-run-tlatex-pdf ()
|
||||
"Create PDF file from TLA+ Specification.
|
||||
|
|
@ -1050,15 +1046,17 @@ The procedure works by:
|
|||
:notify
|
||||
(lambda (&rest ignore)
|
||||
(let ((cfgtlc
|
||||
(replace-regexp-in-string ".*\\[\\(.*\\)\\].*"
|
||||
"\\1tlcopt"
|
||||
(buffer-name))))
|
||||
(replace-regexp-in-string
|
||||
".*\\[\\(.*\\)\\].*"
|
||||
"\\1tlcopt"
|
||||
(buffer-name))))
|
||||
(tla+/read-options cfgtlc)
|
||||
(let ((value
|
||||
(cdr
|
||||
(assoc 'tla+-tlc-deadlock
|
||||
tla+-option-list))))
|
||||
(if (or (equal nil value) (string= value " "))
|
||||
(if (or (equal nil value)
|
||||
(string= value " "))
|
||||
(tla+/add-option
|
||||
cfgtlc
|
||||
'tla+-tlc-deadlock
|
||||
|
|
@ -1076,15 +1074,17 @@ The procedure works by:
|
|||
:notify
|
||||
(lambda (&rest ignore)
|
||||
(let ((cfgtlc
|
||||
(replace-regexp-in-string ".*\\[\\(.*\\)\\].*"
|
||||
"\\1"
|
||||
(buffer-name))))
|
||||
(replace-regexp-in-string
|
||||
".*\\[\\(.*\\)\\].*"
|
||||
"\\1"
|
||||
(buffer-name))))
|
||||
(tla+/read-options cfgtlc)
|
||||
(let ((value
|
||||
(cdr
|
||||
(assoc 'tla+-tlc-simulate
|
||||
tla+-option-list))))
|
||||
(if (or (equal value nil) (string= value " "))
|
||||
(if (or (equal value nil)
|
||||
(string= value " "))
|
||||
(tla+/add-option
|
||||
cfgtlc
|
||||
'tla+-tlc-simulate
|
||||
|
|
@ -1105,9 +1105,10 @@ The procedure works by:
|
|||
:notify
|
||||
(lambda (widget &rest ignore)
|
||||
(let ((cfgtlc
|
||||
(replace-regexp-in-string ".*\\[\\(.*\\)\\].*"
|
||||
"\\1"
|
||||
(buffer-name))))
|
||||
(replace-regexp-in-string
|
||||
".*\\[\\(.*\\)\\].*"
|
||||
"\\1"
|
||||
(buffer-name))))
|
||||
(tla+/add-option cfgtlc
|
||||
'tla+-tlc-depth
|
||||
(format " -depth %s "
|
||||
|
|
@ -1127,9 +1128,10 @@ The procedure works by:
|
|||
:notify
|
||||
(lambda (widget &rest ignore)
|
||||
(let ((cfgtlc
|
||||
(replace-regexp-in-string ".*\\[\\(.*\\)\\].*"
|
||||
"\\1"
|
||||
(buffer-name))))
|
||||
(replace-regexp-in-string
|
||||
".*\\[\\(.*\\)\\].*"
|
||||
"\\1"
|
||||
(buffer-name))))
|
||||
(tla+/add-option cfgtlc
|
||||
'tla+-tlc-workers
|
||||
(format " -workers %s "
|
||||
|
|
@ -1146,15 +1148,16 @@ The procedure works by:
|
|||
:notify
|
||||
(lambda (&rest ignore)
|
||||
(let*
|
||||
((config-buffer
|
||||
(get-buffer-create
|
||||
(replace-regexp-in-string
|
||||
((confname
|
||||
(replace-regexp-in-string
|
||||
".tla$" ".cfg"
|
||||
(replace-regexp-in-string
|
||||
"\\*TLC Configuration\\* \\[\\(.*\\)\\]"
|
||||
"\\1"
|
||||
(buffer-name))
|
||||
)))
|
||||
))
|
||||
(config-buffer (get-buffer-create confname))
|
||||
(config-buffer-file-name (buffer-file-name config-buffer))
|
||||
(str-confname (widget-value widget-tlc-confname))
|
||||
(str-specname (widget-value widget-tlc-specname))
|
||||
(str-init (widget-value widget-tlc-init))
|
||||
|
|
@ -1164,13 +1167,21 @@ The procedure works by:
|
|||
(lst-const (widget-value widget-tlc-constant))
|
||||
(lst-constraint (widget-value widget-tlc-constraint)))
|
||||
(progn
|
||||
(if (and confname
|
||||
(file-exists-p confname))
|
||||
(rename-file confname
|
||||
(concat confname ".old."
|
||||
(number-to-string
|
||||
(nth 1 (current-time)))
|
||||
)))
|
||||
(switch-to-buffer config-buffer)
|
||||
(erase-buffer)
|
||||
(tla+-mode)
|
||||
(insert
|
||||
(format
|
||||
(concat "\\* -*- mode: tla+; -*-\n"
|
||||
"\\* TLA+ Config %s\n"
|
||||
"\\* XXX date/time\n"
|
||||
"\\* Created %s\n"
|
||||
"%s\n"
|
||||
"\\* properties\n"
|
||||
"%s\n"
|
||||
|
|
@ -1182,6 +1193,7 @@ The procedure works by:
|
|||
"%s\n"
|
||||
"\n")
|
||||
str-confname
|
||||
(current-time-string)
|
||||
(if (not (string= str-specname "")) ""
|
||||
(concat "INIT " str-init "\n"
|
||||
"NEXT " str-next "\n"))
|
||||
|
|
|
|||
|
|
@ -0,0 +1,43 @@
|
|||
* This is an Org file
|
||||
** TLA+ with Org
|
||||
This is an attempt to combine Org-Mode Babel with TLA+.
|
||||
|
||||
Keyboard Shortcuts:
|
||||
|
||||
| Keystroke | Description |
|
||||
|-----------+-------------------------|
|
||||
| c-c c-t c | SANY Syntactic Analyzer |
|
||||
| c-c c-t e | Export DVI |
|
||||
| c-c c-t o | Open DVI file |
|
||||
| c-c c-t m | run TLC model checker |
|
||||
| c-c c-t p | run PlusCal Translator |
|
||||
|
||||
** Modul1 with descriptions
|
||||
|
||||
uyam erat, sed diam voluptua. At *vero* eos et accusam et justo duo
|
||||
dolores et ea rebum. _Stet_ clita kasd gubergren, no sea takimata
|
||||
sanctus est Lorem ipsum dolor sit amet.
|
||||
|
||||
- Unordered List
|
||||
- a
|
||||
- b
|
||||
- Unordered
|
||||
|
||||
Use: ~org-babel-tangle~ to export the module above:
|
||||
|
||||
#+BEGIN_SRC tla+ :tangle TestModul.tla
|
||||
------------------- MODULE TestModul -----------------------
|
||||
EXTENDS Naturals
|
||||
VARIABLE hr
|
||||
------------------------------------------------------------
|
||||
Init == hr \in (1..12)
|
||||
Next == hr' = IF hr = 12 THEN
|
||||
1
|
||||
ELSE
|
||||
hr + 1
|
||||
------------------------------------------------------------
|
||||
Spec == Init /\ [][Next]_hr
|
||||
============================================================
|
||||
\* Modification History
|
||||
\* Created Mon Aug 3 03:46:40 2020 by Christian Barthel
|
||||
#+END_SRC
|
||||
Loading…
Reference in New Issue