1 - Can we have a macro that returns a macro? I suppose no. I don't understand this, because macros don't "return" anything.
I wanted a macro like: Macro(a,b) = Test(x) == x.out = a /\ x.in = b That way I could write later: SelectSeq(u, Macro(1,2))
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+.
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_.
Best regards, Stephan
|