Open ahelwer opened 6 months ago
Picked this up from a new submodule added to the tlaplus/examples repo:
https://github.com/tlaplus/azure-cosmos-tla/blob/4b8785a36ed16faa2cd1bd78b89e224d71711ee3/scenario1/swscop.tla#L34
Both pcal.trans and tla2sany.SANY accept this syntax. At first glance I think the grammar wants there to be curly braces, but they're elided here.
pcal.trans
tla2sany.SANY
@susliko would you be able to take a look when you have time?
Tried simple fix but ran into a whole bunch of parser ambiguity issues. Work currently lives in pcal-no-delimiter branch.
pcal-no-delimiter
Picked this up from a new submodule added to the tlaplus/examples repo:
https://github.com/tlaplus/azure-cosmos-tla/blob/4b8785a36ed16faa2cd1bd78b89e224d71711ee3/scenario1/swscop.tla#L34
Both
pcal.trans
andtla2sany.SANY
accept this syntax. At first glance I think the grammar wants there to be curly braces, but they're elided here.@susliko would you be able to take a look when you have time?