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

ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
TRACE_ROOT="$ROOT/../setdb"
FASM_BIN="${FASM_BIN:-$(command -v fasm)}"
SETDB_BIN="${SETDB_BIN:-$(command -v setdb || true)}"
[[ -n "$SETDB_BIN" ]] || SETDB_BIN=/tmp/aiq-setdb-bin
WORK="$(mktemp -d "${TMPDIR:-/tmp}/aiq-abstract-simulation.XXXXXX")"
trap 'rm -rf "$WORK"' EXIT

mkdir -p "$WORK/trace-source"
cp -R "$TRACE_ROOT/." "$WORK/trace-source"
sed -i.bak 's/^MODEL_BOUND equ 10$/MODEL_BOUND equ 12/' "$WORK/trace-source/model_state.inc"
rm "$WORK/trace-source/model_state.inc.bak"
(cd "$WORK/trace-source" && "$FASM_BIN" aiq_model_normal.asm "$WORK/trace" >/dev/null)
(cd "$ROOT" && "$FASM_BIN" abstract_model_normal.asm "$WORK/abstract" >/dev/null)
"$WORK/trace" >"$WORK/trace.all"
sed '/^# ENC /d' "$WORK/trace.all" >"$WORK/trace.facts"
"$WORK/abstract" >"$WORK/abstract.facts"

"$SETDB_BIN" new "$WORK/model.db"
"$SETDB_BIN" load "$WORK/model.db" "$WORK/trace.facts"
"$SETDB_BIN" load "$WORK/model.db" "$WORK/abstract.facts"

store_pairs() {
  local relation="$1"
  local facts="$2"
  awk -v relation="$relation" '
    /^\([^,]+,[^)]+\)$/ {
      line=$0
      sub(/^\(/, "", line)
      sub(/\)$/, "", line)
      split(line, pair, ",")
      print "RADD " relation " " pair[1] " " pair[2]
    }
  ' >"$facts"
  [[ -s "$facts" ]] && "$SETDB_BIN" load "$WORK/model.db" "$facts"
}

"$SETDB_BIN" inverse "$WORK/model.db" Beta \
  | store_pairs BetaInverse "$WORK/beta-inverse.facts"
"$SETDB_BIN" join "$WORK/model.db" BetaInverse Transition \
  | store_pairs AbstractToConcreteNext "$WORK/abstract-to-concrete.facts"
"$SETDB_BIN" join "$WORK/model.db" AbstractToConcreteNext Beta \
  | store_pairs ProjectedTransition "$WORK/projected.facts"

"$SETDB_BIN" domain "$WORK/model.db" Beta | while IFS= read -r state; do
  [[ -n "$state" ]] && echo "SADD BetaDomain $state"
done >"$WORK/beta-domain.facts"
"$SETDB_BIN" load "$WORK/model.db" "$WORK/beta-domain.facts"

missing_states="$($SETDB_BIN diff "$WORK/model.db" States BetaDomain)"
unmatched="$($SETDB_BIN rdiff "$WORK/model.db" ProjectedTransition ATransition)"
concrete_initial="$($SETDB_BIN members "$WORK/model.db" Initial)"
abstract_initial="$($SETDB_BIN select "$WORK/model.db" Beta first "$concrete_initial")"
initial_ok="$($SETDB_BIN member "$WORK/model.db" AInitial "$abstract_initial")"

if [[ -n "$missing_states" || -n "$unmatched" || "$initial_ok" != true ]]; then
  echo "SIMULATION_FAIL initial_ok=$initial_ok" >&2
  [[ -n "$missing_states" ]] && echo "missing_beta=$missing_states" >&2
  if [[ -n "$unmatched" ]]; then
    echo 'unmatched_transitions:' >&2
    printf '%s\n' "$unmatched" | head -20 >&2
  fi
  exit 1
fi

concrete_states="$($SETDB_BIN members "$WORK/model.db" States | awk 'NF {n++} END {print n+0}')"
concrete_transitions="$($SETDB_BIN pairs "$WORK/model.db" Transition | awk 'NF {n++} END {print n+0}')"
projected="$($SETDB_BIN pairs "$WORK/model.db" ProjectedTransition | awk 'NF {n++} END {print n+0}')"
echo "SIMULATION_PASS concrete_states=$concrete_states concrete_transitions=$concrete_transitions projected_transitions=$projected unmatched_initial=0 unmatched_transitions=0 concrete_bad=0"
