 Weak until

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