Change check.sh to use the TLA+ tools wrapper scripts

Also update README to point at the tla-bit project.

Signed-off-by: Catalin Marinas <catalin.marinas@arm.com>

2 files changed, 13 insertions, 20 deletions

diff --git a/README b/README
index f95fc22..36c4ec0 100644
--- a/README
+++ b/README
@@ -1,19 +1,18 @@
 This repository contains formal TLA+ specs of different algorithms used
-in the Linux kernel. So far it only contains asidalloc.tla (see below).
+in the Linux kernel.
 
-The TLA+ Tools need to be installed (together with a Java runtime):
+The recommended way to enable the checking of these specs is to use the
+TLA+ wrapper scripts:
 
-  https://lamport.azurewebsites.net/tla/tools.html (pre-built)
+  $ git clone https://github.com/pmer/tla-bin.git
+  $ ./download_or_update_tla.sh
+  $ ./install.sh $PREFIX
 
-or:
+The TLA+ Tools can also be downloaded directly from:
 
-  https://github.com/tlaplus/tlaplus/tree/master/tlatools (source)
-
-The graphical TLA Toolbox is not required.
-
-CLASSPATH in check.sh needs to point to the TLA+ Tools installation
-directory.
+  https://lamport.azurewebsites.net/tla/tools.html
 
+A Java runtime is required.
 
 asidalloc.tla
 -------------
diff --git a/check.sh b/check.sh
index 917b516..920705c 100755
--- a/check.sh
+++ b/check.sh
@@ -1,17 +1,11 @@
 #!/bin/bash
 
+# Download and install the TLA+ Tools wrapper scripts from
+# https://github.com/pmer/tla-bin.git
+
 set -e
 shopt -s expand_aliases
 
-export CLASSPATH=~/tla
-# Uncomment if TLC causes an exception in javax.activation.DataSource
-#export _JAVA_OPTIONS="--add-modules=java.activation"
-
-alias tlc="java tlc2.TLC"
-alias tla2sany="java tla2sany.SANY"
-alias pcal="java pcal.trans"
-alias tla2tex="java tla2tex.TLA"
-
 SPEC=$1
 shift
 
@@ -21,7 +15,7 @@ if grep -q -e "^\s*ProcessEnabled(self)\s*==" $SPEC.tla; then
 	sed -i -e 's%pc\[self\] = ".*"$%& /\\\ ProcessEnabled(self)%' $SPEC.tla
 fi
 
-# Generate{global,local}_vars
+# Split vars into {global,local}_vars tuples
 gawk -i inplace -f varsplit.awk $SPEC.tla
 
 tlc -workers $(nproc) $@ $SPEC.tla | tee -a $SPEC.log