Repository navigation
Support TLA+ bags #8
Description
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
Activity
minhnhdo commentedon Jan 17, 2018
Can you also post the TLA+ bags doc?
Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/32/support-tla-bags#comment-37468475
minhnhdo commentedon Jan 17, 2018
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 commentedon Jan 17, 2018
Bags (and records) should be implemented in Go using maps.
Original comment: https://bitbucket.org/whiteoutblackout/pgo/issues/32/support-tla-bags#comment-39332688
fhackett commentedon Jun 11, 2018
We now have a framework for implementing built-in modules. See
pgo.trans.intermediate.TLABuiltinsfor details.