search

DistCompiler / pgo

PGo is a source to source compiler from Modular PlusCal specs into Go programs.
https://distcompiler.github.io/
Apache License 2.0
172 stars 13 forks source link

Add more TLA+ operators if necessary #3

Closed minhnhdo closed 5 years ago

minhnhdo commented 6 years ago

PlusCal may support some TLA+ operations that may not be found in the TLAExprParser token dictionary. If these exist, we need to add them to the dictionary and handle them properly.

Original issue: https://bitbucket.org/whiteoutblackout/pgo/issues/11/add-more-tla-operators-if-necessary

minhnhdo commented 6 years ago

The most important operators that are not parsed (properly) are the Cartesian product operator \X, the IF...THEN...ELSE expression and CASE construct, and the DOMAIN operator. It is also possible to use multiple |-> operators in one map declaration, like in ["a" |-> 1, "b" |-> 2, "c" |-> 3].

Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/11/add-more-tla-operators-if-necessary#comment-39332715

rmascarenhas commented 5 years ago

Closing this since the classes mentioned no longer exist (and we now support IF and CASE expressions).