From 3b3c117677f7315985644c4dd6d8aa6083e15640 Mon Sep 17 00:00:00 2001 From: Alex Xiong Date: Thu, 20 Oct 2022 22:53:44 +0800 Subject: [PATCH 1/2] Feedback on WF and SF syntax - Consistent subscript on `SF` and `WF` - Troubleshooting hints for accidentally redefining them in TLA+ (which I tried to do while learning) --- docs/core/tla.rst | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/docs/core/tla.rst b/docs/core/tla.rst index 89fc408..f7ecf72 100644 --- a/docs/core/tla.rst +++ b/docs/core/tla.rst @@ -356,20 +356,29 @@ Fairness is formally defined in TLA+ as follows:: In English: -* ``WF_x(A)``: If it is *eventually always* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v). -* ``SF_vars(A)``: If it is *always eventually* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v). +* ``WF_v(A)``: If it is *eventually always* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v). +* ``SF_v(A)``: If it is *always eventually* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v). Fairness constraints are appended to the definition of ``Spec``. You can see this in the translation of our prior `strong fairness example `:: - Spec == /\ Init /\ [][Next]_vars - /\ \A self \in Threads : SF_vars(thread(self)) + Spec == /\ Init /\ [][Next]_v + /\ \A self \in Threads : SF_v(thread(self)) (Remember, ``Spec`` defines what *counts as a valid trace*. Fairness is an additional constraint, ruling out things like infinite stutters.) Notice that by writing ``\A self: SF_vars(self)``, we're effectively making every thread fair. If we instead wrote ``\E``, we'd be saying that at least one thread is fair, but the rest may be unfair. If both those conditions are syntactically intuitive to you, I'd say you fully understand how pure TLA+ works. +.. troubleshooting:: + If you get + + Encountered "WF_" at line X, column Y + or + Encountered "SF_" at line X, column Y + + It's because you try to redefine operator ``WF_var(A)`` or ``SF_var(A)`` whereas they are already taken keywords. + Also make sure `VARIABLES var` is declared before using ``SF/WF_var()``. .. _fairness_status_example: From 56264ba4293b58f704b5713250420a80b63bd362 Mon Sep 17 00:00:00 2001 From: Alex Xiong Date: Mon, 28 Nov 2022 11:20:25 +0800 Subject: [PATCH 2/2] small update --- docs/core/tla.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/core/tla.rst b/docs/core/tla.rst index f7ecf72..1c414a3 100644 --- a/docs/core/tla.rst +++ b/docs/core/tla.rst @@ -362,7 +362,7 @@ In English: Fairness constraints are appended to the definition of ``Spec``. You can see this in the translation of our prior `strong fairness example `:: - Spec == /\ Init /\ [][Next]_v + Spec == /\ Init /\ [][Next]_vars /\ \A self \in Threads : SF_v(thread(self)) (Remember, ``Spec`` defines what *counts as a valid trace*. Fairness is an additional constraint, ruling out things like infinite stutters.) @@ -377,7 +377,7 @@ Notice that by writing ``\A self: SF_vars(self)``, we're effectively making ever or Encountered "SF_" at line X, column Y - It's because you try to redefine operator ``WF_var(A)`` or ``SF_var(A)`` whereas they are already taken keywords. + It's because you try to redefine operators (or variables) that start with ``WF_`` or ``SF_`` whereas they are already taken keywords. Also make sure `VARIABLES var` is declared before using ``SF/WF_var()``. .. _fairness_status_example: