[tlaplus] Nailing down how/where fariness is inherited by macros, procedures

[Shane Miller <gshanemiller6@xxxxxxxxx>]

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;*)

And everything meaning processes, procedures, and macros runs under weak fairness.

Other hand 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;*)

By the second point there is no way to make a label in a procedure weakly fair by adding '+' following a label. Is that true or false? 

I'm trying to get an overall weakly fair specification except for a few places in processes or procedures where I want strongly fair by appending '+' to a label.

Regards

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/955f3a4e-1744-4e10-9a75-6a9f5d7bfbfan%40googlegroups.com.