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
174 stars 14 forks source link

Generated PlusCal code has errors #147

Closed shayanh closed 3 years ago

shayanh commented 3 years ago

MPCal program with compiled PlusCal code: https://gist.github.com/shayanh/4f7ed959d69c0c2720592c8bc5c153db

If you try to compiled above program into TLA+, you'll get the following error: image

fhackett commented 3 years ago

That's really interesting. Seems there's an edge case around mapping macros performing a many-to-one substitution, e.g: two archetype params are actually refs to the same state variable, mapped differently.

They have different names inside the archetype, and, but, after macros are expanded, the remaining references have the same name and refer to the same thing. Maybe the scoping isn't updated properly...