mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-25 14:25:02 +00:00
95 lines
2.3 KiB
Bash
Executable File
95 lines
2.3 KiB
Bash
Executable File
#!/bin/bash
|
|
# Validate TLA+ Specifications
|
|
# This script checks the syntax of all TLA+ specifications in the spec directory
|
|
|
|
set -e
|
|
|
|
SPEC_DIR="$(dirname "$0")"
|
|
TLA_TOOLS="${TLA_TOOLS:-/tmp/tla2tools.jar}"
|
|
|
|
# Color output
|
|
RED='\033[0;31m'
|
|
GREEN='\033[0;32m'
|
|
YELLOW='\033[1;33m'
|
|
NC='\033[0m' # No Color
|
|
|
|
echo "TLA+ Specification Validator"
|
|
echo "============================="
|
|
echo ""
|
|
|
|
# Check if TLA+ tools are available
|
|
if [ ! -f "$TLA_TOOLS" ]; then
|
|
echo -e "${YELLOW}TLA+ tools not found at $TLA_TOOLS${NC}"
|
|
echo "Downloading TLA+ tools..."
|
|
wget -q -O "$TLA_TOOLS" https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
|
|
if [ $? -eq 0 ]; then
|
|
echo -e "${GREEN}✓ Downloaded TLA+ tools${NC}"
|
|
else
|
|
echo -e "${RED}✗ Failed to download TLA+ tools${NC}"
|
|
exit 1
|
|
fi
|
|
fi
|
|
|
|
# Check Java
|
|
if ! command -v java &> /dev/null; then
|
|
echo -e "${RED}✗ Java not found. Please install Java 11 or later.${NC}"
|
|
exit 1
|
|
fi
|
|
|
|
echo "Using TLA+ tools: $TLA_TOOLS"
|
|
echo ""
|
|
|
|
# List of specifications to validate
|
|
SPECS=(
|
|
"metabuilder.tla"
|
|
"workflow_system.tla"
|
|
"collaboration.tla"
|
|
"integrations.tla"
|
|
)
|
|
|
|
FAILED=0
|
|
PASSED=0
|
|
|
|
# Validate each specification
|
|
for spec in "${SPECS[@]}"; do
|
|
spec_path="$SPEC_DIR/$spec"
|
|
|
|
if [ ! -f "$spec_path" ]; then
|
|
echo -e "${YELLOW}⚠ Skipping $spec (file not found)${NC}"
|
|
continue
|
|
fi
|
|
|
|
echo "Validating $spec..."
|
|
|
|
# Run SANY (syntax and semantic analyzer)
|
|
output=$(java -cp "$TLA_TOOLS" tla2sany.SANY "$spec_path" 2>&1)
|
|
|
|
# Check for errors
|
|
if echo "$output" | grep -q "Semantic errors:" || echo "$output" | grep -q "Parsing or semantic analysis failed."; then
|
|
echo -e "${RED}✗ $spec: FAILED${NC}"
|
|
echo "$output" | grep -A 10 "Semantic errors:"
|
|
FAILED=$((FAILED + 1))
|
|
else
|
|
echo -e "${GREEN}✓ $spec: PASSED${NC}"
|
|
PASSED=$((PASSED + 1))
|
|
fi
|
|
|
|
echo ""
|
|
done
|
|
|
|
# Summary
|
|
echo "============================="
|
|
echo "Validation Summary"
|
|
echo "============================="
|
|
echo -e "${GREEN}Passed: $PASSED${NC}"
|
|
echo -e "${RED}Failed: $FAILED${NC}"
|
|
echo ""
|
|
|
|
if [ $FAILED -eq 0 ]; then
|
|
echo -e "${GREEN}All specifications are valid!${NC}"
|
|
exit 0
|
|
else
|
|
echo -e "${RED}Some specifications have errors. Please review the output above.${NC}"
|
|
exit 1
|
|
fi
|