Repository navigation
CICS POST / WAIT EVENT / terminal CONVERSE modelled (X63); SEND PAGE / PURGE MESSAGE stay refused (Part of #5079) - #5216
Merged
Conversation
Owner
Author
|
No description provided. |
squid-protocol
marked this pull request as ready for review
October 15, 2026 22:17
squid-protocol
enabled auto-merge (squash)
October 15, 2026 22:21
| if kind == "post": | ||
| _, label, how, n, h, m, s, reqid = op | ||
| j = lambda v: "null" if v is NG else str(v) # noqa: E731 | ||
| r = f'{{"{reqid}"}}' if False else (f'"{reqid}"' if reqid else "null") |
Contributor
squid-protocol
added a commit
that referenced
this pull request
Oct 16, 2026
…dling and #5216 POST/WAIT/CONVERSE/CANCEL) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
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
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.
Part of #5079
What
#5185 refused the last members of #5079's old-style set by name (SEND PAGE, PURGE MESSAGE, terminal CONVERSE, POST, WAIT EVENT). IBM's pages define POST, WAIT EVENT and CONVERSE (default) fully enough to model them, so this PR does, on both runtimes (det port
CicsTask/ stubggcics.c) and in the equivalence harness; SEND PAGE and PURGE MESSAGE stay refused by name. Register entry X63 (new; X59 trimmed to point at it) quotes each IBM page.INTERVAL | TIME | AFTER / AT HOURS MINUTES SECONDS [SET(ptr)] [REQID]: a 4-byte timer-event control area, "initialized to binary zeros", posted (first byte X'40', third X'80') at expiry. INVREQ RESP2 4 / 5 / 6, EXPIRED. The area is a block of task storage on the pointer lane (X47 / X58), soSET ADDRESS OF rec TO ptrshares its bytes.ECADDR(ptr) [NAME]: the area is posted at its expiry (a task takes no time, X4: the wait dispatches RUN children and runs the stated clock to the expiry); INVREQ RESP2 2 for a null pointer. CANCEL REQID finds a POST's REQID (NORMAL while unexpired, NOTFND once the wait expired it).FROM [FROMLENGTH] INTO [TOLENGTH] [MAXLENGTH] [NOTRUNCATE](terminal form): the FROM data recorded as a plain SEND records it, then the terminal RECEIVE of the reply (LENGERR cut, TOLENGTH the original length, NOTRUNCATE keeps the rest).cobol_eventshad noCANCELbranch, so any harness proof of a program with CANCEL compared Java's CANCEL event against nothing and mismatched. Added it.POST AFTER ...read AFTER as a second verb word; added to_SECOND_OPTIONS.Class table (old-style CICS commands that were refused whole)
Assumed (X63; IBM leaves open) / refused
Assumed: a POSTed area is posted only by WAIT EVENT or a CANCEL (a task takes no time, and SUSPEND, the polling IBM suggests, is refused); WAIT EVENT on an already posted area returns at once; a POST with no REQID runs under POST0001, POST0002 ... in EIBREQID; an EXPIRED POST leaves SET's pointer as it was; a negative FROMLENGTH is LENGERR with nothing sent. Refused at run time: WAIT EVENT on an address that is no POST's area, or on one a later POST / CANCEL / local START / DELAY ended (IBM: "unpredictable"); CONVERSE on an LUTYPE2 terminal (EOC is not among CONVERSE's conditions).
Evidence level (policy 1)
test_post_wait_converse_e2e_5079.py, GnuCOBOL + stub vs det port under CicsTask,EQUIVALENCE_E2E=1), 2 scenarios (reply fits / reply cut), 14 events each, 0 diffs, PROVED; paragraphs 2/2, branches 4/4 (reported "not proven" by the harness: coverage is not the corpus's).test_post_wait_converse_5079.py: every expiry form and range, EXPIRED, generated REQID, WAIT on a posted / unposted / null / foreign / ended area, CANCEL of a POST, CONVERSE that fits / is cut / keeps the rest / has a negative or zero length, LUTYPE2 refusal), 83 tests.Gates
pr_gates --fast6/6;--ratchets8/8, none skipped (cics-spec, ports, port-surface, estate, fact-crosscheck, completeness, ground-truth, time).det_port.py check: 98 of 112 ports differ only by the 126 added lines ofCicsTask.java(no generated service code moved), 14 unchanged; re-provedcarddemo-acctviewandzecs-ecs001PROVED. Golden masters not touched (no scan output moves). cics-spec counts: 98 modelled, 155 name-only.Cross-repo
No companion PR is needed to merge. cics-crucible cases to queue (separate items): POST AFTER + WAIT EVENT + CANCEL NOTFND; a second POST ends the first area (refused); CONVERSE with a reply that fits and one that is cut (LENGERR, TOLENGTH the original length); WAIT EVENT on a null pointer (INVREQ RESP2 2); POST TIME already past (EXPIRED).
Overlap: open PRs #5204 / #5211 / #5213 also touch
det/cics.py,ggcics.candequivalence_cics.py(this PR adds new functions beside the existing ones, and one 4-line edit totest_det_translate.py, which #5204 / #5213 also touch).Lessons for agents
equivalence_cics.cobol_events: an event the stub logs but that function does not read shows up as a Java-only event in the proof ("event 3: ('SEND-TEXT', 'CANCEL')"), not as a stub bug.textwrap.wrap) when a test builds programs from command strings.🤖 Generated with Claude Code