#!/usr/bin/env bash
# misc_illegal_requires — `nucleos verify` WITHOUT `-k` must match `dzn verify`.
#
# The model has BOTH a dead-code line in the `ihello` interface
# (`[false] on world: {}` — guard is constantly false) AND an illegal
# action in the component (`on h.hello(): w.world()` calls `world` on
# the requires port, which the interface forbids).
#
# dzn treats dead code as a WARNING: it reports the `code will never be
# executed` line and KEEPS GOING, so it still finds + reports the
# `<illegal>` counter-example, exiting 1. The dzn reference output is:
#
#   <file>:32:16: error: code will never be executed
#   error: illegal action performed in model illegal_requires
#   model: illegal_requires
#   h.hello
#   w.world
#   <illegal>
#
# nucleos's DEFAULT verify is fail-fast (dzn's `-k` is the inverse). The
# bug this test pins: nucleos must NOT stop at the dead-code report —
# dead code is a warning, not a fail-fast trigger — so `verify` (no `-k`)
# must still continue and emit the `<illegal>` counter-example, byte-for-
# byte matching dzn. (With `-k` it already did; this asserts the no-`-k`
# default.)
set -euo pipefail

F="$NUCTEST_TMPDIR/illegal_requires.dzn"
cat > "$F" <<'EOF'
interface ihello
{
  in void hello ();
  in void world ();
  behavior
  {
    on hello: {}
    [false] on world: {}
  }
}

component illegal_requires
{
  provides ihello h;
  requires ihello w;

  behavior
  {
    on h.hello (): w.world ();
  }
}
EOF

# The dead-code loc (line:col) = the `world` member of `[false] on world`,
# derived from this fixture's layout so it survives edits.
deadloc=$(awk '/\[false\] on world/{print NR":"index($0,"world"); exit}' "$F")

# Run verify WITHOUT -k (the default fail-fast mode). Capture combined
# output + exit code; normalize the absolute fixture path to a basename
# so the assertion is location-independent.
out=$("$NUCLEOS" verify -m illegal_requires "$F" 2>&1) && rc=0 || rc=$?
norm=$(printf '%s\n' "$out" | sed "s#${NUCTEST_TMPDIR}/##g")

# Expected = the dzn reference behaviour: dead-code warning AND the
# illegal counter-example (dead code did NOT stop the run).
expected="illegal_requires.dzn:${deadloc}: error: code will never be executed
error: illegal action performed in model illegal_requires
model: illegal_requires
h.hello
w.world
<illegal>"

if [[ "$norm" != "$expected" ]]; then
  echo "FAIL: nucleos verify (no -k) output != dzn reference"
  echo "--- expected (dzn) ---"; printf '%s\n' "$expected"
  echo "--- got (nucleos) ---";  printf '%s\n' "$norm"
  exit 1
fi

# dzn exits 1 (errors present: both dead code and the illegal).
if [[ "$rc" -ne 1 ]]; then
  echo "FAIL: expected exit 1 (errors present), got $rc"
  exit 1
fi

# --- Parity part 2: dead code ALONE is a pure warning → exit 0 (matches dzn). ---
# A model whose ONLY finding is dead code must report the warning and exit 0,
# exactly like `dzn verify` (which exits 0 on dead-code-only).
G="$NUCTEST_TMPDIR/deadcode_only.dzn"
cat > "$G" <<'EOF'
interface Ionly {
  in void a();
  in void b();
  behavior {
    on a: {}
    [false] on b: {}
  }
}
EOF
out2=$("$NUCLEOS" verify -m Ionly "$G" 2>&1) && rc2=0 || rc2=$?
norm2=$(printf '%s\n' "$out2" | sed "s#${NUCTEST_TMPDIR}/##g")
exp2="deadcode_only.dzn:$(awk '/\[false\] on b/{print NR":"index($0,"b")}' "$G"): error: code will never be executed"
if [[ "$norm2" != "$exp2" ]]; then
  echo "FAIL: dead-code-only output != dzn reference"
  echo "--- expected (dzn) ---"; printf '%s\n' "$exp2"
  echo "--- got (nucleos) ---";  printf '%s\n' "$norm2"
  exit 1
fi
if [[ "$rc2" -ne 0 ]]; then
  echo "FAIL: dead-code-only must exit 0 (warning, dzn parity), got $rc2"
  exit 1
fi

echo "ok: dead code is a warning — does not stop (illegal still found, exit 1)"
echo "ok: dead-code-only is a warning — exit 0 (dzn parity)"
