I am teaching myself logic in concurrent programming with Principles of concurrent and distributed programming, from Ben-Ari. I have to because I study Ada, in a manual from the guy, and the chapter on concurrency requires working the first book for an "introduction" to concurrency.

I just started the chapter on temporal linear logic. But Ben-Ari is so goddamn terse, it's infuriating when you don't have a teacher at home. I consider this a pedagogic failure.

So I can't read the formula below:

tryP => non-csQ until csQ Ｗ non-csQ Ｗ csP

We deal with two processes, P and Q, cs being the critical section, and try its precondition instruction. I know the implication operator, and the W or "weak until" operator. try means "try to enter critical section".

And I know (from the book) that it expresses the need for fairness, meaning a process can only enter the CS once before the other does.

... But for the life of me, I can't read it ! How do we even read when temporal operators are stacked like this ? I assume associativity goes left to right like addition, but how do I make sense of it?

I don't understand his explanation, my brain goes mush:

We want the formula to be true at time 1 when tryP is true. Between 1 and 4, i csQ is true, so we have to check the truth of (csQ) W (¬csQ) W (csP) at time 4. Now csQ is true from time 4 to time 6, so it remains to check if (¬csQ) W (csP) is true at time 6. And, in fact, ¬csQ remains true until csP becomes true at time 8.

So, if you could share some light on how to tackle this...