diff --git a/tla+-mode.el b/tla+-mode.el
index 866f051..4e7b2dd 100644
--- a/tla+-mode.el
+++ b/tla+-mode.el
@@ -58,7 +58,7 @@
   :group 'tla+)
 
 (defcustom tla+-tlatools-path
-  "/usr/home/bch/tmp/tlaplus/tlatools/dist/tla2tools.jar"
+  "/usr/home/bch/tmp/tlaplus/tlatools/dist/tla2tools_1.6.0.jar"
   "Path to the TLA+ `tlatools.jar' file"
   :type 'file
   :group 'tla+)
@@ -97,6 +97,7 @@
     (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)
 
     ;; Main TLA+ Menu:
     (bindings--define-key map [menu-bar tla+]
@@ -257,7 +258,7 @@
     ;; Operators
     (bindings--define-key menu-map [operator]
       (cons "Insert Operator.." operator-map))
-
+    (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
     ;; Action Operators
     (bindings--define-key operator-map [action-operator]
       (cons "Action Operator" action-operator-map))
@@ -344,6 +345,12 @@
     ;; Main Menu
     (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
 
+    (bindings--define-key map [menu-bar tla+ tla+-run-pluscal]
+      '(menu-item "Run PlusCal Translator" tla+-run-pluscal
+                  :help
+                  "Run pcal.trans"
+                  "(Translator from PlusCal algorithm language to TLA+)"))
+    
     (bindings--define-key map [menu-bar tla+ tla+-run-sany]
       '(menu-item "Run Syntax Checker" tla+-run-sany
                   :help
@@ -353,7 +360,7 @@
     (bindings--define-key map [menu-bar tla+ tla+-create-module]
       '(menu-item "Create new Module" tla+-create-module
                   :help "Create a new TLA+ Module"))
-    (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
+    ;(bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
     map)
   "Keymap for `tla+-mode'.")
 
@@ -412,6 +419,8 @@ The function executes the TLA+ Syntax checker and reports errors
 in a new frame.  Errors are clickable buttons and the user can 
 directly go to the error line.
 
+It is meant to be run from a TLA+ Specification buffer.
+
 Operation:
 1. execute the tla2sany.SANY program
 2. the output of the shell-command is inserted into a newly
@@ -435,6 +444,42 @@ Operation:
       (insert output)
       (tla+/find-error-marks))))
 
+(defun tla+-run-pluscal ()
+  "This function runs pcal.trans (PlusCal Translator to TLA+)
+This function executes the PlusCal Translator on the current
+buffer (Assumption: the buffer is a TLA+ buffer that contains 
+PlusCal code).  
+On success, the buffer will be reloaded and a message will be 
+printed.  On failure (i.e. the exit code of the shell command 
+was not 0), an error message will be printed.
+"
+  (interactive)
+  (let* ((filename (buffer-file-name))
+	 (oldfile (replace-regexp-in-string
+		   ".tla$" ".old" filename))
+	 (pcalbuf (get-buffer-create "*pcal.trans*"))
+	 (cmd (concat 
+	       tla+-java-path " -cp " tla+-tlatools-path
+	       " pcal.trans "filename ))
+	 (output (shell-command cmd)))
+    (if (= output 0)
+	(progn
+	  (revert-buffer nil t)
+	  (message (concat
+		    "Successfully Transalted"
+		    " - You can visit the old file at "
+		    oldfile)))
+      (progn
+	(split-window-below)
+	(other-window 1)
+	(switch-to-buffer pcalbuf)
+	(erase-buffer)
+	(insert
+	 (shell-command-to-string cmd))
+	(message "Translation Failed")))))
+      
+      
+
 (defun tla+-open-dvi (buffername)
   "Function to open a DVI file.
 This function starts the `xdvi' utility and opens the TLA+