A more straightforward translation might be:
...
b == \* /\ pc = "b" The definitions of b_BRANCH* make this conjunct redundant.
/\ \/ b__BRANCH1
\/ b__BRANCH2
But this doesn't solve the problem. The desired fairness condition is
fairness of both b_BRANCH1 and b_BRANCH2, and how is that supposed to
be indicated in the PlusCal code?
Before we waste any more time discussing this, everyone should realize
that it is just one of many kinds of fairness conditions one might
want that aren't expressible in PlusCal. For example in
w : with (n \in 1..42) { x := n }
one might want the fairness condition
\A n \in 1..42 : SF_...(pc = "w" /\ x' = n)
Other specification methods that have been proposed write a spec with
a next-state relation as the disjunction of a particular set of
(named) actions. Some of them can specify liveness with fairness
conditions on those particular actions. But TLA+ is more expressive
than any other formalism I know of because it isn't limited to
fairness of those particular named actions. I know no way to get that
expressiveness when using PlusCal other than by defining a spec that
is the conjunction of the formula Spec generated by the PlusCal
translation with additional fairness formulas.
Perhaps someone else can find a way to do this that I haven't been
able to think of in the last 14 years. But please realize the scope
and difficulty of the problem and let's not clutter the group with ad
hoc proposals that may or may not work in one particular example.
Leslie