work on TLC config dialogue
this commit adds a small graphical interface to create models which can be executed by the TLC model checker.
This commit is contained in:
parent
a29978acaf
commit
1522267517
263
tla+-mode.el
263
tla+-mode.el
|
@ -46,6 +46,12 @@
|
||||||
|
|
||||||
;;; Code:
|
;;; Code:
|
||||||
|
|
||||||
|
(require 'seq) ; reduce (fold) function
|
||||||
|
(require 'widget) ; TLC Configuration dialogue
|
||||||
|
(eval-when-compile
|
||||||
|
(require 'wid-edit))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
;; -------------------------------------------------------------------
|
;; -------------------------------------------------------------------
|
||||||
;; Customization variables:
|
;; Customization variables:
|
||||||
|
@ -79,6 +85,14 @@
|
||||||
:type 'file
|
:type 'file
|
||||||
:group 'tla+)
|
:group 'tla+)
|
||||||
|
|
||||||
|
|
||||||
|
(defcustom tla+-tlatex-arguments
|
||||||
|
" -shade -number "
|
||||||
|
"Arguments which will be used when running `TLaTeX'"
|
||||||
|
:type 'string
|
||||||
|
:group 'tla+)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
;; -------------------------------------------------------------------
|
;; -------------------------------------------------------------------
|
||||||
(defvar tla+-mode-map
|
(defvar tla+-mode-map
|
||||||
|
@ -355,6 +369,13 @@
|
||||||
:help
|
:help
|
||||||
"Run tlc2.TLC"
|
"Run tlc2.TLC"
|
||||||
"(Execute the TLC Model Checker)"))
|
"(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]
|
(bindings--define-key map [menu-bar tla+ tla+-run-pluscal]
|
||||||
'(menu-item "Run PlusCal Translator" 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 "
|
" -cp "
|
||||||
tla+-tlatools-path
|
tla+-tlatools-path
|
||||||
" tla2tex.TLA "
|
" tla2tex.TLA "
|
||||||
|
tla+-tlatex-arguments
|
||||||
|
" "
|
||||||
filename)))
|
filename)))
|
||||||
(dvipath (replace-regexp-in-string
|
(dvipath (replace-regexp-in-string
|
||||||
".tla$" ".dvi" filename))
|
".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)
|
(provide 'tla+-mode)
|
||||||
|
|
Loading…
Reference in New Issue