93 lines
2.7 KiB
Bash
Executable file
93 lines
2.7 KiB
Bash
Executable file
#!/bin/bash
|
|
|
|
# Description: This script runs TLA2TEX on a TLA+ specificaiton file,
|
|
# generating a TEX file, then converts it to PDF format, and opens the resulting file.
|
|
# Usage: ./tlapdf <file.tla>
|
|
|
|
# Constants
|
|
TOOLS_JAR="$HOME/Downloads/tla2tools.jar"
|
|
TOOLS="java -XX:+UseParallelGC -cp $TOOLS_JAR"
|
|
TLA2TEX="tla2tex.TLA"
|
|
|
|
# Function to display usage information
|
|
usage() {
|
|
echo "Usage: $0 [--no-clean] <file.tla>"
|
|
exit 1
|
|
}
|
|
|
|
# Check for the --no-clean option.
|
|
NO_CLEAN=false
|
|
if [[ "$1" == "--no-clean" ]]; then
|
|
NO_CLEAN=true
|
|
shift # Remove the option from the arguments
|
|
fi
|
|
|
|
# Check if a file name is provided.
|
|
SPEC="$1"
|
|
if [[ -z "$SPEC" ]]; then
|
|
echo "Error: No file name provided."
|
|
usage
|
|
fi
|
|
|
|
# Check if the file name ends with .tla
|
|
if [[ "$SPEC" != *.tla ]]; then
|
|
echo "Error: File name must end with .tla"
|
|
usage
|
|
fi
|
|
|
|
# Check if the input file exists and is readable
|
|
if [ ! -f "$SPEC" ] || [ ! -r "$SPEC" ]; then
|
|
echo "Error: File '$SPEC' does not exist or is not readable."
|
|
usage
|
|
fi
|
|
|
|
# Define the path to the TLA+ tools JAR file
|
|
if [ ! -f "$TOOLS_JAR" ] || [ ! -r "$TOOLS_JAR" ]; then
|
|
echo "Error: TLA+ tools JAR file '$TOOLS_JAR' does not exist or is not readable."
|
|
exit 1
|
|
fi
|
|
|
|
# Extract the base name without the .tla extension
|
|
BASENAME="${SPEC%.tla}"
|
|
PDFOUT="${BASENAME}.pdf"
|
|
|
|
# Convert TLA+ to LaTeX. A4 format.
|
|
$TOOLS $TLA2TEX -shade -grayLevel .97 -textwidth 540 -textheight 770 "$BASENAME.tla" 2>&1 | \
|
|
grep -vE '(looking for file|TLATeX .* output written|tla2tex.TLA Version|Total execution time)'
|
|
EXIT_STATUS=$?
|
|
|
|
if [[ $EXIT_STATUS -gt 1 ]]; then # Status is 1 when output is empty, which is our default case.
|
|
echo "tla2tex failed for $BASENAME.tla."
|
|
exit 1
|
|
fi
|
|
|
|
# Adjust the generated LaTeX file to use A4 paper.
|
|
if [[ "$OSTYPE" =~ ^darwin ]]; then
|
|
# macOS: the "-i ''" and LF are for compatibility with macOS sed.
|
|
sed -i '' '/\\usepackage{color}/a\
|
|
\\usepackage[a4paper, margin=1cm]{geometry}' "${BASENAME}.tex"
|
|
else
|
|
# Linux: traditional sed.
|
|
sed -i '/\\usepackage{color}/a \\usepackage[a4paper, margin=1cm]{geometry}' "${BASENAME}.tex"
|
|
fi
|
|
|
|
# Convert LaTeX to PDF.
|
|
pdflatex --interaction=batchmode "${BASENAME}.tex" 2>&1 | \
|
|
grep -vE '(This is pdfTeX|restricted|extended)'
|
|
EXIT_STATUS=$?
|
|
|
|
if [[ $EXIT_STATUS -gt 1 ]]; then # Status is 1 when output is empty, which is our default case.
|
|
echo "Error: pdflatex failed for $BASENAME.tex"
|
|
exit 1
|
|
fi
|
|
|
|
# Clean up unless --no-clean was specified.
|
|
if [[ "$NO_CLEAN" == false ]]; then
|
|
echo "Cleaning up..."
|
|
rm -fr states ".log" "$BASENAME.tex" "$BASENAME.dvi" "$BASENAME.ps" "$BASENAME.aux" "$BASENAME.log"
|
|
fi
|
|
|
|
# Open the resulting file
|
|
open "$PDFOUT"
|
|
|
|
echo "Script completed successfully."
|