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

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

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:

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:

    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 TLC

The 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:

It 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/a111a2e7-2561-4f59-beab-1e8dd15fb3fcn%40googlegroups.com.