Re: [tlaplus] [Edit 1 of 1] Nailing down how/where fariness is inherited by macros, procedures

On 3 Oct 2025, at 07:01, Shane Miller <gshanemiller6@xxxxxxxxx> wrote:

Please ignore the first message; I apologize for wasting bandwidth with sloppy late night typing.

Here is the corrected question consisting of 4 true/false questions clarifying how different TLA capabilities compose under fairness.

------------
True or false: a macro inherits its calling process fairness?

True: macros are inlined, the instructions of a macro are indistinguishable from instructions appearing in the body of the process or algorithm that uses the macro.

True or false: a procedure inherits its calling process fairness?

True: although the action corresponding to executing the procedure is not part of the action of the calling process, the PlusCal translator will generate a fairness condition for the instances of the procedure called from a process that has a fairness annotation.

Relatedly, per PlucCal documentation we can write:

(*--fair algorithm test
end algorithm;*)

Meaning all processes, procedures, and macros runs under weak fairness. True or false?

False: there will be a global fairness condition corresponding to the overall next-state relation, so execution will not stutter forever if some transition is enabled. However, this does not mean that there is a fairness condition for each of the processes appearing in the algorithm, which is what you are after if I understand correctly. Annotating an algorithm with a fairness condition is mostly relevant if there are no processes.

Other documentation (https://lamport.azurewebsites.net/tla/p-manual.pdf) p39 specifically says:

A process that is not a fair or fair+ process is called an unfair process and has no fairness assumptions on its actions. Adding + or - after a label in such a process has no effect.

Now, if I specify

(*--fair algorithm test ... end algorithm;*)

If I do this everything is running under weak fairness, and no process is decorated with fair or fair+. But by the PDF there is no way to make a label in a procedure strongly fair by adding '+' following a label. True or false?

True: you can try this out in the example by declaring the algorithm as fair and removing the fairness condition on the worker processes. You’ll see that you only get WF_vars(Next), and adding a "+" decoration for one of the process statements has no effect.

Being able to be cherry pick seems important. What I really need is strong fairness everywhere, however,

* writing (*--algorithm test ... end algorithm;*) omitting fair
* decorating my three processes with "fair+"
* poses a problem for LTL property checking: TLA tells me it's a tautology and stops with an error

That doesn’t happen with the attached module. It rather sounds like a malformed property?

Also note that there are certain fairness conditions that cannot be expressed in PlusCal, in particular for requiring fair non-deterministic choice. In those cases, you will have to write your fairness conditions in TLA+ directly.

Regards,

Stephan