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

Re: [tlaplus] Macros with PlusCal and Toolbox


bug reports are welcome, but they should contain enough information to be reproducible. Could you please include a minimal example exhibiting the problem?

The attached module contains a PlusCal algorithm with several definitions and macros, and it is accepted by the Toolbox and the PlusCal translator.


Attachment: LamportMutex.tla
Description: Binary data

On 18 Dec 2014, at 18:34, fl <freder...@xxxxxxxxxxx> wrote:

It is maybe a bug
I think that Toolbox doesn't want several PlusCal macros in an algorithm.
But the specification of PlusCal says it is possible.

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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.