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

*From*: Brandon Barker <brandon.barker@xxxxxxxxx>*Date*: Tue, 2 Aug 2022 15:11:54 -0700 (PDT)*References*: <c7ad139e-5c11-4df4-883b-e49c10f71d0fn@googlegroups.com> <a111a2e7-2561-4f59-beab-1e8dd15fb3fcn@googlegroups.com> <ac722f3f-a751-459d-b8cd-0d2a0c3ba7adn@googlegroups.com> <8eb90ad3-0e00-43db-a092-5f99938491bfn@googlegroups.com> <98c48137-da4c-4973-95a9-84b22a4ccb95n@googlegroups.com> <fe886986-ddbb-4f80-b69d-686b25de491bn@googlegroups.com>

Haha, sorry for the lack of context in that statement - I should have said "use for infinite sets in TLC", meaning I just need to read more and come to grips with the specific limitations of TLC. I appreciate that TLC does not support everything that might be expressed in TLA+, and other solvers or model checkers may have other feature sets.

On Tuesday, August 2, 2022 at 6:05:02 PM UTC-4 Leslie Lamport wrote:

I suppose in time I will see some use for infinite sets, since they exist in TLAYou might start by wondering why you've been using one since you were a young child.On Tuesday, August 2, 2022 at 7:11:20 AM UTC-7 brandon...@xxxxxxxxx wrote:Got it, makes sense - I suppose in time I will see some use for infinite sets, since they exist in TLA.On Tuesday, August 2, 2022 at 8:20:51 AM UTC-4 andrew...@xxxxxxxxx wrote:You have to override the value of Nat to be some set like 0 .. 100 or something.On Monday, August 1, 2022 at 4:35:03 PM UTC-4 brandon...@xxxxxxxxx wrote:Apologies, minor typo (though the issue is unrelated) - due to a refactor I should have had randomActiveCampaign[c], not randomActiveCampaign[c.id], in the last snippet. Like this:CreateActiveCampaign ==

/\ campaign' = \E c \in CAMPAIGN :

IF campaign[c.id] = {} THENOn Monday, August 1, 2022 at 4:31:59 PM UTC-4 Brandon Barker wrote:A little more context. Although those are the only places I'm referencing startDate directly, I am positing the existence of a campaign (of which campaign details is a member of) here:CreateActiveCampaign ==

/\ campaign' = \E c \in CAMPAIGN :

IF campaign[c.id] = {} THEN

[campaign EXCEPT ![c.id] = c /\ randomActiveCampaign[c.id]]

ELSE campaign[c.id]I'm not sure how TLC is handling this under the hood; in principle, I'm constraining the values of startDate to be finite by using randomActiveCampaign, but I'm not sure if that is how things are composing here.On Monday, August 1, 2022 at 4:14:59 PM UTC-4 Brandon Barker wrote:Hello,I'm having an issue running TLC on a model where, so far, I'm just "creating" a somewhat complex record, and not doing much else. Here is one component of the record:CAMPAIGN_DETAILS == [startDate: Nat

, endDate: Nat

]

\*

randomFutureCampaignDetails[details \in CAMPAIGN_DETAILS] ==

/\ details.startDate \in currentTime..monthsToSeconds[3]

/\ details.endDate \in (details.startDate+1)..monthsToSeconds[3]`randomFutureCampaignDetails` is used, indirectly, from `Next`. This results in the following error from TLCThe exception was a java.lang.RuntimeException

: Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],

but can't enumerate the value of the `startDate' field:

NatIt seems like I have bounded startDate to a finite set in:details.startDate \in currentTime..monthsToSeconds[3]Are there any suggestions for debugging this sort of error?

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/1bb3ceaa-4b3a-4fd6-830d-001a9ea7b622n%40googlegroups.com.

**References**:**[tlaplus] Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Andrew Helwer

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Leslie Lamport

- Prev by Date:
**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Next by Date:
**[tlaplus] Re: Question about the value of action expressions** - Previous by thread:
**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Next by thread:
**[tlaplus] Question about the value of action expressions** - Index(es):