Differences

This shows you the differences between two versions of the page.

--- learning:pluscal [2024/09/28 15:58] – created - external edit 127.0.0.1
+++ learning:pluscal [2025/07/26 17:56] (current) – [Learning Pluscal] lorinh
@@ Line 1: / Line 1: @@
-====== Learning Pluscal ======
+====== Learning PlusCal ======
 PlusCal is an algorithm language—a language for writing and debugging algorithms. It is especially good for algorithms to be implemented with multi-threaded code. Instead of being compiled into code, a PlusCal algorithm is translated into a TLA+ specification. An algorithm written in PlusCal is debugged using the TLA+ tools—mainly the TLC model checker. Correctness of the algorithm can also be proved with the TLAPS proof system, but that requires a lot of hard work and is seldom done.
-The easiest way to learn pluscal, is to read the Pluscal tutorial by Lamport. Free, and readable online; it can be found here: https:%%//%%lamport.azurewebsites.net/tla/tutorial/contents.html
+===== External resources =====
+  * [[https://lamport.azurewebsites.net/tla/tutorial/contents.html|The PlusCal Tutorial]] by Leslie Lamport
+  * [[https://learntla.com/|Learn TLA+]] by Hillel Wayne, which starts off by teaching PlusCal
 ===== C-style vs P-Style =====
-Pluscal comes into two flavors: C-Style and P-Style. For a more complete overview of Pluscal, there is a manual available for each style: [[https://lamport.azurewebsites.net/tla/c-manual.pdf|c-manual.pdf]], [[https://lamport.azurewebsites.net/tla/p-manual.pdf|p-style.pdf]].
+PlusCal comes into two flavors: C-Style and P-Style. For a more complete overview of PlusCal, there is a manual available for each style: [[https://lamport.azurewebsites.net/tla/c-manual.pdf|c-manual.pdf]], [[https://lamport.azurewebsites.net/tla/p-manual.pdf|p-style.pdf]].
 To have a taste of each style: