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

Hi Tsuna,

You need to add the class to https://github.com/Tsunaou/CommunityModules/blob/master/modules/tlc2/overrides/TLCOverrides.java#L38 (and in the other return in the same file).

TLC looks primarily for this class (there is also another way to configure it) for operators overriding.

Let me know the result o/

Paulo

On Tue, May 18, 2021, 9:33 AM Ouyang Tsuna <tsunaouyang@xxxxxxxxx> wrote:

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/040cba6c-4863-4212-b256-355a616fe549n%40googlegroups.com.