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