Re: [tlaplus] Pcal, procedures and tests

[fl <freder...@xxxxxxxxxxx>]

 

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.

 

http://research.microsoft.com/en-us/um/people/lamport/tla/summary.pdf

 

--

FL