Search code examples
tla+

TLA+ translated result parse failed

my TLA+ spec write by PlusCalc compile to TLA+ succeed, but parse failed:

THE SPEC: https://justpaste.it/39pru

where is the error location in PlusCalc?

Thanks!

Solution

  • See answer on the semi-official Google Group: https://groups.google.com/forum/#!msg/tlaplus/x3G2DC91fpc/r-_VpqjZBQAJ

    (Mirror: http://discuss.tlapl.us/msg03251.html)