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 or false: a procedure inherits its calling process fairness?
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?
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?
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
Regards