fix(tla): enumerate memberships in a disjunctive Init conjunct (Prisoner under-exploration) - #190
Merged
Merged
Conversation
…ner under-exploration)
An Init that is a conjunction with a disjunctive conjunct —
`/\ A /\ (\/ B1 \/ B2) /\ C` — dropped the disjunct branches' initial
states. `evaluate_init_states` handled a whole-body top-level disjunction
but not a disjunction nested as ONE conjunct: the clause path evaluated the
`\/` conjunct as a boolean guard, and with an unbound state variable that
reads FALSE (`light \in {"off","on"}` with `light` unbound is
`ModelValue("light") \in {..}` = false), so the branch's membership/equality
alternatives were never enumerated. Prisoner{Solo,}LightUnknown lost the
`\/ Light_Unknown /\ light \in {"off","on"}` alternative, producing 1 initial
state instead of 2 → under-exploration (Solo 2 vs 4, Light 30 vs 62).
Fix: after `merged_clauses` rejoins any split disjunction, if a clause is a
top-level disjunction, DISTRIBUTE the Init over it —
`(A /\ B1 /\ C) \/ (A /\ B2 /\ C)` — and recurse each alternative (reusing
the whole-body-disjunction path). Distributing over `merged_clauses` (not a
raw `split_top_level(_, "/\\")`, which shreds a disjunct's inner `/\` guards)
keeps each disjunction whole. A disjunct with a false constant guard
(`~Light_Unknown` when `Light_Unknown = TRUE`) yields zero states via the
existing guard check, so the union is exact; recursion terminates (each level
removes one disjunctive conjunct).
Result: PrisonerSoloLightUnknown 4 == TLC, PrisonerLightUnknown 62 == TLC.
Gate: diff_tlc 20/20 (adds InitDisjunctConjunct, 2 == TLC), cargo test
--release 1486 passed / 0 failed.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
An
Initthat is a conjunction with a disjunctive conjunct —/\ A /\ (\/ B1 \/ B2) /\ C— dropped the disjunct branches' initial states.evaluate_init_stateshandled a whole-body top-level disjunction, but not a disjunction nested as one conjunct of a conjunctive Init. The clause path evaluated the\/conjunct as a boolean guard, and with an unbound state variable that reads FALSE (light \in {"off","on"}withlightunbound isModelValue("light") \in {..}= false), so the branch's membership/equality alternatives were never enumerated.Prisoner{Solo,}LightUnknown (
Prisoners_Single_Switch) lost the\/ Light_Unknown /\ light \in {"off","on"}alternative → 1 initial state instead of 2 → under-exploration:PrisonerSoloLightUnknown: ours 2 → 4 (== TLC)PrisonerLightUnknown: ours 30 → 62 (== TLC)Fix
After
merged_clausesrejoins any split disjunction, if a clause is a top-level disjunction, distribute the Init over it —(A /\ B1 /\ C) \/ (A /\ B2 /\ C)— and recurse each alternative (reusing the existing whole-body-disjunction path).merged_clauses(not a rawsplit_top_level(_, "/\\"), which shreds a disjunct's inner/\guards likeLight_Unknown /\ …) keeps each disjunction whole.~Light_UnknownwhenLight_Unknown = TRUE) yields zero states via the existing guard check, so the union is exact.Validation
PrisonerSoloLightUnknown4 == TLC,PrisonerLightUnknown62 == TLC.scripts/diff_tlc.sh: 20/20 — addsInitDisjunctConjunct(guarded disjunctive Init conjunct, 2 == TLC; also covers the unbounded-union case).cargo test --release: 1486 passed / 0 failed.