pgo icon indicating copy to clipboard operation
pgo copied to clipboard

Published 20 hours ago • verified publisher icon DistCompiler

Support TLA+ bags

Open minhnhdo opened this issue 7 years ago • 4 comments

TLA+ has a "bag" type which is better known as a multiset. We need to support bags and their corresponding operators and functions. A bare-bones Go multiset library is available at https://github.com/soniakeys/multiset.

Original issue: https://bitbucket.org/whiteoutblackout/pgo/issues/32/support-tla-bags

minhnhdo avatar Jan 17 '18 06:01 minhnhdo

Can you also post the TLA+ bags doc?

Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/32/support-tla-bags#comment-37468475

minhnhdo avatar Jan 17 '18 06:01 minhnhdo

Bag operations are listed at http://lamport.azurewebsites.net/tla/summary-standalone.pdf. The full specification of a bag is in the TLA+ book http://lamport.azurewebsites.net/tla/book-02-08-08.pdf (chapter 18).

Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/32/support-tla-bags#comment-37468551

minhnhdo avatar Jan 17 '18 06:01 minhnhdo

Bags (and records) should be implemented in Go using maps.

Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/32/support-tla-bags#comment-39332688

minhnhdo avatar Jan 17 '18 06:01 minhnhdo

We now have a framework for implementing built-in modules. See pgo.trans.intermediate.TLABuiltins for details.

fhackett avatar Jun 11 '18 12:06 fhackett