Dear Yuri,
Chris Newcombe once aptly called PlusCal the gateway drug to TLA+ ... it is a thin layer on top of TLA+ that has a more familiar syntax for programmers. Personally, I find TLA+ better suited for modeling high-level distributed algorithms. PlusCal is a step closer to (sequential or parallel) programs, and if your task is to model executions at that level, then you'll probably find that you have to worry about these "implementation details".
Best regards, Stephan
Thank you Stephan.
I always thought the beauty of TLA+ is its use of math, which results in concise and easy to understand specs that can also be verified. There are no “implementation details” constructs such as loops, artificial stacks to manage (non-TLA) function calls, program counters, etc. PlusCal brings these details back and makes them part of the spec (translated code). If somebody is fine with TLA+ as it is, do they need PlusCal? Is there anything so important that can be expressed in PlusCal but not in TLA+?
Thank you again, Yuri
--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|