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

*From*: Paulo Feodrippe <pfeodrippe@xxxxxxxxx>*Date*: Thu, 27 May 2021 01:26:14 -0300*Ironport-hdrordr*: A9a23:bRQQwKMJr+y0IsBcTtSjsMiBIKoaSvp037BN7SFMoH1uGfBw+PrBoB1273PJYXMqN03I5+rhBEDwexnhHPdOiOEs1PWZLWrbUQCTQb2Kg7GSoQEIYxeOk9Jg6Q==*References*: <040cba6c-4863-4212-b256-355a616fe549n@googlegroups.com> <CANDKcwCMd_8hoOxQR9oxgsVSRiPxOJg77NwuKvKWaV-382__Bg@mail.gmail.com> <cd111cbb-a3a4-46d8-b7a3-0b81f5c3d75bn@googlegroups.com> <CANDKcwDarzOo4hO8K7-R_3CVWxnx6jZ36FU_V5x=NX=yrhBEAQ@mail.gmail.com>

On Thu, May 27, 2021, 1:25 AM Paulo Feodrippe <pfeodrippe@xxxxxxxxx> wrote:

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.PauloOn Wed, May 26, 2021, 2:04 PM Ouyang Tsuna <tsunaouyang@xxxxxxxxx> wrote:

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.SincerelyOuyang--在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.

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/CANDKcwANT9tS5TE4KKSbxOYe-7Cuq2z2o_vB1F-KcqU-HAo-dQ%40mail.gmail.com.

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

**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

**Re: [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] How to write my operator which can be used in TLA+** - Next by Date:
**Re: [tlaplus] How to write my operator which can be used in TLA+** - 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):