#!/usr/bin/env bash
set -euo pipefail

ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
FASM_BIN="${FASM_BIN:-$(command -v fasm)}"
SETDB_BIN="${SETDB_BIN:-$(command -v setdb || true)}"
if [[ -z "$SETDB_BIN" && -x /tmp/aiq-setdb-bin ]]; then
  SETDB_BIN=/tmp/aiq-setdb-bin
fi
if [[ -z "$SETDB_BIN" ]]; then
  echo 'setdb not found; set SETDB_BIN' >&2
  exit 2
fi

BASE_BOUND=12
GUARD_BOUND=14
CORE_HEX_LENGTH=$((1 + (8 + BASE_BOUND * 4) * 2))
WORK="$(mktemp -d "${TMPDIR:-/tmp}/aiq-saturation.XXXXXX")"
trap 'rm -rf "$WORK"' EXIT

build_graph() {
  local bound="$1"
  local target="$WORK/bound-$bound"
  mkdir -p "$target/source"
  cp -R "$ROOT/." "$target/source"
  sed -i.bak "s/^MODEL_BOUND equ 10$/MODEL_BOUND equ $bound/" "$target/source/model_state.inc"
  rm "$target/source/model_state.inc.bak"
  (cd "$target/source" && "$FASM_BIN" aiq_model_normal.asm "$target/model" >/dev/null)
  "$target/model" >"$target/model.all"
  sed '/^# ENC /d' "$target/model.all" >"$target/model.setdb"
  "$SETDB_BIN" new "$target/model.db"
  "$SETDB_BIN" load "$target/model.db" "$target/model.setdb"
  "$SETDB_BIN" members "$target/model.db" States | sort >"$target/states"
  "$SETDB_BIN" pairs "$target/model.db" Transition | sort >"$target/transitions"
  awk -v core_length="$CORE_HEX_LENGTH" '/^# ENC / {print $3, substr($4, 1, core_length)}' \
    "$target/model.all" | sort >"$target/core-encodings"
}

MODEL_BOUND="$BASE_BOUND" "$ROOT/verify" >/dev/null
MODEL_BOUND="$GUARD_BOUND" "$ROOT/verify" >/dev/null
build_graph "$BASE_BOUND"
build_graph "$GUARD_BOUND"

for relation in states transitions core-encodings; do
  if ! cmp -s "$WORK/bound-$BASE_BOUND/$relation" "$WORK/bound-$GUARD_BOUND/$relation"; then
    echo "SATURATION_FAIL relation=$relation base=$BASE_BOUND guard=$GUARD_BOUND" >&2
    diff -u "$WORK/bound-$BASE_BOUND/$relation" "$WORK/bound-$GUARD_BOUND/$relation" | head -80 >&2 || true
    exit 1
  fi
done

states_count="$(wc -l <"$WORK/bound-$BASE_BOUND/states" | tr -d ' ')"
transition_count="$(wc -l <"$WORK/bound-$BASE_BOUND/transitions" | tr -d ' ')"
echo "SATURATION_PASS base=$BASE_BOUND guard=$GUARD_BOUND max_append_batch=2 states=$states_count transitions=$transition_count"
