Skip to content

Instantly share code, notes, and snippets.

@gterzian

gterzian/conv.md

Created January 11, 2026 12:39
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save gterzian/92ead35831fa6774fedfbccfc64ba057 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save gterzian/92ead35831fa6774fedfbccfc64ba057 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
conv.md

User: Ok I think we can solve this by removing pendingDbVersion, and instead replace it with the use of requested_version, and then set requested_version to dbVersion in abort

Agent: I have successfully refactored the TLA+ specification to remove pendingDbVersion and use requestedVersion instead. Here is a summary of the changes:

User: Add an oldDbVersion variable, set it from dbVersion at CreateUpgradeTransaction. Then, when aborting an upgrade, set requested_version to oldDbVersion, and also reset dbVersion

I have successfully implemented the oldDbVersion variable and the associated logic to handle database version rollbacks during upgrade aborts. I verified the changes using the SANY parser (which passed) and ran a TLC smoke test

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment