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)