Weak until
= Weak until
{title2=$\alpha\mathbin{\mathrm W}\beta$}
In <linear temporal logic>, $\alpha\mathbin{\mathrm W}\beta$ means $(\alpha\mathbin{\mathrm U}\beta)\lor G\alpha$. Thus it permits the left operand to hold forever without the right operand ever becoming true, unlike <strong until>.