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

ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
MODEL_BOUND_VALUE="${MODEL_BOUND:-10}"
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

WORK="$(mktemp -d "${TMPDIR:-/tmp}/aiq-formal.XXXXXX")"
trap 'rm -rf "$WORK"' EXIT
if [[ "$MODEL_BOUND_VALUE" == "10" ]]; then
  (cd "$ROOT" && "$FASM_BIN" aiq_model_normal.asm "$WORK/model" >/dev/null)
else
  cp -R "$ROOT/." "$WORK/source"
  sed -i.bak "s/^MODEL_BOUND equ 10$/MODEL_BOUND equ $MODEL_BOUND_VALUE/" "$WORK/source/model_state.inc"
  rm "$WORK/source/model_state.inc.bak"
  (cd "$WORK/source" && "$FASM_BIN" aiq_model_normal.asm "$WORK/model" >/dev/null)
fi
"$WORK/model" >"$WORK/model.all"
sed '/^# ENC /d' "$WORK/model.all" >"$WORK/model.setdb"
"$SETDB_BIN" new "$WORK/model.db"
"$SETDB_BIN" load "$WORK/model.db" "$WORK/model.setdb"

initial="$($SETDB_BIN members "$WORK/model.db" Initial)"
reachable="$($SETDB_BIN expand "$WORK/model.db" Transition first "$initial")"
{
  echo "SADD Reachable $initial"
  while IFS= read -r state; do
    [[ -n "$state" ]] && echo "SADD Reachable $state"
  done <<<"$reachable"
} >"$WORK/reachable.setdb"
"$SETDB_BIN" load "$WORK/model.db" "$WORK/reachable.setdb"

properties=(HistoryAppendOnly CheckpointMonotonic ResultHasRequest ResultOperationMatchesRequest AtMostOneResultPerRequest AtMostOneTerminal TerminalIsAbsorbing DefinitionResourceConsistent)
violations_file="$WORK/violations.setdb"
: >"$violations_file"
for property in "${properties[@]}"; do
  bad="Bad${property}"
  "$SETDB_BIN" add "$WORK/model.db" "$bad" __empty__
  "$SETDB_BIN" remove "$WORK/model.db" "$bad" __empty__
  while IFS= read -r state; do
    [[ -n "$state" ]] && echo "SADD Violations $state" >>"$violations_file"
  done < <("$SETDB_BIN" intersect "$WORK/model.db" Reachable "$bad")
done
"$SETDB_BIN" add "$WORK/model.db" Violations __empty__
"$SETDB_BIN" remove "$WORK/model.db" Violations __empty__
[[ -s "$violations_file" ]] && "$SETDB_BIN" load "$WORK/model.db" "$violations_file"

violations="$($SETDB_BIN members "$WORK/model.db" Violations)"
states_count="$($SETDB_BIN members "$WORK/model.db" States | awk 'NF {n++} END {print n+0}')"
reachable_count="$($SETDB_BIN members "$WORK/model.db" Reachable | awk 'NF {n++} END {print n+0}')"
transition_count="$($SETDB_BIN pairs "$WORK/model.db" Transition | awk 'NF {n++} END {print n+0}')"
if [[ -n "$violations" ]]; then
  echo "FAIL bound=$MODEL_BOUND_VALUE states=$states_count transitions=$transition_count reachable=$reachable_count"
  echo "$violations"
  exit 1
fi
echo "PASS bound=$MODEL_BOUND_VALUE states=$states_count transitions=$transition_count reachable=$reachable_count violations=0"
