82 lines
2.1 KiB
Bash
Executable file
82 lines
2.1 KiB
Bash
Executable file
#!/bin/bash
|
|
|
|
# Description: This script runs TLC2 on a TLA+ specification file,
|
|
# generating a DOT file, then converts it to SVG format, and opens the resulting file.
|
|
# Usage: ./tlcdump <file.tla>
|
|
|
|
# Constants
|
|
TOOLS_JAR="$HOME/Downloads/tla2tools.jar"
|
|
TOOLS="java -XX:+UseParallelGC -cp $TOOLS_JAR"
|
|
TLC=tlc2.TLC
|
|
|
|
# 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}"
|
|
MAINOUT="${BASENAME}.dot"
|
|
LIVEOUT="${BASENAME}_liveness.dot"
|
|
SVGOUT="${BASENAME}.svg"
|
|
SVGLIVE="${BASENAME}_liveness".svg
|
|
|
|
# Run TLC2 with the -dump dot option
|
|
echo "Running TLC2 on '$SPEC'..."
|
|
$TOOLS $TLC -dump dot,colorize,actionlabels "$BASENAME" "$SPEC"
|
|
EXIT_STATUS=$?
|
|
|
|
# Check if TLC2 succeeded or failed
|
|
if [ $EXIT_STATUS -ne 0 ]; then
|
|
echo "TLC2 encountered an error for $BASENAME.tla. Proceeding with DOT file generation..."
|
|
fi
|
|
|
|
# Convert the DOT file to SVG format
|
|
echo "Converting DOT file to SVG format..."
|
|
dot -Tsvg "$MAINOUT" -o "$SVGOUT"
|
|
dot -Tsvg "$LIVEOUT" -o "$SVGLIVE"
|
|
|
|
# Clean up unless --no-clean was specified.
|
|
if [[ "$NO_CLEAN" == false ]]; then
|
|
echo "Cleaning up..."
|
|
rm -f "$MAINOUT" "$LIVEOUT"
|
|
fi
|
|
|
|
# Open the resulting file
|
|
echo "Opening '$SVGOUT'..."
|
|
open "$SVGOUT"
|
|
|
|
echo "Script completed successfully."
|