Use TLC -dump option to generate a SVG trace of a model behavior

tlcdump.bash

#!/bin/bash

# Description: This script runs TLC2 on a TLA+ specification file,
# generates a DOT file, converts it to SVG format, and opens the SVG file.
# Usage: ./script.sh <spec_file.tla>

# Function to display usage information
usage() {
    echo "Usage: $0 <spec_file.tla>"
    exit 1
}

# Check if the correct number of arguments is provided
if [ "$#" -ne 1 ]; then
    usage
fi

# Check if the input file exists and is readable
SPEC="$1"
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
TOOLS_JAR="$HOME/Downloads/tla2tools.jar"
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"

# Run TLC2 with the -dump dot option
echo "Running TLC2 on '$SPEC_FILE'..."
java -XX:+UseParallelGC -cp "$TOOLS_JAR" tlc2.TLC -dump dot,colorize,actionlabels "$BASENAME" "$SPEC"
TLC_EXIT_STATUS=$?

# Check if TLC2 succeeded or failed
if [ $TLC_EXIT_STATUS -ne 0 ]; then
    echo "TLC2 encountered an error. 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"

# Clean up the DOT files
echo "Cleaning up DOT files..."
rm -f "$MAINOUT" "$LIVEOUT"

# Open the SVG file
echo "Opening '$SVGOUT'..."
open "$SVGOUT"

echo "Script completed successfully."