What is the plan for Distributed PlusCal?

[Chris Ortiz]

Hi,

Good morning. I am wondering what is the plan to have Distributed PlusCal option (-distpcal).

https://members.loria.fr/SMerz/papers/2023-ifm.pdf

https://github.com/DistributedPlusCal/DistributedPlusCal

Thanks and best regards,

Chris (Zitro)

[Andrew Helwer]

No plan currently. The route at this point would be to submit it to the specification language committee along with a plan for acquiring development resources for its implementation.

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/896821d8-3855-4280-ba9f-a668ba940324n%40googlegroups.com.

[Stephan Merz]

Thank you for the interest in Distributed PlusCal! It motivated us to take it up again and make the extra push so that it could be made available. Our current plan is to make that happen and to publish a beta version in the first quarter of 2026, hopefully as an optional feature in the PlusCal translator.

Stephan

[Chris Ortiz]

Hi Stephan,

Yes I am very interested. In fact, I am working on a side project with our univerisity partner having help from 4 students. We hope to deliver the P2P2P project (PlusCal to PlantUML to PDF) around end of April'26 that will utilize the AST.tla (via -writeAST) of PlusCal file to generate UML via PlantUML (Sequence for trace scenario, Activity for behavior Specs, and State Diagram for state transition scenarios). Currently we are focusing on the Activity Diagram New Syntax (https://plantuml.com/activity-diagram-beta). Where labels in PlusCal, that are actions in TLA+, will be the activity component in that diagram that can fork (due non-determinism) and join at some point. Where the PlusCal global variables assignments as TLA+ initialization, will be the Start component in that diagram. Where processes in PlusCal can be partition in the diagram, or subprocesses in Distributed PlusCal can be Swimlane in that diagram, and so on.

We understand the purpose of PlusCal in relation to TLA+ and we believe the Distributed PlusCal is an attempt to add more modern programming context to it. As an example, there is a stereotype syntax in the Activity Diagram that represent <<input>> and <<output>> form which can be used as send and receive context of Distributed PlusCal. Currently what we are doing is that we are inventing a non-standard PlusCal annotation convention (\*<p2p2p>) that we can parse from the raw PlusCal (non-AST) to denote those stereotype context. All we are doing are external application for ourselves (we challenge ourselves on using Rust) and not modifying any of the TLA+ toolset but rather leverage on their current capabilities.

We understand the importance of formal specification but most team-member I dealt with in our company are not savvy with either math-TLA+ nor with pseudo-code-PlusCal. Most are visual learners when we discuss design and I believe presenting it with a standard diagrams like UML can help. I also believe that little conveniences such as autogenerating diagram can encourage more to learn the source, which is to learn PlusCal, then in turn learn TLA+.

There are more things about our P2P2P project but this summary I hope give more motivation to your extra push.

I think for what it is right now for Distributed PlusCal is very useful for which it tried to be as much less changes as possible so it does not break compatibility with PlusCal. During few observation I have with the -writeAST option, I found out that "chan" and "threads" field names are added that we can key off our AST parser (in fact we can INSTANCE or EXTEND AST and access the records in TLA+/PlusCal). BUT, I noticed that in the body's stmts of the AST the "chan" becomes a value of the "var" field to leverage on existing PlusCal functionality. ALSO, there are no new fields that the send action (Bag assignments or update) which indicated that it came from the send context of Distributed PlusCal or came from explicit assignment of ordinary PlusCal. Maybe adding new fields explicitly for those Distributed PlusCal context add more complication to existing PlusCal, I am not sure if that is a good idea or not....but it would be really nice to see that those news construct in Distributed PlusCal has their own explicit AST fields (or their own "type", maybe?).

Thanks and best regards,

Chris (Zitro)

[Filip Schmole]

This is exactly what I've been looking for! Reviewing the paper from Stephan et al, the additions to PlusCal are exactly what's missing for my purposes. Also, visualizing the flows is an incredibly powerful tool for model development and ultimately, generating documentation. I was not aware of this effort before seeing this forum and searching for "plantUML", so last week, I contributed an enhancement to the tlaplus-vscode extension that generates plantUML sequence diagram code from TLC traces. Could that be useful for your P2P2P project? The coolest thing about it (in my opinion) is the algorithmic extraction of fork/join threads, listed in the code as "concurrent chains". 

I do have one fundamental question: It sounds like P2P2P intends to generate plantUML from the PlusCal code itself (model parsing approach). Is that correct? That has the benefit of running faster, i.e., not requiring model simulation, but it might risk being less accurate. Chris, have you given thought to a post-extraction vs. model-parsing approach?

Either way, I'm so glad to find people interested in the same goal!

Filip

[Chris Ortiz]

Hi Filip,

Yes I've been working with this with NAU 4 Students (P2P2P: https://www.ceias.nau.edu/cs/CS_Capstone/Projects/F25/F25_teams.html). I actually noticed your commits days ago and I jokingly told the students that someone is beating them regarding PlantUML Sequence Diagram :) But there are difference in approaches. Before I saw your commits I was discussing with the students that for Sequence it has to be derived from a trace interestingly sampled from the spec showing certain condition or property (like the DieHard example) so unfortunately the way we will generate that trace is actually another NAU project that a different team is handling (AI-ACETONE: https://www.ceias.nau.edu/cs/CS_Capstone/Projects/S26/S26_Teams.html). If you like we can collaborate, and I think that is best for the TLA+ community. We can together share learning and methods but remember that these are NAU Capstone projects so their implementation will differ than yours. These are students who are TLA+ first-timer, myself included, so we don't like to mess up directly the tlaplus github repos.

Yes, for the Activity Diagram it is derived from PlusCal but from it's AST which we will only generate if it pass TLC model-checker. Remember we designed these NAU projects with intent to benefit Sandisk. You can find more details and other TLA+ projects in the 2 links I provided above. We can even add you in our private repo if necessary.

I personally believe that fun projects and working with experienced folks related to TLA+ will teach students critical-thinking system skills that can give them edge when they graduate to face AI-based job market.

Kindly, let me know if you like to join us on Teams meeting. I have a weekly meeting with the students every Wednesday 10:30AM - 11:30AM Pacific Time.

Thanks,

Chris