search

tlaplus / CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
MIT License
273 stars 36 forks source link

How to write my operator which can be used in TLA+ #42

Closed Tsunaou closed 3 years ago

Tsunaou commented 3 years ago

In my work, I want to enumerate all possible event structure satisfying partial order. However, if we write TLA+ like this:

PartialOrderSubset(s) ==
    LET rels == SUBSET (s \X s)
    IN {po \in rels : IsStrictPartialOrder(po, s)}

We should enumerate all subsets, it's time costing. So I'd like to define my operator by Java and override it. I forked this repository and writes my implementation. See Update PartialOrderExt

And then, I built my CommunityModules-deps.jar and added it to TLC's or the Toolbox's TLA+ library path. I think it will call my implementation in PartialOrderSubset.java instead of the original definition in PartialOrderSubset.tla but it didn't work. Is there anything wrong of my settings?

lemmy commented 3 years ago

You have to load PartialOrderExt.java in TLCOverrides.java:

https://github.com/tlaplus/CommunityModules/blob/fa811ceba9c1170003f0dc8fd168b7d7fcfff9bd/modules/tlc2/overrides/TLCOverrides.java#L38-L47