I am reading an article called The temporal semantics of concurrent programs .
On page $9$, there is a small section (numbered as $2$) called "clean behavior".
I think that there is a problem with this part, what does Pnueli meant by "Let $\lambda_i$ be the leagality condition for the statement departing from $m^i$" ?
I have marked the word "the" in bold since, as I see it, there can be more than one edge departing from $m^i$, an example can be seen on page $11$, at the beginning of part $5$.
Did I missunderstood something , or is there actually a mistake in the article by not addressing the fact that there can be more than one statement that can be exectuded after $m^i$, and that this expression for clean behavior need to be corrected accordingly ?