Improve TLC checker script to be more flexible

examples/classic/distributed/ewd426/README.md

@@ -5,7 +5,12 @@ This folder contains Quint specifications for the three different self-stabiliza
 2. A solution with three-state machines [ewd426_3.qnt](ewd426_3.qnt)
 3. A solution with four-state machines [ewd426_4.qnt](ewd426_4.qnt)
 
-Due to the presence of temporal properties and fairness, we need to use TLC to model check these specs. As the integration with TLC is not completed, we provide a script to automate running it for these specific specifications: [check_with_tlc.sh](check_with_tlc.sh).
+Due to the presence of temporal properties and fairness, we need to use TLC to model check these specs. As the integration with TLC is not completed, we provide a script to automate running it for these specific specifications: [check_with_tlc.sh](../../../../tlc/check_with_tlc.sh). Usage:
+
+```sh
+sh check_with_tlc.sh --file ewd426_3.qnt --temporal convergence,closure,persistence
+sh check_with_tlc.sh --file ewd426_4.qnt --temporal convergence,closure,persistence
+```
 
 If you are trying to learn/understand these algorithms, we recommend playing with the Quint REPL. For that, pick one of the files (for example [ewd426.qnt](ewd426.qnt)) and run the following command in the terminal:
 ``` sh

tlc/check_with_tlc.sh

@@ -0,0 +1,133 @@
+#!/bin/bash
+
+# Load common utilities
+source ./common.sh || { echo "Error: Could not load common.sh"; exit 1; }
+
+# Default configurations
+APALACHE_JAR="$HOME/.quint/apalache-dist-0.47.2/apalache/lib/apalache.jar"
+JAVA_OPTS="-Xmx8G -Xss515m"
+FILE=""  # Mandatory: User must specify a file
+
+# Optional parameters
+INVARIANTS=()
+TEMPORAL_PROPS=()
+
+# Function to parse command-line arguments
+parse_args() {
+    while [[ $# -gt 0 ]]; do
+        case "$1" in
+            --invariant)
+                shift
+                IFS=',' read -ra INVARIANTS <<< "$1"
+                ;;
+            --temporal)
+                shift
+                IFS=',' read -ra TEMPORAL_PROPS <<< "$1"
+                ;;
+            --file)
+                shift
+                FILE="$1"
+                ;;
+            --apalache-jar)
+                shift
+                APALACHE_JAR="$1"
+                ;;
+            --help)
+                echo "Usage: $0 --file FILE.qnt [--invariant INV1,INV2] [--temporal TEMP1,TEMP2] [--apalache-jar JAR_PATH]"
+                exit 0
+                ;;
+            *)
+                err "Unknown option: $1"
+                exit 1
+                ;;
+        esac
+        shift
+    done
+
+    # Ensure exactly one file is provided
+    if [[ -z "$FILE" ]]; then
+        err_and_exit "You must specify a Quint file using --file FILE.qnt"
+    fi
+}
+
+# Function to generate the compilation arguments dynamically
+generate_compile_options() {
+    local options=()
+    if [[ ${#INVARIANTS[@]} -gt 0 ]]; then
+        options+=("--invariant=$(IFS=,; echo "${INVARIANTS[*]}")")
+    fi
+    if [[ ${#TEMPORAL_PROPS[@]} -gt 0 ]]; then
+        options+=("--temporal=$(IFS=,; echo "${TEMPORAL_PROPS[*]}")")
+    fi
+    echo "${options[*]}"
+}
+
+# Function to create a standard .cfg file
+create_cfg_file() {
+    local cfg_file="$1"
+    echo "INIT" > "$cfg_file"
+    echo "q_init" >> "$cfg_file"
+    echo "" >> "$cfg_file"
+    echo "NEXT" >> "$cfg_file"
+    echo "q_step" >> "$cfg_file"
+
+    # Add default invariant if invariants were specified
+    if [[ ${#INVARIANTS[@]} -gt 0 ]]; then
+        echo "" >> "$cfg_file"
+        echo "INVARIANT" >> "$cfg_file"
+        echo "q_inv" >> "$cfg_file"
+    fi
+
+    # Add default temporal properties if any were specified
+    if [[ ${#TEMPORAL_PROPS[@]} -gt 0 ]]; then
+        echo "" >> "$cfg_file"
+        echo "PROPERTY" >> "$cfg_file"
+        echo "q_temporalProps" >> "$cfg_file"
+    fi
+}
+
+# Function to run TLC model checker
+run_tlc() {
+    local tla_file="$1"
+    local output
+
+    info "Running TLC for $tla_file..."
+    output=$(java $JAVA_OPTS -cp "$APALACHE_JAR" tlc2.TLC -deadlock "$tla_file" 2>&1)
+
+    if echo "$output" | grep -q "Model checking completed. No error has been found."; then
+        info "Model checking succeeded for $tla_file"
+    else
+        err_and_exit "Model checking failed for $tla_file\n$output"
+    fi
+}
+
+# Main function to process the file
+process_file() {
+    local base_name="${FILE%.qnt}"
+    local tla_file="${base_name}.tla"
+    local cfg_file="${base_name}.cfg"
+
+    info "Processing $FILE..."
+
+    # Step 1: Compile the .qnt file to .tla
+    local compile_options
+    compile_options=$(generate_compile_options)
+    quint compile --target=tlaplus "$FILE" $compile_options > "$tla_file" || err_and_exit "Compilation failed for $FILE"
+
+    # Step 2: Create .cfg file with `q_inv` and `q_temporalProps`
+    create_cfg_file "$cfg_file"
+
+    # Step 3: Run model checker
+    run_tlc "$tla_file"
+
+    # Step 4: Cleanup
+    rm -f "$tla_file" "$cfg_file"
+}
+
+# Parse command-line arguments
+parse_args "$@"
+
+# Process the single file
+process_file
+
+info "File processed successfully."

tlc/common.sh

@@ -0,0 +1,30 @@
+#!/bin/bash
+
+# ANSI color codes
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[0;33m'
+NC='\033[0m' # No Color
+
+function log() {
+    local level="${1}"
+    shift
+    echo -e "[$(date -u +"%Y-%m-%d %H:%M:%S")] [${level}]: ${@}"
+}
+
+function err_and_exit() {
+    log "${RED}ERROR${NC}" "${1}" >&2
+    exit ${2:-1}
+}
+
+function err() {
+    log "${RED}ERROR${NC}" "${1}" >&2
+}
+
+function info() {
+    log "${GREEN}INFO${NC}" "${1}"
+}
+
+function warn() {
+    log "${YELLOW}WARN${NC}" "${1}"
+}