# [tlaplus] How to write my operator which can be used in TLA+

• From: Ouyang Tsuna <tsunaouyang@xxxxxxxxx>
• Date: Tue, 18 May 2021 05:16:31 -0700 (PDT)
• Ironport-hdrordr: A9a23:TTBQrKkZhnQZboYDWel/eLLWCFDpDfLY3DAbv31ZSRFFG/Fw9vre4cjzsCWftN9/YgBGpTntAtjnfZsznaQFlbX4E9+ZLXzbUSiTXfFfBbKL+UyTJ8SGzJ8r6U4CSdkFNDVEZmIK/PoSnjPIa+rIm+P3jpxA7N22pxwdLnAOV0gH1XYHNu+1KCFLrWJ9dOEE/fSnl7N6T/vJQxQqhweAaUXtndKvmzV6/6iWEiLuyyRI1OF/5gnYlIIS2iL4r3VuNw9y/Q==

In my work, I want to enumerate all possible event structure satisfying partial order.
However, if we write TLA+ like this:
TLA+
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?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.