#!/usr/bin/env bash
# gate/model/check.sh — TLC checks the gate's model (Gate.tla) for every order of events
# up to the bounds in Gate.cfg. gate-2 must keep every property in every state it can
# reach. Each known-bad design, the same model with one check removed (Mut), must break
# the property named for it: that shows the properties can fail, and what each check is
# for. One of them is gate-1, before 18 October.
#
#   bash gate/model/check.sh               every case
#   bash gate/model/check.sh gate-1        the cases whose name starts with this
#
# Needs only Docker. TLC runs with no network, on TLC_CPUS cores (default 1, so it can
# run on the production server beside ARBITER). Exit 0 only if every case ends as expected.

set -uo pipefail
cd "$(dirname "$0")" || exit 2

IMG="arbiter_tlc_$$"
OUT=$(mktemp -d)
cleanup() { docker rmi -f "$IMG" >/dev/null 2>&1 || true; rm -rf "$OUT"; }
trap cleanup EXIT
trap 'exit 130' INT TERM
chmod 777 "$OUT"
umask 000

docker build -q -t "$IMG" . >/dev/null || { echo "ABORT: could not build the TLC image"; exit 2; }

# name | constants changed from Gate.cfg (;-separated) | "holds", or the property TLC must find violated
# Gate.cfg is the payments config: any state the owner's changes can reach, two requests, and
# one change by the owner at any moment while they wait. OWNERS checks changes of authority:
# two owners, three changes, everything granted at the start, no requests. SETUP starts with
# nothing: setup, registrations, the four changes a payment needs, then one request.
OWNERS='Start = "granted";Owners = {o, o2};MaxOps = 3;ReqIds = {}'
SETUP='Start = "setup";Tenants = {t1};MaxOps = 4;ReqIds = {r1}'
CASES=(
  "gate-2: payments|Mut = {}|holds"
  "gate-2: owner changes|Mut = {};$OWNERS|holds"
  "gate-2: from setup|Mut = {};$SETUP|holds"
  "gate-1: key and payee not re-checked at approval|Mut = {\"no_standing\"}|G1_ApprovedWithAuthorityInForce"
  "an approval checked only before its transaction|Mut = {\"verify_only\"}|G1_ApprovedWithAuthorityInForce"
  "approval terms without the request id and hash|Mut = {\"terms_without_request\"}|G1_PaidOnlyAsAPersonApproved"
  "an approval leaves the request pending|Mut = {\"no_single_use\"}|G2_AtMostOnce"
  "no record of applied changes (used_ops)|Mut = {\"no_used_ops\"};$OWNERS|G3_AuthorityOnlyByOwners"
  "the signer not re-checked in a change's transaction|Mut = {\"no_signer_recheck\"};$OWNERS|G3_AuthorityOnlyByOwners"
)

fail=0; n=0
for c in "${CASES[@]}"; do
  IFS='|' read -r name sets expect <<< "$c"
  case "$name" in "${1:-}"*) ;; *) continue ;; esac
  n=$((n + 1))
  cfg="$OUT/case$n.cfg"
  cp Gate.cfg "$cfg"
  IFS=';' read -ra kvs <<< "$sets"
  for kv in "${kvs[@]}"; do
    key="${kv%% =*}"
    grep -qE "^    $key = " "$cfg" || { echo "ABORT: Gate.cfg has no constant $key"; exit 2; }
    awk -v k="$key" -v line="    $kv" '$0 ~ "^    " k " = " { print line; next } { print }' "$cfg" > "$cfg.new" && mv "$cfg.new" "$cfg"
  done
  echo "=== $name ($sets) ==="
  start=$(date +%s)
  # TLC reads a config only from the spec's own folder: each case gets a folder with both.
  mkdir -p "$OUT/case$n" && cp Gate.tla "$OUT/case$n/" && mv "$cfg" "$OUT/case$n/Case.cfg"
  docker run --rm --network none --cpus "${TLC_CPUS:-1}" -m 3g -v "$OUT/case$n:/work" -w /work "$IMG" \
    java -Xmx2g -XX:+UseParallelGC -cp /opt/tla2tools.jar tlc2.TLC -workers auto \
    -metadir /work/states -config Case.cfg Gate.tla > "$OUT/case$n.log" 2>&1
  rc=$?
  secs=$(( $(date +%s) - start ))
  grep -E 'states generated|depth of the complete state graph' "$OUT/case$n.log" | sed 's/^/  /'
  violated=$(grep -oE '(Invariant|Action property) [A-Za-z0-9_]+ is violated' "$OUT/case$n.log" | head -1 | awk '{print $(NF-2)}')
  if [ "$expect" = holds ]; then
    if [ $rc -eq 0 ] && grep -q 'No error has been found' "$OUT/case$n.log"; then
      echo "  PASS  every property holds (${secs}s)"
    else
      echo "  FAIL  expected every property to hold (TLC exit $rc${violated:+, $violated violated})"
      tail -60 "$OUT/case$n.log" | sed 's/^/    /'
      fail=1
    fi
  else
    if [ "$violated" = "$expect" ]; then
      echo "  PASS  TLC finds $expect violated (${secs}s); its shortest counterexample:"
      grep -E '^State [0-9]+: ' "$OUT/case$n.log" | sed -E 's/^State ([0-9]+): <([A-Za-z]+).*/    \1. \2/'
    else
      echo "  FAIL  expected $expect violated, got: ${violated:-none} (TLC exit $rc)"
      tail -60 "$OUT/case$n.log" | sed 's/^/    /'
      fail=1
    fi
  fi
done

[ $n -gt 0 ] || { echo "ABORT: no case is named ${1:-}"; exit 2; }
echo
[ $fail -eq 0 ] && echo "Result: all $n cases as expected" || echo "Result: NOT all $n cases as expected"
exit $fail