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

Re: [tlaplus] Pcal, procedures and tests

On 10 Apr 2015, at 16:18, fl <freder...@xxxxxxxxxxx> wrote:

Hi Stephan,
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).