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

*From*: Ouyang Tsuna <tsunaouyang@xxxxxxxxx>*Date*: Wed, 26 May 2021 23:56:14 -0700 (PDT)*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> <CANDKcwANT9tS5TE4KKSbxOYe-7Cuq2z2o_vB1F-KcqU-HAo-dQ@mail.gmail.com>

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.

在2021年5月27日星期四 UTC+8 下午12:26:25<pfeod...@xxxxxxxxx> 写道：

On Thu, May 27, 2021, 1:25 AM Paulo Feodrippe <pfeod...@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 <tsuna...@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+u...@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/1b4e8eed-7818-4dbf-8ddf-c398538d7818n%40googlegroups.com.

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

**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:
**[tlaplus] Doing arithmetic with current state value and next state value of a variable in TLA+** - Previous by thread:
**Re: [tlaplus] How to write my operator which can be used in TLA+** - Next by thread:
**[tlaplus] REPL enhancements** - Index(es):