diff --git a/ChangeLog b/ChangeLog new file mode 100644 index 0000000..6a96db8 --- /dev/null +++ b/ChangeLog @@ -0,0 +1,22 @@ +2020-08-02 Christian Barthel + + * 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. + + diff --git a/lisp/tla+-mode.el b/lisp/tla+-mode.el index a5c0c12..6103816 100644 --- a/lisp/tla+-mode.el +++ b/lisp/tla+-mode.el @@ -29,8 +29,8 @@ ;;; Code: -(require 'seq) ; reduce (fold) function -(require 'widget) ; TLC Configuration dialogue +(require 'seq) ; reduce (fold) function +(require 'widget) ; TLC Configuration dialogue (eval-when-compile (require 'wid-edit)) @@ -88,7 +88,7 @@ :group 'tla+) (defcustom tla+-tlc-depth - " -depth 100 " + " -depth 1000 " "Tell `TLC' to do max. X steps (default: 100)" :type 'string :group 'tla+) @@ -100,7 +100,7 @@ :group 'tla+) (defcustom tla+-tlc-workers - " -workers 1 " + " -workers 2 " "Tell `TLC' how many threads to generate." :type 'string :group 'tla+) @@ -111,7 +111,15 @@ "Assoc list for TLC Options" :type 'string) +(defcustom tla+-dot-convert + "out.png" + "If non-nil, convert states.dot to the filename given by the string" + :type 'string) +(defcustom tla+-dot-binary + "dot" + "path to dot binary" + :type 'string) ;; ------------------------------------------------------------------- @@ -251,7 +259,7 @@ (insert "Seq(S)") (backward-char 2)) :help - "Set of all Sequences of Elements of Set `S'")) + "Set of all Sequences of Elements of Set `S'")) (bindings--define-key modul-sequences-operators [head-s] @@ -513,7 +521,7 @@ A new module will be created with the typical structure of a TLA+ specification file." (interactive) (let ((modulename - (concat (file-name-base (buffer-file-name))))) + (concat (file-name-base (buffer-file-name))))) (insert (concat "------------------- MODULE " @@ -533,7 +541,7 @@ specification file." (let ((text "...describe changes here...")) (goto-char (point-max)) (insert (concat "\\* Updated " (current-time-string) " by " - user-full-name "\n")) + user-full-name "\n")) (insert (concat "\\* " text)) (goto-char (- (point-max) (length text))))) @@ -556,8 +564,8 @@ Operation: (interactive) (let* ((filename (buffer-file-name)) (sanybuffer - (get-buffer-create - (format "*tla2sany.SANY* [%s]" (buffer-name)))) + (get-buffer-create + (format "*tla2sany.SANY* [%s]" (buffer-name)))) (output (shell-command-to-string (concat tla+-java-path " -cp " @@ -573,6 +581,12 @@ Operation: (tla+/find-error-marks) (other-window 1)))) +(defun tla+-run-dot () + (let ((cmd (format "%s -Tpng states.dot > %s" + tla+-dot-binary + tla+-dot-convert))) + (shell-command-to-string cmd))) + (defun tla+-run-model (cfgfile) "Run the tlc2.TLC Model checker Run the tlc2.TLC model checker on a TLA+ buffer with a given @@ -585,57 +599,68 @@ Note: The TLA+ specification file is a relative path. " (interactive (list (read-file-name - "Filename (or enter to use current buffer): " - (file-name-directory (buffer-file-name)) - nil nil - (concat - (file-name-base (buffer-file-name)) - ".cfg" )))) + "Filename (or enter to use current buffer): " + (file-name-directory (buffer-file-name)) + nil nil + (concat + (file-name-base (buffer-file-name)) + ".cfg" )))) (let* ((filename (buffer-file-name)) - (tlcbuffer (get-buffer-create - (format "*tlc2.TLC* [%s]" (buffer-name)))) - ;; 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")) - (tlcconf (concat finame "tlcopt")) - (loadconf (tla+/read-options tlcconf)) - (opt-deadlock (tla+/coalesce - (tla+/get-option 'tla+-tlc-deadlock) - tla+-tlc-deadlock)) - (opt-simulate (tla+/coalesce - (tla+/get-option 'tla+-tlc-simulate) - tla+-tlc-simulate)) - (opt-depth (tla+/coalesce - (tla+/get-option 'tla+-tlc-depth) - tla+-tlc-depth)) - (opt-workers (tla+/coalesce - (tla+/get-option 'tla+-tlc-workers) - tla+-tlc-workers)) - (cmd (concat - tla+-java-path " -cp " tla+-tlatools-path - " tlc2.TLC " - " -dump dot states.dot " - opt-deadlock " " - opt-simulate " " - opt-depth " " - tla+-tlc-coverage " " - opt-workers " " - " -config " cfgfile " " - finame)) - (output (shell-command-to-string cmd))) + (tlcbufname (format "*tlc2.TLC* [%s]" (buffer-name))) + ;(tlcbuffer (get-buffer-create + ; (format "*tlc2.TLC* [%s]" (buffer-name)))) + (tlcbuffer (get-buffer tlcbufname)) + (cubuffer (current-buffer)) + ;; 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")) + (tlcconf (concat finame "tlcopt")) + (loadconf (tla+/read-options tlcconf)) + (opt-deadlock (tla+/coalesce + (tla+/get-option 'tla+-tlc-deadlock) + tla+-tlc-deadlock)) + (opt-simulate (tla+/coalesce + (tla+/get-option 'tla+-tlc-simulate) + tla+-tlc-simulate)) + (opt-depth (tla+/coalesce + (tla+/get-option 'tla+-tlc-depth) + tla+-tlc-depth)) + (opt-workers (tla+/coalesce + (tla+/get-option 'tla+-tlc-workers) + tla+-tlc-workers)) + (cmd (concat + tla+-java-path " -cp " tla+-tlatools-path + " tlc2.TLC " + " -dump dot states.dot " + opt-deadlock " " + opt-simulate " " + opt-depth " " + tla+-tlc-coverage " " + opt-workers " " + " -config " cfgfile " " + finame)) + (output (shell-command-to-string cmd)) + (dot (tla+-run-dot))) (save-excursion - (split-window-below) - (other-window 1) - (switch-to-buffer tlcbuffer) - (erase-buffer) - (insert output) - (tla+/find-error-marks) - (other-window 1) - ;(message "marked") - (message (concat "cmd: " cmd)) - ))) - + (if tlcbuffer + (progn + (switch-to-buffer tlcbuffer) + (setq buffer-read-only nil) + (erase-buffer) + (insert output) + (tla+/find-error-marks) + (setq buffer-read-only 't) + (switch-to-buffer cubuffer)) + (progn + (let ((newbuf (get-buffer-create tlcbufname))) + (split-window-below) + (other-window 1) + (switch-to-buffer newbuf) + (insert output) + (tla+/find-error-marks) + (setq buffer-read-only 't) + (other-window 1))))))) (defun tla+-run-pluscal () @@ -649,29 +674,29 @@ was not 0), an error message will be printed. " (interactive) (let* ((filename (buffer-file-name)) - (oldfile (replace-regexp-in-string - ".tla$" ".old" filename)) - (pcalbuf (get-buffer-create - (format "*pcal.trans* [%s]" (buffer-name)))) - (cmd (concat - tla+-java-path " -cp " tla+-tlatools-path - " pcal.trans "filename )) - (output (shell-command cmd))) + (oldfile (replace-regexp-in-string + ".tla$" ".old" filename)) + (pcalbuf (get-buffer-create + (format "*pcal.trans* [%s]" (buffer-name)))) + (cmd (concat + tla+-java-path " -cp " tla+-tlatools-path + " pcal.trans "filename )) + (output (shell-command cmd))) (if (= output 0) - (progn - (revert-buffer nil t) - (message (concat - "Successfully Transalted" - " - You can visit the old file at " - oldfile))) + (progn + (revert-buffer nil t) + (message (concat + "Successfully Transalted" + " - You can visit the old file at " + oldfile))) (progn - (split-window-below) - (other-window 1) - (switch-to-buffer pcalbuf) - (erase-buffer) - (insert - (shell-command-to-string cmd)) - (message "Translation Failed"))))) + (split-window-below) + (other-window 1) + (switch-to-buffer pcalbuf) + (erase-buffer) + (insert + (shell-command-to-string cmd)) + (message "Translation Failed"))))) @@ -748,8 +773,8 @@ The function executes one or two shell commands synchronously." " -cp " tla+-tlatools-path " tla2tex.TLA " - tla+-tlatex-arguments - " " + tla+-tlatex-arguments + " " filename))) (dvipath (replace-regexp-in-string ".tla$" ".dvi" filename)) @@ -816,11 +841,11 @@ Steps done by this function: 5. goto line and column. " (let* ((pos (point)) - (buffername - (replace-regexp-in-string - "\\*.*\\* \\[\\(.*\\)\\]" - "\\1" - (buffer-name))) + (buffername + (replace-regexp-in-string + "\\*.*\\* \\[\\(.*\\)\\]" + "\\1" + (buffer-name))) (the-button (button-at pos)) (text (button-label the-button)) (s (string-match @@ -866,18 +891,18 @@ The procedure works by: (progn (goto-char (point-min)) (while (re-search-forward - (concat - "line \\([0-9][0-9]*\\), " - "\\(column\\|col\\) " - "\\([0-9][0-9]*\\)") + (concat + "line \\([0-9][0-9]*\\), " + "\\(column\\|col\\) " + "\\([0-9][0-9]*\\)") (point-max) t) (let* ((rstart (match-beginning 0)) (linenum (match-beginning 1)) (colnum (match-beginning 3)) (rend (+ colnum (- (length (int-to-string colnum)) 0))) ) - (message "%s %s" linenum colnum) - ;(message "%d %d" rstart rend) + (message "%s %s" linenum colnum) + ;(message "%d %d" rstart rend) (tla+/make-link-button rstart rend) )))) @@ -885,8 +910,8 @@ The procedure works by: (defun tla+/read-options (filename) (if (file-exists-p filename) (let ((data (with-temp-buffer - (insert-file-contents filename) - (buffer-string)))) + (insert-file-contents filename) + (buffer-string)))) (setq tla+-option-list (read data))) (setq tla+-option-list '()))) @@ -899,9 +924,9 @@ The procedure works by: (let ((newopt (list (cons key value)))) (tla+/read-options filename) (setq tla+-option-list - (assq-delete-all key tla+-option-list)) + (assq-delete-all key tla+-option-list)) (setq tla+-option-list - (append tla+-option-list newopt)) + (append tla+-option-list newopt)) (tla+/write-options filename))) (defun tla+/get-option (key) @@ -930,11 +955,10 @@ The procedure works by: (defun tlc-widget-example (filename) "Create the widgets from the Widget manual." (interactive) - (let* ((cfgname (replace-regexp-in-string - ".tla$" ".cfg" filename)) - (cfgtlc (concat cfgname "tlcopt"))) + (let ((cfgname (replace-regexp-in-string + ".tla$" ".cfg" filename))) (switch-to-buffer (format "*TLC Configuration* [%s]" - cfgname)) + cfgname)) (kill-all-local-variables) (make-local-variable 'widget-tlc-specname) (make-local-variable 'widget-tlc-init) @@ -952,117 +976,125 @@ The procedure works by: (remove-overlays) (widget-insert "TLC Configuration Dialogue\n\n") (setq widget-tlc-confname - (widget-create 'editable-field - :size 18 - :format "Config Name.......: %v " - (replace-regexp-in-string - ".tla$" ".cfg" filename) - filename)) + (widget-create 'editable-field + :size 18 + :format "Config Name.......: %v " + (replace-regexp-in-string + ".tla$" ".cfg" filename) + filename)) (widget-insert "\n") (setq widget-tlc-specname - (widget-create 'editable-field - :size 18 - :format "Specification Name: %v " "")) + (widget-create 'editable-field + :size 18 + :format "Specification Name: %v " "")) (widget-insert "\n") (setq widget-tlc-init - (widget-create 'editable-field - :size 18 - :format "Init..............: %v " "Init")) + (widget-create 'editable-field + :size 18 + :format "Init..............: %v " "Init")) (widget-insert "\n") (setq widget-tlc-next - (widget-create 'editable-field - :size 18 - :format "Next..............: %v " "Next")) + (widget-create 'editable-field + :size 18 + :format "Next..............: %v " "Next")) (widget-insert "\n") (widget-insert "\nList of properties (PROPERTY): \n") (setq widget-tlc-props - (widget-create 'editable-list - :entry-format "%i %d %v" - :notify - (lambda (widget &rest ign) - (setq widget-tlc-props widget)) - :value '() - '(editable-field :value ""))) + (widget-create 'editable-list + :entry-format "%i %d %v" + :notify + (lambda (widget &rest ign) + (setq widget-tlc-props widget)) + :value '() + '(editable-field :value ""))) (widget-insert "\nList of invariants (INVARIANT): \n") (setq widget-tlc-inv - (widget-create 'editable-list - :entry-format "%i %d %v" - :notify - (lambda (widget &rest ign) - (setq widget-tlc-inv widget)) - :value '() - '(editable-field :value "Spec => TypeInv"))) + (widget-create 'editable-list + :entry-format "%i %d %v" + :notify + (lambda (widget &rest ign) + (setq widget-tlc-inv widget)) + :value '() + '(editable-field :value "Spec => TypeInv"))) (widget-insert "\nList of Constants (CONSTANTS): \n") (setq widget-tlc-constant - (widget-create 'editable-list - :entry-format "%i %d %v" - :notify - (lambda (widget &rest ign) - (setq widget-tlc-constant widget)) - :value '() - '(editable-field :value ""))) + (widget-create 'editable-list + :entry-format "%i %d %v" + :notify + (lambda (widget &rest ign) + (setq widget-tlc-constant widget)) + :value '() + '(editable-field :value ""))) (widget-insert "\nList of constraints (CONSTRAINT): \n") (setq widget-tlc-constraint - (widget-create 'editable-list - :entry-format "%i %d %v" - :notify - (lambda (widget &rest ign) - (setq widget-tlc-constraint widget)) - :value '() + (widget-create 'editable-list + :entry-format "%i %d %v" + :notify + (lambda (widget &rest ign) + (setq widget-tlc-constraint widget)) + :value '() '(editable-field :value ""))) (widget-insert "--------------------------------------") (widget-insert "\nTLC Options\n\n") (widget-insert "No Deadlocks.......: " ) (widget-create 'checkbox - :notify - (lambda (&rest ignore) - (tla+/read-options cfgtlc) - (let ((value - (cdr - (assoc 'tla+-tlc-deadlock - tla+-option-list)))) - (if (or (equal nil value) (string= value " ")) - (tla+/add-option - cfgtlc - 'tla+-tlc-deadlock - " -deadlock ") - (tla+/add-option - cfgtlc - 'tla+-tlc-deadlock - " ") - ))) - nil - ) + :notify + (lambda (&rest ignore) + (let ((cfgtlc + (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 " ")) + (tla+/add-option + cfgtlc + 'tla+-tlc-deadlock + " -deadlock ") + (tla+/add-option + cfgtlc + 'tla+-tlc-deadlock + " ") + )))) + nil + ) (widget-insert "\nSimulation Mode....: ") (widget-create 'checkbox - :notify - (lambda (&rest ignore) - (tla+/read-options cfgtlc) - (let ((value - (cdr - (assoc 'tla+-tlc-simulate - tla+-option-list)))) - (if (or (equal value nil) (string= value " ")) - (tla+/add-option - cfgtlc - 'tla+-tlc-simulate - " -simulate ") - (tla+/add-option - cfgtlc - 'tla+-tlc-simulate - " ") - ))) - nil) + :notify + (lambda (&rest ignore) + (let ((cfgtlc + (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 " ")) + (tla+/add-option + cfgtlc + 'tla+-tlc-simulate + " -simulate ") + (tla+/add-option + cfgtlc + 'tla+-tlc-simulate + " ") + )))) + nil) (widget-insert "\nDepth (# behaviors): ") @@ -1071,11 +1103,15 @@ The procedure works by: :value "100" :help-echo "Choose -depth" :notify - (lambda (widget &rest ignore) - (tla+/add-option cfgtlc - 'tla+-tlc-depth - (format " -depth %s " - (widget-value widget)))) + (lambda (widget &rest ignore) + (let ((cfgtlc + (replace-regexp-in-string ".*\\[\\(.*\\)\\].*" + "\\1" + (buffer-name)))) + (tla+/add-option cfgtlc + 'tla+-tlc-depth + (format " -depth %s " + (widget-value widget))))) '(item :tag "100" :value "100") '(choice-item "250" ) '(choice-item "300" ) @@ -1089,11 +1125,15 @@ The procedure works by: :value "1" :help-echo "Choose -workers" :notify - (lambda (widget &rest ignore) - (tla+/add-option cfgtlc - 'tla+-tlc-workers - (format " -workers %s " - (widget-value widget)))) + (lambda (widget &rest ignore) + (let ((cfgtlc + (replace-regexp-in-string ".*\\[\\(.*\\)\\].*" + "\\1" + (buffer-name)))) + (tla+/add-option cfgtlc + 'tla+-tlc-workers + (format " -workers %s " + (widget-value widget))))) '(item :tag "1" :value "1") '(choice-item "2" ) '(choice-item "4" ) @@ -1103,88 +1143,88 @@ The procedure works by: (widget-insert "\n\n") (widget-create 'push-button - :notify - (lambda (&rest ignore) - (let* - ((config-buffer - (get-buffer-create - (replace-regexp-in-string - ".tla$" ".cfg" - (replace-regexp-in-string - "\\*TLC Configuration\\* \\[\\(.*\\)\\]" - "\\1" - (buffer-name)) - ))) - (str-confname (widget-value widget-tlc-confname)) - (str-specname (widget-value widget-tlc-specname)) - (str-init (widget-value widget-tlc-init)) - (str-next (widget-value widget-tlc-next)) - (lst-props (widget-value widget-tlc-props)) - (lst-inv (widget-value widget-tlc-inv)) - (lst-const (widget-value widget-tlc-constant)) - (lst-constraint (widget-value widget-tlc-constraint))) - (progn - (switch-to-buffer config-buffer) - (tla+-mode) - (insert - (format - (concat "\\* -*- mode: tla+; -*-\n" - "\\* TLA+ Config %s\n" - "\\* XXX date/time\n" - "%s\n" - "\\* properties\n" - "%s\n" - "\\* invariants\n" - "%s\n" - "\\* constants\n" - "%s\n" - "\\* constraints\n" - "%s\n" - "\n") - str-confname - (if (not (string= str-specname "")) "" - (concat "INIT " str-init "\n" - "NEXT " str-next "\n")) - (if (not (equal lst-props '())) - (seq-reduce - 'concat - (mapcar - (lambda (s) (concat "PROPERTY " s)) - (mapcar (lambda (s) (concat s "\n")) - lst-props)) "") "") - (if (not (equal lst-inv '())) - (seq-reduce - 'concat - (mapcar - (lambda (s) (concat "INVARIANT " s)) - (mapcar (lambda (s) (concat s "\n")) - lst-inv)) "") "") - (if (not (equal lst-const '())) - (seq-reduce - 'concat - (mapcar - (lambda (s) (concat "CONSTANT " s)) - (mapcar (lambda (s) (concat s "\n")) - lst-const)) "") "") - (if (not (equal lst-constraint '())) - (seq-reduce - 'concat - (mapcar - (lambda (s) (concat "CONSTRAINT " s)) - (mapcar (lambda (s) (concat s "\n")) - lst-constraint)) "") "")))))) - "Get Configuration") + :notify + (lambda (&rest ignore) + (let* + ((config-buffer + (get-buffer-create + (replace-regexp-in-string + ".tla$" ".cfg" + (replace-regexp-in-string + "\\*TLC Configuration\\* \\[\\(.*\\)\\]" + "\\1" + (buffer-name)) + ))) + (str-confname (widget-value widget-tlc-confname)) + (str-specname (widget-value widget-tlc-specname)) + (str-init (widget-value widget-tlc-init)) + (str-next (widget-value widget-tlc-next)) + (lst-props (widget-value widget-tlc-props)) + (lst-inv (widget-value widget-tlc-inv)) + (lst-const (widget-value widget-tlc-constant)) + (lst-constraint (widget-value widget-tlc-constraint))) + (progn + (switch-to-buffer config-buffer) + (tla+-mode) + (insert + (format + (concat "\\* -*- mode: tla+; -*-\n" + "\\* TLA+ Config %s\n" + "\\* XXX date/time\n" + "%s\n" + "\\* properties\n" + "%s\n" + "\\* invariants\n" + "%s\n" + "\\* constants\n" + "%s\n" + "\\* constraints\n" + "%s\n" + "\n") + str-confname + (if (not (string= str-specname "")) "" + (concat "INIT " str-init "\n" + "NEXT " str-next "\n")) + (if (not (equal lst-props '())) + (seq-reduce + 'concat + (mapcar + (lambda (s) (concat "PROPERTY " s)) + (mapcar (lambda (s) (concat s "\n")) + lst-props)) "") "") + (if (not (equal lst-inv '())) + (seq-reduce + 'concat + (mapcar + (lambda (s) (concat "INVARIANT " s)) + (mapcar (lambda (s) (concat s "\n")) + lst-inv)) "") "") + (if (not (equal lst-const '())) + (seq-reduce + 'concat + (mapcar + (lambda (s) (concat "CONSTANT " s)) + (mapcar (lambda (s) (concat s "\n")) + lst-const)) "") "") + (if (not (equal lst-constraint '())) + (seq-reduce + 'concat + (mapcar + (lambda (s) (concat "CONSTRAINT " s)) + (mapcar (lambda (s) (concat s "\n")) + lst-constraint)) "") "")))))) + "Get Configuration") (widget-insert " ") (widget-create 'push-button - :notify - (lambda (&rest ignore) - (tlc-widget-example - (replace-regexp-in-string - "\\*TLC Configuration\\* \\[\\(.*\\)\\]" - "\\1" - (buffer-name))) - ) - "Reset Form") + :notify + (lambda (&rest ignore) + (tlc-widget-example + (replace-regexp-in-string + "\\*TLC Configuration\\* \\[\\(.*\\)\\]" + "\\1" + (buffer-name))) + ) + "Reset Form") (widget-insert "\n") (use-local-map widget-keymap) (widget-setup)))