Realized over night, if my understanding of what has been said is correct then: In order for the small program to be terminating, when restricting to fair behaviors, you would not need to change how temporal logic was calculated only how either... or .... was translated.
With the extra label "oneMore" the state graph (attached) always branches with two arrows in the same step
s--oneMore-->h--upx-->n and s--oneMore-->g--upy-->m
but if the translation made the branch occur between different steps
s--upx-->h and s--upy-->m
then I think the tool would give the desired result. How easy it would be to change the translation I do not know.
But all of this is only relevant if other peoples intuition is that a fair execution of the small program would indeed terminate.