bch
/
tlamode
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

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.
master
Christian Barthel 2020-07-19 10:05:13 +02:00
parent deba3792c9
commit b84b64612a
1 changed files with 294 additions and 166 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

460
lisp/tla+-mode.el
View File

@ -1,3 +1,4 @@
;; -*- lexical-binding: t -*-
;; Copyright (C) 2019-2020 Christian Barthel <bch@online.de>
;; 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 </path/to/tla+-mode.el>)
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 </path/to/tla2tools.jar>)
or with:
M-x customize-group <RET> 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 <variablename>
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
\\{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)