#!/usr/bin/env bash
# gate/model/trace.sh — ties the gate's code to its model: replays a log the code wrote
# (gate/worker.js) against Gate.tla. trace.py turns each entry that changed the gate's
# records into the step of Gate.tla it stands for, with the logged values; TraceGate.tla
# lets TLC take exactly those steps, in order. TLC either replays the whole log, so every
# change the code made is one the model allows, or stops at the first entry the model does
# not allow, and this says which.
#
#   bash gate/model/trace.sh LOG.json          a saved /v1/log (entries from the first)
#   bash gate/model/trace.sh https://<gate>    a gate's public log, read here
#
# tests/gate.sh runs it on the log of the gate's own test run, so a change to worker.js
# that does what the model does not allow fails CI. It checks what the code did, not what
# it refused (a refusal changes nothing in either). Needs Docker and python3; TLC runs with
# no network, on one core. Exit 0 only if the whole log replays.

set -uo pipefail
cd "$(dirname "$0")" || exit 2
src="${1:-}"
[ -n "$src" ] || { echo "usage: bash gate/model/trace.sh LOG.json | https://<gate>"; exit 2; }

IMG="arbiter_tlc_trace_$$"
OUT=$(mktemp -d -p /var/tmp)   # on disk: TLC and tlapm write a lot, and /tmp may be in memory
cleanup() { docker rmi -f "$IMG" >/dev/null 2>&1 || true; rm -rf "$OUT"; }
trap cleanup EXIT
trap 'exit 130' INT TERM
chmod 777 "$OUT"

if [[ "$src" == https://* ]]; then
  # The log in pages of 500, then one JSON with every entry from the first.
  after=0; : > "$OUT/pages"
  while :; do
    curl -fsS --max-time 30 "${src%/}/v1/log?after=$after&limit=500" -o "$OUT/page.json" ||
      { echo "ABORT: could not read ${src%/}/v1/log"; exit 2; }
    n=$(python3 -I -c 'import json,sys; print(len(json.load(open(sys.argv[1]))["entries"]))' "$OUT/page.json") || exit 2
    cat "$OUT/page.json" >> "$OUT/pages"; echo >> "$OUT/pages"
    [ "$n" -lt 500 ] && break
    after=$((after + n))
  done
  python3 -I -c '
import json, sys
pages = [json.loads(l) for l in open(sys.argv[1]) if l.strip()]
json.dump({"gate": pages[0]["gate"], "entries": [e for p in pages for e in p["entries"]]}, open(sys.argv[2], "w"))
' "$OUT/pages" "$OUT/log.json" || exit 2
else
  cp "$src" "$OUT/log.json" || { echo "ABORT: no log at $src"; exit 2; }
fi

echo "=== the log replayed against Gate.tla ==="
summary=$(python3 -I trace.py "$OUT/log.json" "$OUT") || { echo "ABORT: $summary"; exit 2; }
echo "  $summary"
cp Gate.tla TraceGate.tla TraceGate.cfg "$OUT/" && chmod 666 "$OUT"/*.tla "$OUT"/*.cfg
docker build -q -t "$IMG" . >/dev/null || { echo "ABORT: could not build the TLC image"; exit 2; }
docker run --rm --network none --cpus 1 -m 2g -v "$OUT:/work" -w /work "$IMG" \
  java -Xmx1g -XX:+UseParallelGC -cp /opt/tla2tools.jar tlc2.TLC -workers 1 \
  -metadir /work/states -config TraceGate.cfg TraceGate.tla > "$OUT/tlc.log" 2>&1

total=$(python3 -I -c 'import json,sys; print(len(json.load(open(sys.argv[1]))["entries"]))' "$OUT/log.json")
i=$(awk '/^\/\\ i = /{i=$4} END{print i}' "$OUT/tlc.log")
ph=$(awk '/^\/\\ ph = /{p=$4} END{print p}' "$OUT/tlc.log")
if grep -q 'Invariant NotDone is violated' "$OUT/tlc.log" && [ "$i" = "$((total + 1))" ]; then
  echo "  PASS  the model takes all $total entries, in order: every change the code made is a step of Gate.tla"
  exit 0
fi
if grep -q 'Deadlock reached' "$OUT/tlc.log" && [ -n "$i" ]; then
  echo "  FAIL  the model does not allow log entry #$i (its step $ph); the entries up to it:"
  python3 -I -c '
import json, sys
E = json.load(open(sys.argv[1]))["entries"]; i = int(sys.argv[2])
for e in E[max(0, i - 4):i]:
    b = json.loads(e["body"])
    what = json.loads(b["terms"]).get("op") if e["kind"] == "owner_op" else {k: b[k] for k in ("request", "by", "fp", "key") if k in b}
    print("    #%-4s %s  %-22s %s" % (e["seq"], e["at"], e["kind"], what))
' "$OUT/log.json" "$i"
  exit 1
fi
echo "  ABORT  TLC ended some other way:"
tail -25 "$OUT/tlc.log" | sed 's/^/    /'
exit 2