From 30d6a1b7ee95a0a2ba62f60c3fb26ba58fe8498b Mon Sep 17 00:00:00 2001
From: Christian Barthel <bch@online.de>
Date: Sun, 5 Jan 2020 14:11:19 +0100
Subject: [PATCH] add model checker run function

add a new function to run the tla+ model
checker on a model.
---
 tla+-mode.el | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/tla+-mode.el b/tla+-mode.el
index 4e7b2dd..49fb78c 100644
--- a/tla+-mode.el
+++ b/tla+-mode.el
@@ -98,6 +98,7 @@
     (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)    
 
     ;; Main TLA+ Menu:
     (bindings--define-key map [menu-bar tla+]
@@ -345,6 +346,12 @@
     ;; Main Menu
     (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
 
+    (bindings--define-key map [menu-bar tla+ tla+-run-model]
+      '(menu-item "Run TLC Model Checker" tla+-run-model
+                  :help
+                  "Run tlc2.TLC"
+                  "(Execute the TLC Model Checker)"))
+    
     (bindings--define-key map [menu-bar tla+ tla+-run-pluscal]
       '(menu-item "Run PlusCal Translator" tla+-run-pluscal
                   :help
@@ -444,6 +451,47 @@ Operation:
       (insert output)
       (tla+/find-error-marks))))
 
+(defun tla+-run-model (cfgfile)
+  "Run the tlc2.TLC Model checker
+Run the tlc2.TLC model checker on a TLA+ buffer with a given
+moden CFGFILE.  The function constructs an absolute path to
+a model file spec.cfg and uses the current buffer as TLA+ 
+specification.  It then executes the tlc2.TLC model checker
+with the given model. 
+
+Note: The TLA+ specification file is a relative path.
+"
+  (interactive
+     (list (read-file-name
+	    "Filename (or enter to use current buffer): "
+	    (file-name-directory (buffer-file-name))
+	    nil nil
+	    (concat
+	     (file-name-base (buffer-file-name))
+	     ".cfg" ))))
+  (let* ((filename (buffer-file-name))
+	 (tlcbuffer (get-buffer-create "*tlc2.TLC*"))
+	 ;; XXX: tlc2.TLC -config /full/path/to/TLA.cfg TLA.tla
+	 ;;  not sure why the tla file itself should not be a
+	 ;;  full path?
+	 (finame (concat (file-name-base (buffer-file-name)) ".tla"))
+	 (cmd (concat
+	       tla+-java-path " -cp " tla+-tlatools-path
+	       " tlc2.TLC "
+	       " -config " cfgfile " "
+	       finame))
+	 (output (shell-command-to-string cmd)))
+    (save-excursion
+      (split-window-below)
+      (other-window 1)
+      (switch-to-buffer tlcbuffer)
+      (erase-buffer)
+      (insert output)
+      (message  (concat "cmd: " cmd))
+      )))
+
+
+  
 (defun tla+-run-pluscal ()
   "This function runs pcal.trans (PlusCal Translator to TLA+)
 This function executes the PlusCal Translator on the current