Another question about Next and Until

[n s]

Hello everyone, I'm sure this topic has come up a few times, but my intent here is not to question why these two operators are missing from TLA but how best to represent their meaning (preferably in a form that's TLC checkable). Suppose I have the following spec

Init == ...

Next == Input \/ Process \/ Output

Spec == Init /\ [Next]_vars /\ WF_vars(Next)

where Input, Process, and Output definitions aren't shown. and I wish to say that an Input is always followed by an Output before the next Input (and v.v. for Output and Input). I can write this requirement fairly concisely in LTL

[] (Input -> X(~Input U Output))                         [by using WeakUntil, the WF reqt can be eliminated]

What's the best way to capture this in TLA+? The only way I can think of is to explicitly incorporate this property into the model

VARS round, old_round

InitV2 == round=0 /\ old_round=0 /\ Init

InputV2 == round=old_round /\ Input /\ round'=1-round

OutputV2 == Output /\ old_round'=1-old_round

with InitV2, InputV2 OutputV2 in place of their originals in the spec. But his feels somewhat like an "implementation" to me. It also doesn't leave me any way to  check that I actually modeled it correctly. Any suggestions on how to improve on this?

thanks

[n s]

So I just realized that there is a property that I can verify, namely that [](ENABLED(Input) -> round=old_round) but nevertheless my main question still stands