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

[Brandon Barker <brandon.barker@xxxxxxxxx>]

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/c7ad139e-5c11-4df4-883b-e49c10f71d0fn%40googlegroups.com.