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

77 views
Skip to first unread message

Ouyang Tsuna

unread,
May 18, 2021, 8:33:49 AM5/18/21
to tlaplus
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?

Paulo Feodrippe

unread,
May 18, 2021, 8:57:09 AM5/18/21
to tla...@googlegroups.com
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

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

Ouyang Tsuna

unread,
May 26, 2021, 1:04:43 PM5/26/21
to tlaplus

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. 

TLA+ Error.png

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

Paulo Feodrippe

unread,
May 27, 2021, 12:26:07 AM5/27/21
to tla...@googlegroups.com
Hi Tsuna,

Glad that it worked for you :)

If the main issue is just the size of the enumeration, try setting the "-maxSetSize" parameter. 

Do you really need a set of this size?

Let me know if it works (or not) for you.

Paulo

Paulo Feodrippe

unread,
May 27, 2021, 12:26:25 AM5/27/21
to tla...@googlegroups.com

Ouyang Tsuna

unread,
May 27, 2021, 2:56:14 AM5/27/21
to tlaplus

Oh thanks! It really helps. Now the only issue is Java heap out of memory, maybe I should decrease the scale of my checking or find a new way to do this work. Thanks again.
Reply all
Reply to author
Forward
0 new messages