Model checking: deterministic config resolution + embedded .tla config picking

[younes-io]

• Summary: Harden model resolution and artifact naming; keep custom runs able to pick embedded .tla configs. (Supersedes Model checking: deterministic config resolution and config-based outputs/traces #494: DCO requires sign-offs and the old branch would need a force-push.)
• Root cause: The model-resolution refactor stopped offering .tla configs in the custom picker; Windows CI was also asserting raw path casing and a SANY-based test was too tight on timeouts.
• Fix: Add resolver modes (adjacent default, customPick for custom runs); compute modelName from path.parse(cfgPath).name; base outputs/traces on the chosen config; make -config accept absolute paths; adjust tests for Windows + increase the SANY test timeout on Windows.
• Tests: npm test