Skip to content

Model checking: deterministic config resolution and config-based outputs/traces#494

Closed
younes-io wants to merge 3 commits intomasterfrom
fix/restore-embedded-config-picking
Closed

Model checking: deterministic config resolution and config-based outputs/traces#494
younes-io wants to merge 3 commits intomasterfrom
fix/restore-embedded-config-picking

Conversation

@younes-io
Copy link
Collaborator

@younes-io younes-io commented Feb 4, 2026

  • Summary: restore custom model picking for embedded .tla configs and normalize model/trace naming
  • Root cause: the new resolver only considered adjacent .cfg files, so custom runs could not select .tla configs
  • Fix: add a customPick resolver mode for custom commands and strip .tla from model/trace names
  • Tests: npm test

@younes-io younes-io changed the title fix: restore embedded tla config picking Restore embedded .tla config picking Feb 4, 2026
@lemmy
Copy link
Member

lemmy commented Feb 5, 2026

@younes-io, "restore" implies that there’s a commit that caused the issue. Could you please share the commit? Was it mine? :-)

@younes-io younes-io changed the title Restore embedded .tla config picking Model checking: deterministic config resolution and config-based outputs/traces Feb 5, 2026
@younes-io
Copy link
Collaborator Author

You’re right, “restore” was a bad choice of wording.

master never lost .tla-as-config. checkModelCustom on master already lists *.cfg and *.tla.

the "restore" was within this PR, as part of a refactor.

So no “regression commit” on master, and not yours. I've changed the PR's title. Thanks for the tip

@younes-io
Copy link
Collaborator Author

Superseded by #495 (same changes + DCO sign-offs). Closing this PR to avoid duplicate review.

@younes-io younes-io closed this Feb 5, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants