I do not understand what you intend but this must be wrong. You can only pass expressions as arguments to operators (such as SelectSeq), whereas you seem to intend your Macro to produce a definition. Definitions are not expressions in TLA+.
Well I will check but I'm pretty sure you can pass a macro to SelectSeq. Secondly, I do not understand the example because SelectSeq is a ternary operator, and the second and third argument are expected to be integers whereas the right-hand side of your Test operator is a Boolean _expression_.
I think you are confusing SelectSeq and SubSeq. SelectSeq is binary and takes a macro.
My bad, excuse me. You want to write the following:
Test(a,b,x) == x.out = a /\ x.in = b
and then use it as in
SelectSeq(u, LAMBDA x : Test(1,2,x))
It might be tempting to write
Test(a,b) == LAMBDA x : ... SelectSeq(u, Test(1,2))
but the TLA+ syntax does not allow you to do that (see Section 16.4 of the Hyperbook).
Regards, Stephan |