From 1522267517faab03f97f7c262fe3139516e5fccb Mon Sep 17 00:00:00 2001 From: Christian Barthel Date: Sat, 15 Feb 2020 20:02:07 +0100 Subject: [PATCH] work on TLC config dialogue this commit adds a small graphical interface to create models which can be executed by the TLC model checker. --- tla+-mode.el | 263 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 263 insertions(+) diff --git a/tla+-mode.el b/tla+-mode.el index c8aab99..dd6d030 100644 --- a/tla+-mode.el +++ b/tla+-mode.el @@ -46,6 +46,12 @@ ;;; Code: +(require 'seq) ; reduce (fold) function +(require 'widget) ; TLC Configuration dialogue +(eval-when-compile + (require 'wid-edit)) + + ;; ------------------------------------------------------------------- ;; Customization variables: @@ -79,6 +85,14 @@ :type 'file :group 'tla+) + +(defcustom tla+-tlatex-arguments + " -shade -number " + "Arguments which will be used when running `TLaTeX'" + :type 'string + :group 'tla+) + + ;; ------------------------------------------------------------------- (defvar tla+-mode-map @@ -355,6 +369,13 @@ :help "Run tlc2.TLC" "(Execute the TLC Model Checker)")) + + (bindings--define-key map [menu-bar tla+ tla+-conf-model] + '(menu-item "Create TLC Model" tlc-widget-start + :help + "Create a TLC Model" + "(Open the TLC Configuration dialogue)")) + (bindings--define-key map [menu-bar tla+ tla+-run-pluscal] '(menu-item "Run PlusCal Translator" tla+-run-pluscal @@ -607,6 +628,8 @@ The function executes one or two shell commands synchronously." " -cp " tla+-tlatools-path " tla2tex.TLA " + tla+-tlatex-arguments + " " filename))) (dvipath (replace-regexp-in-string ".tla$" ".dvi" filename)) @@ -740,4 +763,244 @@ The procedure works by: + + + +;; GUI +(defvar widget-tlc-confname) +(defvar widget-tlc-specname) +(defvar widget-tlc-init) +(defvar widget-tlc-next) +(defvar widget-tlc-props) +(defvar widget-tlc-inv) +(defvar widget-tlc-constant) +(defvar widget-tlc-constraint) + +(defun tlc-widget-start () + "foo" + (interactive) + (progn + ;(tlc-widget-example (buffer-name)) + (tlc-widget-example (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") + + (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-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 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 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 "\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 "\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) + (insert + (format + (concat "\\* 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") + 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") + (widget-insert "\n") + (use-local-map widget-keymap) + (widget-setup)) + + (provide 'tla+-mode)