add model checker run function

add a new function to run the tla+ model
checker on a model.
Christian Barthel 2020-01-05 14:11:19 +01:00
parent 1a13c39218
commit 30d6a1b7ee
1 changed files with 48 additions and 0 deletions

View File

@ -98,6 +98,7 @@
(define-key map (kbd "C-c C-t o") 'tla+-open-dvi)
(define-key map (kbd "C-c C-t c") 'tla+-run-sany)
(define-key map (kbd "C-c C-t p") 'tla+-run-pluscal)
(define-key map (kbd "C-c C-t m") 'tla+-run-model)
;; Main TLA+ Menu:
(bindings--define-key map [menu-bar tla+]
@ -345,6 +346,12 @@
;; Main Menu
(bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
(bindings--define-key map [menu-bar tla+ tla+-run-model]
'(menu-item "Run TLC Model Checker" tla+-run-model
"Run tlc2.TLC"
"(Execute the TLC Model Checker)"))
(bindings--define-key map [menu-bar tla+ tla+-run-pluscal]
'(menu-item "Run PlusCal Translator" tla+-run-pluscal
@ -444,6 +451,47 @@ Operation:
(insert output)
(defun tla+-run-model (cfgfile)
"Run the tlc2.TLC Model checker
Run the tlc2.TLC model checker on a TLA+ buffer with a given
moden CFGFILE. The function constructs an absolute path to
a model file spec.cfg and uses the current buffer as TLA+
specification. It then executes the tlc2.TLC model checker
with the given model.
Note: The TLA+ specification file is a relative path.
(list (read-file-name
"Filename (or enter to use current buffer): "
(file-name-directory (buffer-file-name))
nil nil
(file-name-base (buffer-file-name))
".cfg" ))))
(let* ((filename (buffer-file-name))
(tlcbuffer (get-buffer-create "*tlc2.TLC*"))
;; XXX: tlc2.TLC -config /full/path/to/TLA.cfg TLA.tla
;; not sure why the tla file itself should not be a
;; full path?
(finame (concat (file-name-base (buffer-file-name)) ".tla"))
(cmd (concat
tla+-java-path " -cp " tla+-tlatools-path
" tlc2.TLC "
" -config " cfgfile " "
(output (shell-command-to-string cmd)))
(other-window 1)
(switch-to-buffer tlcbuffer)
(insert output)
(message (concat "cmd: " cmd))
(defun tla+-run-pluscal ()
"This function runs pcal.trans (PlusCal Translator to TLA+)
This function executes the PlusCal Translator on the current