You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
equivalence: model-port proofs don't run a case's LINKed programs (INQACC, XFRFUN, LGUPDB01 unprovable) #4188
A model-port proof (equivalence.py run <case> with a committed port/) runs only the case's main program as Java. Cases that LINK a second program ("programs": [...]) get no Java for that program, so whatever it writes never appears on the Java side.
Seen in #4168's loop runs. CBSA INQACC and XFRFUN (which LINK ABNDPROC) and GenApp LGUPDB01 (which LINKs LGUPVS01) were not proven after 4 attempts each. From attempt 2 on, every CICS event and Db2 row matched; only the record written by the LINKed program differed (ABNDFILE, KSDSPOLY).
Proposal
During a model-port proof, run the case's other programs from their proven det ports, or from committed model ports where they exist, so the task is complete on the Java side. The report should state which programs each side's Java came from.
Activity
Model ports CBSA INQACC, GenApp LGUPDB01: unedited model answers, pro…
equivalence: an SQL fault is injected only where its statement's prog…
equivalence: a port's proof runs the programs its task LINKs to as Ja…