Check refinement of high-level spec abs with all models

[lemmy]

• Move refinement mapping from TLC-specific module into ccfraft. Clearly, refinement mapping belongs in ccfraft, but we couldn't do that up until recently because of a TLC limitation that was resolved by Better parameterized instantiation support tlaplus/tlaplus#441 (depended on TLA+ PR Refinement checking for INSTANCEs with arguments. tlaplus/tlaplus#1014)
• Add CopyMaxAndExtend action. Add node may copy the longest log from some other node and extend the copied log in one step. Background: Check refinement of high-level spec abs for configs with reconfiguration. #6493 (comment)
• Check refinement of high-level spec abs for all configs (reconfiguration, simulation).
• When checking refinement, prevent TLC from enumerating the set of suffixes by expressing abs!Extend and abs!CopyMaxAndExtend axiomatically.

Replaces #6493 and depends on #6508.

[achamayou]

Unless I am missing something, this change is adding very substantially to the runtime of long model checks:

Before: https://github.com/microsoft/CCF/actions/runs/11107110210/job/30856948052

After: https://github.com/microsoft/CCF/actions/runs/11127867170/job/30921202022?pr=6509

These are already by far our longest running jobs, my fervent hope is that we find ways to speed them up so we can relax the state space restrictions, and this seems to be taking us in the wrong direction.

[lemmy]

Unless I am missing something, this change is adding very substantially to the runtime of long model checks:

[...]

These are already by far our longest running jobs, my fervent hope is that we find ways to speed them up so we can relax the state space restrictions, and this seems to be taking us in the wrong direction.

This doesn't seem directly related to this pull request. There's nothing preventing us from relaxing the state-space restrictions and skipping the refinement checks in those models.

[achamayou]

This doesn't seem directly related to this pull request. There's nothing preventing us from relaxing the state-space restrictions and skipping the refinement checks in those models.

Agreed, but there remains an open question about the value of the abstract model, and of the refinement. We are already severely constrained in the space we can check, adding the refinement makes that substantially worse. I am not sure what the utility of having it and not checking would be.

[lemmy]

This was merged despite the failure of two long-running jobs. The last successful checks were completed with commit bbd4a4f. The causes seems to be that StartTerm..MaxTermLimit+1 was changed to StartTerm..StartTerm + TermCount, which is not equivalent (+1).