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

[Brandon Barker <brandon.barker@xxxxxxxxx>]

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

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.