DistCompiler / pgo

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

Support TLC module `ToString` Operator #229

Closed shayanh closed 2 years ago

shayanh commented 2 years ago

TLC module has a ToString operator that converts an input to string. Currently, it's not possible to use this in an MPCal spec.

fhackett commented 2 years ago

Can you include a link to where this operator is documented / specified? I'd like to attach it to the correct import, etc...

shayanh commented 2 years ago

https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLC.tla#L121