From b84b64612a2ea868ac0c2492ffc9a80c473c08bc Mon Sep 17 00:00:00 2001 From: Christian Barthel Date: Sun, 19 Jul 2020 10:05:13 +0200 Subject: [PATCH] select and use tlc parameters - 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. --- lisp/tla+-mode.el | 460 +++++++++++++++++++++++++++++----------------- 1 file changed, 294 insertions(+), 166 deletions(-) diff --git a/lisp/tla+-mode.el b/lisp/tla+-mode.el index cac0c2e..a5c0c12 100644 --- a/lisp/tla+-mode.el +++ b/lisp/tla+-mode.el @@ -1,3 +1,4 @@ +;; -*- lexical-binding: t -*- ;; Copyright (C) 2019-2020 Christian Barthel ;; Author: Christian Barthel @@ -20,29 +21,11 @@ ;;; Commentary: -;; This package defines TLA+ Major Mode to manipulate TLA+ -;; specifications as invented by Leslie Lamport [1]. -;; -;; Features: -;; - Syntax Highlighting for TLA+ Specification Files -;; - Running `SANY Syntactic Analyzer' on TLA+ files -;; - Exporting TLA+ Specification files with TLATeX to -;; DVI, PS or PDF files -;; - Inserting TLA+ Operators with an easy to use menu -;; or typical Emacs keystrokes. -;; - Use templates to generate Modules -;; -;; Installation: -;; To use tla+-mode, you have to load the tla+-mode.el file -;; with -;; (load "/path/to/tla+-mode.el") -;; and use it with -;; (require tla+-mode) -;; -;; Getting, and Using the tlatoolbox: -;; https://tla.msr-inria.inria.fr/tlatoolbox/dist/ -;; https://lamport.azurewebsites.net/tla/tools.html -;; https://lamport.azurewebsites.net/tla/standalone-tools.html +;; This package defines TLA+ Major Mode to manipulate TLA+ specification +;; files. Use the `describe-mode' to see additional commentary on +;; its features, use and configuration. + + ;;; Code: @@ -63,13 +46,13 @@ :group 'tla+) (defcustom tla+-java-path "java" - "Path to the `java' program" + "Path to the `java' binary" :type 'file :group 'tla+) (defcustom tla+-tlatools-path "/usr/home/bch/tmp/tlaplus/tlatools/dist/tla2tools_1.6.0.jar" - "Path to the TLA+ `tlatools.jar' file" + "Path to the TLA+ `tlatools.jar' toolbox java archive" :type 'file :group 'tla+) @@ -100,7 +83,7 @@ (defcustom tla+-tlc-simulate " " - "Tell `TLC' to do simulation (randomly chosen behaviors) (-simulate)" + "Tell `TLC' to do simulation (-simulate)" :type 'string :group 'tla+) @@ -112,7 +95,7 @@ (defcustom tla+-tlc-coverage " " - "Tell `TLC' to print coverage every X minutes: -coverage X" + "Tell `TLC' to print coverage every X minutes" :type 'string :group 'tla+) @@ -123,6 +106,12 @@ :group 'tla+) +(defcustom tla+-option-list + '() + "Assoc list for TLC Options" + :type 'string) + + ;; ------------------------------------------------------------------- @@ -143,8 +132,8 @@ ) (set-keymap-parent map lisp-mode-shared-map) (define-key map "\e\t" 'ispell-complete-word) - (define-key map (kbd "C-c C-t e") 'tla+-run-tlatex-dvi) - (define-key map (kbd "C-c C-t o") 'tla+-open-dvi) + (define-key map (kbd "C-c C-t e") 'tla+-run-tlatex-dvi) + (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) @@ -412,7 +401,7 @@ '(menu-item "Run PlusCal Translator" tla+-run-pluscal :help "Run pcal.trans" - "(Translator from PlusCal algorithm language to TLA+)")) + "(Translator (PlusCal algorithm language -> TLA+)")) (bindings--define-key map [menu-bar tla+ tla+-run-sany] '(menu-item "Run Syntax Checker" tla+-run-sany @@ -448,10 +437,68 @@ ;;;###autoload (add-to-list 'auto-mode-alist '("\\.tla\\'" . tla+-mode)) ;;;###autoload (define-derived-mode tla+-mode fundamental-mode "TLA+" - "Major mode for editing TLA+ specifications. -In this mode, syntax highlighting is activated for TLA+ specification -files. Various operators can be inserted by `tla+-operator-NAME'. -\\{text-mode-map} + "Major mode for editing TLA+ specification files. + +This package defines TLA+ Major Mode to manipulate TLA+ +specifications as invented by Leslie Lamport [1]. + +In this mode, syntax highlighting is activated for TLA+ +specification files. Various operators can be inserted +by `tla+-operator-NAME'. + +Features: + - Syntax Highlighting for TLA+ Specification Files + - Running `SANY Syntactic Analyzer' on TLA+ files, + default keybinding: `C-c C-t c'. + - Exporting TLA+ Specification files with TLATeX to + DVI, PS or PDF files (Export it with `C-c C-t e' + and open the viewer `C-c C-t o') + - Inserting TLA+ Operators with an easy to use menu + or typical Emacs keystrokes. + - Use templates to generate Modules + - An Emacs widget to create TLC configuration files + - Options to run the TLC model checker on TLA+ + specifications (`C-c C-t m'). + - Translate PlusCal code to TLA+ specification + with `C-c C-t p'. + +Installation: + To use tla+-mode, you have to load the tla+-mode.el file + with + (load ) + and use it with + (require tla+-mode) + The TLA+ Toolbox can be downloaded at [1]. + +Configuration: + You must at least set the variable to the TLA2 Toolbox. This + can be done by setting the variable in the emacs configuration + file (i.e. ~/.emacs or ~/.emacs.d/init.el) + (setq tla+-tlatools-path ) + or with: + M-x customize-group tla+ + + You may also set the following paths: + tla+-java-path + tla+-dvipdf-path + tla+-dvips-path + tla+-tla+-tlatex-arguments + TLC options can be set globally or in the TLC configuration + GUI dialogue: + tla+-tlc-deadlock + tla+-tlc-simulate + tla+-tlc-depth + tla+-tlc-coverage + tla+-tlc-workers + To get help on one of the variables: + C-h v + M-x describe-variable + +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 +\\{tla+-mode-map} Turning on Text mode runs the normal hook `text-mode-hook'." (setq-local font-lock-defaults '(tla+-font-lock-keywords)) @@ -551,15 +598,29 @@ Note: The TLA+ specification file is a relative path. ;; 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 " - tla+-tlc-deadlock " " - tla+-tlc-simulate " " - tla+-tlc-depth " " + opt-deadlock " " + opt-simulate " " + opt-depth " " tla+-tlc-coverage " " - tla+-tlc-workers " " + opt-workers " " " -config " cfgfile " " finame)) (output (shell-command-to-string cmd))) @@ -572,7 +633,7 @@ Note: The TLA+ specification file is a relative path. (tla+/find-error-marks) (other-window 1) ;(message "marked") - ;(message (concat "cmd: " cmd)) + (message (concat "cmd: " cmd)) ))) @@ -821,9 +882,33 @@ 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)))) + (setq tla+-option-list (read data))) + (setq tla+-option-list '()))) +(defun tla+/write-options (filename) + (write-region + (prin1-to-string tla+-option-list) + nil filename)) +(defun tla+/add-option (filename key value) + (let ((newopt (list (cons key value)))) + (tla+/read-options filename) + (setq tla+-option-list + (assq-delete-all key tla+-option-list)) + (setq tla+-option-list + (append tla+-option-list newopt)) + (tla+/write-options filename))) +(defun tla+/get-option (key) + (cdr (assoc key tla+-option-list))) + +(defun tla+/coalesce (var1 var2) + (if var1 var1 var2)) ;; GUI (defvar widget-tlc-confname) @@ -836,145 +921,185 @@ The procedure works by: (defvar widget-tlc-constraint) (defun tlc-widget-start () - "foo" + "Start TLC Config GUI" (interactive) (progn - ;(tlc-widget-example (buffer-name)) (tlc-widget-example (buffer-name)) - (message "%s" (buffer-name)) - )) + (message "%s" (buffer-name)))) (defun tlc-widget-example (filename) "Create the widgets from the Widget manual." (interactive) - (switch-to-buffer (format "*TLC Configuration* [%s]" - (replace-regexp-in-string - ".tla$" ".cfg" filename))) - (kill-all-local-variables) - (make-local-variable 'widget-tlc-specname) - (make-local-variable 'widget-tlc-init) - (make-local-variable 'widget-tlc-next) - (make-local-variable 'widget-tlc-props) - (make-local-variable 'widget-tlc-inv) - (make-local-variable 'widget-tlc-constant) - (make-local-variable 'widget-tlc-constraint) - (setq widget-tlc-props '()) - (setq widget-tlc-inv '()) - (setq widget-tlc-constant '()) - (setq widget-tlc-constraint '()) - (let ((inhibit-read-only t)) - (erase-buffer)) - (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-insert "\n") + (let* ((cfgname (replace-regexp-in-string + ".tla$" ".cfg" filename)) + (cfgtlc (concat cfgname "tlcopt"))) + (switch-to-buffer (format "*TLC Configuration* [%s]" + cfgname)) + (kill-all-local-variables) + (make-local-variable 'widget-tlc-specname) + (make-local-variable 'widget-tlc-init) + (make-local-variable 'widget-tlc-next) + (make-local-variable 'widget-tlc-props) + (make-local-variable 'widget-tlc-inv) + (make-local-variable 'widget-tlc-constant) + (make-local-variable 'widget-tlc-constraint) + (setq widget-tlc-props '()) + (setq widget-tlc-inv '()) + (setq widget-tlc-constant '()) + (setq widget-tlc-constraint '()) + (let ((inhibit-read-only t)) + (erase-buffer)) + (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-insert "\n") - (setq widget-tlc-specname - (widget-create 'editable-field - :size 18 - :format "Specification Name: %v " "")) - (widget-insert "\n") + (setq widget-tlc-specname + (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-insert "\n") + (setq widget-tlc-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-insert "\n") + (setq widget-tlc-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-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-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-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-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-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-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-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 '() '(editable-field :value ""))) - ;; XXX it might be useful to set some further options? - ;; Those options, however, are not included within the - ;; *.cfg file but must be given to the commandline - ;; (while invoking the TLC program) + (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 + ) - ;; (widget-insert "\nOptions (Select multiple ones)\n\n") - ;; (widget-create 'checkbox t) - ;; (widget-insert " Do not check for Deadlocks\n") - ;; (widget-create 'checkbox nil) - ;; (widget-insert " Simulation Mode\n") - ;; - ;; (widget-insert " Depth (how many behaviors to test): ") - ;; (widget-create 'menu-choice - ;; :tag "Choose" - ;; :value "100" - ;; :help-echo "Choose -depth" - ;; :notify (lambda (widget &rest ignore) - ;; (message "%s is a good choice!" - ;; (widget-value widget))) - ;; '(item :tag "100" :value "100") - ;; '(choice-item "250" ) - ;; '(choice-item "300" ) - ;; '(choice-item "500" ) - ;; '(choice-item "1000" ) - ;; '(editable-field :menu-tag "No option" "100")) - ;; - ;; - ;; (widget-insert " Workers (may speed up execution)..: ") - ;; (widget-create 'menu-choice - ;; :tag "Choose" - ;; :value "1" - ;; :help-echo "Choose -depth" - ;; :notify (lambda (widget &rest ignore) - ;; (message "%s is a good choice!" - ;; (widget-value widget))) - ;; '(item :tag "1" :value "1") - ;; '(choice-item "2" ) - ;; '(choice-item "4" ) - ;; '(choice-item "8" ) - ;; '(choice-item "16" ) - ;; '(editable-field :menu-tag "No option" "100")) + (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) + + + (widget-insert "\nDepth (# behaviors): ") + (widget-create 'menu-choice + :tag "Choose" + :value "100" + :help-echo "Choose -depth" + :notify + (lambda (widget &rest ignore) + (tla+/add-option cfgtlc + 'tla+-tlc-depth + (format " -depth %s " + (widget-value widget)))) + '(item :tag "100" :value "100") + '(choice-item "250" ) + '(choice-item "300" ) + '(choice-item "500" ) + '(choice-item "1000" ) + '(editable-field :menu-tag "No option" "100")) + + (widget-insert "Threads............: ") + (widget-create 'menu-choice + :tag "Choose" + :value "1" + :help-echo "Choose -workers" + :notify + (lambda (widget &rest ignore) + (tla+/add-option cfgtlc + 'tla+-tlc-workers + (format " -workers %s " + (widget-value widget)))) + '(item :tag "1" :value "1") + '(choice-item "2" ) + '(choice-item "4" ) + '(choice-item "8" ) + '(choice-item "16" ) + '(editable-field :menu-tag "No option" "100")) (widget-insert "\n\n") (widget-create 'push-button @@ -1000,9 +1125,11 @@ The procedure works by: (lst-constraint (widget-value widget-tlc-constraint))) (progn (switch-to-buffer config-buffer) + (tla+-mode) (insert (format - (concat "\\* TLA+ Config %s\n" + (concat "\\* -*- mode: tla+; -*-\n" + "\\* TLA+ Config %s\n" "\\* XXX date/time\n" "%s\n" "\\* properties\n" @@ -1012,7 +1139,8 @@ The procedure works by: "\\* constants\n" "%s\n" "\\* constraints\n" - "%s\n") + "%s\n" + "\n") str-confname (if (not (string= str-specname "")) "" (concat "INIT " str-init "\n" @@ -1059,7 +1187,7 @@ The procedure works by: "Reset Form") (widget-insert "\n") (use-local-map widget-keymap) - (widget-setup)) + (widget-setup))) (provide 'tla+-mode)