[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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?

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.