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

[Ouyang Tsuna <tsunaouyang@xxxxxxxxx>]

Thanks for your reply. I have solve the problem. With the help of Java, things become more convenient.

But unfortunately, I encountered some difficulties again, and I don’t know if there is a solution. Could you give me some advice?

As I mentioned before, I want to enumerate all possible event structure satisfying partial order.

But the raw method by enumerating all subsets and judging them is of a great time complexity. 

So Implementation for the partial order part of paper A Verified Algorithm Enumerating Event Structures. And the GitHub repository is at Event-Structure-Enumerator.

All the possible partial order is stored in POFile and I write a Java version which is suitable for TLA+ in PartialOrderExt.java.

Everything seemed to be going well, however, something unexpected happened. 

After reading the source code of TLA, I found The bound for the cardinality of a set is 1000000 in Search · Attempted to construct a set with too many elements (github.com).

What bad news !  I understand that this design makes a certain sense, but a question raises that as follows.

Suppose a set s = {1,2,3,4,5,6,7,8} and we calculate subset SUBSET (s \X s), what is the behavior of TLA+? Out of bound too? Or there is an iterator-like operation? 

I know my question is a bit strange. But if you are interested, looking forward to your early relpy.

Sincerely

Ouyang

在2021年5月18日星期二 UTC+8 下午8:57:09<pfeod...@xxxxxxxxx> 写道：

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

-- 
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/cd111cbb-a3a4-46d8-b7a3-0b81f5c3d75bn%40googlegroups.com.