Skip to content

Feedback on WF and SF syntax #41

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Feedback on WF and SF syntax #41

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3b3c117
Feedback on WF and SF syntax
alxiong Oct 20, 2022
56264ba
small update
alxiong Nov 28, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 12 additions & 3 deletions docs/core/tla.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 <strong_fairness_spec>`::

Spec == /\ Init /\ [][Next]_vars
/\ \A self \in Threads : SF_vars(thread(self))
/\ \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 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:

Expand Down