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?