[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Another question about Next and Until

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

On Friday, September 1, 2023 at 1:19:45 PM UTC-7 n s wrote:
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?


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/093543c5-7653-4a16-8100-740535bd230fn%40googlegroups.com.