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

• From: Brandon Barker <brandon.barker@xxxxxxxxx>
• Date: Tue, 2 Aug 2022 15:11:54 -0700 (PDT)
• Ironport-data: A9a23:pSBv7K5q54Aggj/x944zLwxRtKLCchMFZxGqfqrLsTDasY5as4F+v mcWCmnTPKqDamrxft5waoW380xTsJOExoIxTlZvqC41Zn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOK6UoYoAwgpLeNeYH5JZSlLxqho2eaEvfDjW1nX4 YOq+ZWDULOY82cc3lw8u/rrRCxH56yaVAMw5jTSstgW1LN2vyB94KM3fcldHVOgKmVnNrLSq 9L48V2M1jixEyHBpT+Suu2TnkUiGtY+NOUV45Zcc/DKbhNq/kTe3kunXRYRQR8/ttmHozx+4 PkOm8CZeApzB7/nlthMAgBxGSVwBbITrdcrIVDn2SCS50jPcn+p2uk3SU9vbNde9eFwDmVDs /cfLVjhbDjZ37PwkO/9E7c0wJ1ydqEHP6tH0p1k5S3dBO4iXIuASaPBz/Nk7RdtqOR8JNjkT elHQgc1SC3lTCRiZHwpVakerc+ngX7wdzBXslWIvbFx6G/WpOB0+OSyb4qJJYHXLSlTtmuz+ 3zrr1miOUkHFefPkwqXyS2ijcaayEsXX6pLTOHinhJwu3Wfx3cYFQYNfUe/qL+8kVT7WtRFK kVS+yw0rKF0+lbDczXmdxixoXrBpwJFHtQJQrd85waKxa7ZpQ2eAwDoUwKtdvQK9+FqbA0nj GabtN3VVG12mbeRR0qCo+L8QSyJBQAZKmoLZCkhRAQD4sX+rIxbsv4pZoYzeEJSpo2lcQwc0 wxmvwBl2OpO1Z9jO7GTuAGY02j19/AlWyZsvl2PNl9J+D+Vc2JMWmBFwV3S7PIFNZrAC1fY7 SJClM+Z4+QDS5qKkURhodnh/pn2up5p0xWG2zaD+qXNERzxpBZPmqgMsFlDyL9BaJpsRNMQS Ba7VfltzJFSJmC2SqR8fpi8Dc8npYC5S4m0Cq6JNoATMsMuHONiwM2ITR7At4wKuBh8+ZzTx b/GGSpRJS1HV/o5lWLeqxk1iO90nH5WKZzvqWDTlkz7i9JylVaaTrAKNFbmUwzKxPLsnekhy P4OZ6Oikk0BOMWnO3m/2dNNcTgicCZqbbir+pQ/XrPSfmJORTBxY9ePm+9JU9I+xcx9yLyYl kxRr2cEoLYJrSCcd1Xih7EKQOiHYKuTWlphYHx0YwnyhyJ6CWtthY9GH6YKkXAc3LQL5ZZJo zMtIa1s29xDFWbK/Sozd574oNAwfRinn1vQbSWiZzc7cpF6QBHR4ZnveQ62rHsCCS++tM0fp by811KLGsFaHFs8U8uGOuiyy16RvGQGnL4gVUX/JNQOKl7n95JnKnCsg/Jue5MMJBzPyyG0z QGTBRtE9+DBr5VkotbMjKGA6YyuFrImTEZdGmDa65ewNDXbrjLzm98eDL7QcGmEBm3u+aika eFE9N3GMaUKzARQro5xM7d31qZhtdbiorltyA47TnjGalKcDKw5fiuL0MxJga16xrFDvDywV E/SqMJRPq+EOZ+8HVMcfVF3bumK2fwOoDTK6eUpJ0H2uH1+8LadCBsAMB6LhyhQI6FyLZs+h +wmvZdOuQC4jxMrNPeAjzxVpjTXdSVbDPt4u8FIGpLvhyoq1kpGPc7WBBjw7czdcN5LKEQrf mKZiaee1bRRwk3OLyg6GXTXh7YPgJ0PvFVT0AZHKQ3YwJzKgfg42BAX+jMyF1wHwhJC2uN1G 25qK0wlevnUrmkw3JBODzK2BgVMJByF4UitmVEHo2vUEhuzXWvXIWxhZOuArRId8nlAQz5A4 bucxDq3WDrmZp+hjC47WEp5rK7sStt+8gDNgse6B9/AGpA8aDXowfTxNTtU9kW3Xppo2g7ao /J39v17c6zxOAYfpKo0D4SVz7MNUAvCL2tHGKkz8KQMFGDaWTezxTnfexvqI5gSeaPHoR2iF shjBsNTTBDihiyAmTYWWPwXKLhukf91udcPdu+5LGIKqefO/Dp1rIrLpG+5i3UsXs1118k6L YzVenSJFWnXimFThneKsM1NIm6lep4feQfn1/q0+ugEGs5Rqu1qak1ugLK4s2/PbFli9hOQ+ RrfPurYlr04j4trmIToH+NIAADtcYH/U+GB8QaStdVSbIOQbZ2f6VtN8lS3bR5LObYxWshsk ejfutDA2k6Y7q09VHrUmsXcGqREjSlosDG77i4qwLhmcSq+tAvE5hIC/yWhNcUMnooMvI+oQ Ay3bMb2ftkQMzuYKLu5dAAGeyvxyYyuBksjmc95h/uLDRcZ3APdK86/7jniamQzmuogJcjlE gGt0xqxzokwkWmPbSPow9lpBJh3JFLsQ6w7b8a3vj6dZoVtbpVupZO6/ScdBfr35rVo3So0D V8phvQzSfhqhJz18Q==
• Ironport-hdrordr: A9a23:uJzBlqyuQCtaecM2iBWgKrPwp71zdoMgy1knxilNoH1uA7Clfq WV9pkmPHDP+VIssR0b6Le90ey7MAvhHXAc2/hmAV+NNDOWz1dAb7sSnrcL+lXbalnDH5dmpO 5dmstFeaDN5e0Qt7eL3ODHKadY/DDdytHYuQ629R4EJnAJV0gj1XYDNu/8KDwJeOBoP/UE/f Gnl7B6TlSbCBIqhgXSPAhnYwEBnbP2fVDdDSLvt3UcmXyzZP+TiYIT43Ojr2gjuvp0ocZGzU H11zbh7qHmmfC2wB3R2ivy6NB5g93807J4db6xtvQ=
• Ironport-sdr: ocNrmHpkhoZf9UcRhZxwI1mr0H6RMZ1cqxIfBq6nykouIPSi/fPRLVw04yR4enUvmGIUulASCL 8krBUzeCTAPLujhnYcRr8235zNm53hCKBubxVNkRi1tu7wKcb81l08IL9uRrSMLh2RbLwFW4IX rYodkJbyxYb+VYQuCViJMD7SX+A24Lw44fSeHm2UMQRWa0K6F/TD6UJJjTDFmirq7qf8BvEjto lue5TydFUhG48aCA+kUZOUOdHcoolW+WRmwCoSL/wYLajxnYwiGlEBwg2eqPdSZWyFem3gFHor 5L02wArjqOdIGjGmLRhedHi8

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 TLA

You 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] = {} THEN
[campaign EXCEPT ![c.id] = c /\ randomActiveCampaign[c]]
ELSE campaign[c.id]

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

• References: