Repository navigation
equivalence: dli_faults scenarios in carddemo-copaus1c and copaus0c (Part of #5233) - #6035
Conversation
…coverage refreshed (Part of #5233) COPAUS1C: 7 scenarios (GU AC/GB, qualified and unqualified GNP AC/GB, REPL AC -> ROLL-BACK), 44/48 branches. COPAUS0C: 6 scenarios (GU AC, GNP AC/GB, PF8 reposition AC/GE, the GNP after it AC), 84/93 branches. SCHD TC stays unplanned: the program's TERM after it is refused (no PSB scheduled in the model). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
No description provided. |
|
PR #6035 @ 3c151c5: 1 failed check(s) == db2 1/1 (failure) -- real |
|
No description provided. |
|
No description provided. |
Part of #5233 (slice 4: DL/I status faults under CICS in the COPAU* cases).
What
dli_faultsscenarios ({op, nth, status}, read byggdli.candDetDli) in the two burned-estate CICS cases, proven GnuCOBOL vs the det port (deployed entry point too), coverage ledger refreshed from aproof_sweep.py --det-onlyrun.AC/GB; qualified GNPAC/GB; PF8 GNPAC/GB; REPLAC(ROLL-BACK, the Db2 INSERT undone)AC; first GNPAC; mid-page GNPGB; PF8 reposition GNPACandGE; GNP after itACClass table (DL/I status arms in the CICS programs): GU / GNP / REPL arms of COPAUS0C and COPAUS1C handled here; SCHD
TCretry not handled (below).Not done: SCHD
TCretryPlanned
SCHD TCmakes the program issueTERM, which both stubs refuse (a TERM with no PSB scheduled,ggdli.c:827,DetDli.java:400). Modelling TC-then-TERM changes the runtime and re-proves every IMS port: own slice. It accounts for the 2 + 2 SCHD branches still uncovered (COPAUS1C l.580/590, COPAUS0C l.1007/1017).Notes
GEscenario in COPAUS0C is the harness's planned status, not a real qualified miss (still refused, I3).det_port.py runcrashes withKeyErrorinproof_orderwhen none of the requested cases has a recorded duration (new cases): I ran them alongside a recorded case.det_port_design.md(5 hand-written) + 2 regenerated coverage JSONs.Cross-repo: none.
Gates
pr_gates --fast7/7,--ratchets9/9, test_evidence / test_source_reads / test_proof_reach pass, the touched tests +test_equivalence_cics_dli.pypass. Near-overlap: PRs #5898 / #5900 touchequivalence_cics.py(not touched here); if either merges first the coverage ledger's harness hash goes stale and needsdet_coverage_ledger.py update.Lessons for agents
tests/tools/det_port.py runof only-new cases fails withKeyErrorinproof_order(proof_sweep.case_weightsreturns{}when no requested case has a recorded duration): include one recorded case (e.g.carddemo-posttran-generated) andgit checkoutits ledger file afterdet_coverage_ledger.py update.🤖 Generated with Claude Code