Wrote January 2025 development update post

[ahelwer]

Per @lemmy's suggestion from last month, to try to make this more inclusive & collaborative I'll endeavor to get the first draft published before the monthly community meeting, which will provide an opportunity to gather feedback and record missed contributions. We can target publication on the 15th of each month; I'll also tag people here so they can provide a summary in their own words.

This is intended to cover work that happened during the month of December (modulo a few days on either end) so if it was something more within the past week it can go in the next monthly update.

[ahelwer]

Some people I am seeking feedback/summaries from:

• @will62794 would you like to summarize your work on tla-web? I see the last month had a lot of activity.
• @fhackett what do you think a nice blurb would be about your string deserialization work?
• @FedericoPonzi and @hwayne you both had contributions to the VS Code extension last month, would you like to summarize them?
• @kape1395 are you happy with this summary of your TLAPM work the past month?
• @lemmy gave you your own section, what would you like your summary to be?

[fhackett]

@ahelwer here's my attempt. I just guessed at the format, so feel free to edit / request a different style.

In the emerging use case of validating implementation logging data with TLC, there is a need to read large amounts of structured data efficiently for use in model checking. A recommended option is the binary format TLC uses to store states, for which the community modules expose read/write routines (IOSerialize and IODeserialize respectively, in IOUtils). @fhackett's work addresses teething issues in the types of string value that can be read by TLC in this way, removing a limitation that strings have to come from the same TLC runtime (e.g., generated during model checking, present in the TLA+ files being evaluated), and proposing an extension from the current ASCII format to UTF-8.

[kape1395]

The part describing my progress is ok. If you need more links to PR's, they are here, but I don't know if all those details are needed in the report.:

• Resolved the review comments in the updated_enabled_cdot, made it working with the LSP again.
  • Merge updated_enabled_cdot. tlapm#148
  • Make the LSP independent of level assignment. tlapm#186
• Found the quantifier related level calculation problem and fixed it.
  • Incorrect handling of formula levels? tlapm#188
  • Levels of the quantifier bounds were effectively ignored. tlapm#189
• Fixed a bug related to USE and INSTANCE.
  • Fix instantiation of a module containing USE. tlapm#191
  • The following problem still remains.

    Error: Operator "EnabledWrapper" not found
    tlapm ending abnormally with Failure("Expr.Anon: 4")
    

• Fixed LSP to create proof steps for USE statements that generate proof obligations because of listed facts, PR: LSP: Create proof step markers for USE statements involving facts. tlapm#193
• Fixed LSP to take max instead of latest status for an obligation, PR: LSP: Use maximum obligation status instead of latest. tlapm#194

[ahelwer]

Okay @fhackett and @kape1395 I wrote these up, take a look.

[will62794]

@ahelwer No concrete updates on my end.

[lemmy]

The detailed technical updates can be found at https://github.com/lemmy?tab=overview&from=2024-12-01&to=2024-12-31. On a higher level, recent work includes the TLA+ debugger, diagnosing fingerprint duplication issues that arise during long-running model checking, and exploring liveness checking for monotonic systems.

[ahelwer]

This is good to be published. @lemmy @muenchnerkindl

[muenchnerkindl]

Thanks @ahelwer for the January newsletter!