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