[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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 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?

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?

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

--
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/751f3829-f672-42a7-a686-605679a8d1fen%40googlegroups.com.