Fix spin transition-validation example and trace capture

[Qian-Cheng-nju]

Fixes #22.

The spin example omitted nonblocking request events, so 87 acquisition windows could not match the required single-step transition. This records the missing event and corrects the failed-CAS lock observation, removes the reference model's held-lock requirement for starting a request, and rejects incomplete or inconsistent trace input.

The default fixture now comes from a focused Asterinas/QEMU kernel test; the original windows remain byte-for-byte under legacy/. The candidate specification is unchanged. The runner checks tool installation and separates mismatches from errors/timeouts. Batch tests retain every window, use two workers and allow ten minutes for the largest batch; individual TLC calls retain their 30-second timeout.

Validation:

• Clean, pinned Asterinas/QEMU capture: 11 executed events; candidate acquisition windows 3/3 and reference windows 11/11 pass.
• Legacy data: original 123 pass / 87 fail reproduced; corrected reference passes all 543 windows.
• Reverting the two logging fixes produces 9 events and an incorrect unlocked observation after failed CAS; the strict generator rejects that capture.
• Regression tests cover invalid acquisitions/releases, capture integrity, malformed input and missing tools.

The new kernel fixture uses three logical actors on one CPU; it does not exercise concurrent stress or the blocking spin loop. Historical benchmark scores are not recalculated.