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

*From*: Ouyang Tsuna <tsunaouyang@xxxxxxxxx>*Date*: Wed, 26 May 2021 10:04:43 -0700 (PDT)*Ironport-hdrordr*: A9a23:1w05NaHwYkNr9e6ApLqEEMeALOsnbusQ8zAXPiBKOH9om6uj5qSTdZUgpHrJYVMqNk3I9urwXpVoLUmsl6Kdn7NhRYtKLTOW31dARbsKheCCowEIcBeOj9K1u50QCJSWcOeAd2RSvIL/6Am8V9khxcSK663Av43j5kYoVw5wL6Vp7wJ4DQjzKCBLbTgDH5UjUICE7s4vnVWdUEVSdMuhQmMdV+zZr8DKk5yOW3I7OyI=*References*: <040cba6c-4863-4212-b256-355a616fe549n@googlegroups.com> <CANDKcwCMd_8hoOxQR9oxgsVSRiPxOJg77NwuKvKWaV-382__Bg@mail.gmail.com>

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/PauloOn 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 PartialOrderExtAnd 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.

**Follow-Ups**:**Re: [tlaplus] How to write my operator which can be used in TLA+***From:*Paulo Feodrippe

**References**:**[tlaplus] How to write my operator which can be used in TLA+***From:*Ouyang Tsuna

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

- Prev by Date:
**Re: [tlaplus] About machine-closed Fairness Property** - Next by Date:
**[tlaplus] Curious: stuttering vs recursive** - Previous by thread:
**Re: [tlaplus] How to write my operator which can be used in TLA+** - Next by thread:
**Re: [tlaplus] How to write my operator which can be used in TLA+** - Index(es):